Skip to content
Snippets Groups Projects
Commit 2f1ad327 authored by andrew_miranti's avatar andrew_miranti
Browse files

Opcode disassembly compiles, now need to verify that it works

parent 85a1b2c2
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
decoder.k
+ 5
− 2
View file @ 2f1ad327
...@@ -23,6 +23,7 @@ require "registers.k" ...@@ -23,6 +23,7 @@ require "registers.k"
require "decoder-configuration.k" require "decoder-configuration.k"
require "generated_decoder_rules.k" require "generated_decoder_rules.k"
require "semantics-glue.k" require "semantics-glue.k"
require "inum-to-opcode.k"
require "x86-syntax.k" require "x86-syntax.k"
module DECODER module DECODER
...@@ -33,6 +34,7 @@ module DECODER ...@@ -33,6 +34,7 @@ module DECODER
imports DECODER-CONFIGURATION imports DECODER-CONFIGURATION
imports GENERATED-DECODER-RULES imports GENERATED-DECODER-RULES
imports SEMANTICS-GLUE imports SEMANTICS-GLUE
imports INUM-TO-OPCODE-FUNCTION
imports X86-SYNTAX imports X86-SYNTAX
syntax K ::= "SetMode" | "DecodePrefixes" | "ScanForVEX" | "ScanForEVEX" | "ScanForOpcode" | "ScanForMODRM" | "ScanForSIB" | "Disassemble" | "OutputDisassembly" | "IncrementInstruction" syntax K ::= "SetMode" | "DecodePrefixes" | "ScanForVEX" | "ScanForEVEX" | "ScanForOpcode" | "ScanForMODRM" | "ScanForSIB" | "Disassemble" | "OutputDisassembly" | "IncrementInstruction"
...@@ -91,10 +93,11 @@ module DECODER ...@@ -91,10 +93,11 @@ module DECODER
<decoderBuffer> _ => B </decoderBuffer> <decoderBuffer> _ => B </decoderBuffer>
<instructionpointer> _ => A </instructionpointer> <instructionpointer> _ => A </instructionpointer>
rule <k> OutputDisassembly => DecodedInstruction(Q, S, DisassemblyToOpcode(R, N, SF) .Operands) ... </k> rule <k> OutputDisassembly => DecodedInstruction(Q, S, INumOSZToOpcode(N, O) .Operands) ... </k>
<ilen> Q </ilen> <ilen> Q </ilen>
<REP> R </REP> <REP> R </REP>
<INAME> N </INAME> <INUM> N </INUM>
<OSZ> O </OSZ>
<suffix> SF </suffix> <suffix> SF </suffix>
<disassemblerOut> S </disassemblerOut> <disassemblerOut> S </disassemblerOut>
......
generator/datafiles/inum-opcode-map-groups.csv
+ 141
− 1
View file @ 2f1ad327
...@@ -350,10 +350,16 @@ ...@@ -350,10 +350,16 @@
311,sall 311,sall
311,salq 311,salq
311,salw 311,salw
311,shll
311,shlq
311,shlw
312,sall 312,sall
312,salq 312,salq
312,salw 312,salw
312,shll
312,shlq
312,shlw
313,sarl 313,sarl
313,sarq 313,sarq
...@@ -372,8 +378,10 @@ ...@@ -372,8 +378,10 @@
318,rcrb 318,rcrb
319,salb 319,salb
319,shlb
320,salb 320,salb
320,shlb
321,shrb 321,shrb
...@@ -402,10 +410,16 @@ ...@@ -402,10 +410,16 @@
331,sall 331,sall
331,salq 331,salq
331,salw 331,salw
331,shll
331,shlq
331,shlw
332,sall 332,sall
332,salq 332,salq
332,salw 332,salw
332,shll
332,shlq
332,shlw
333,shrl 333,shrl
333,shrq 333,shrq
...@@ -1125,31 +1139,67 @@ ...@@ -1125,31 +1139,67 @@
930,cmovbl 930,cmovbl
930,cmovbq 930,cmovbq
930,cmovbw 930,cmovbw
930,cmovcl
930,cmovcq
930,cmovcw
930,cmovnael
930,cmovnaeq
930,cmovnaew
931,cmovbl 931,cmovbl
931,cmovbq 931,cmovbq
931,cmovbw 931,cmovbw
931,cmovcl
931,cmovcq
931,cmovcw
931,cmovnael
931,cmovnaeq
931,cmovnaew
932,cmovael
932,cmovaeq
932,cmovaew
932,cmovnbl 932,cmovnbl
932,cmovnbq 932,cmovnbq
932,cmovnbw 932,cmovnbw
932,cmovncl
932,cmovncq
932,cmovncw
933,cmovael
933,cmovaeq
933,cmovaew
933,cmovnbl 933,cmovnbl
933,cmovnbq 933,cmovnbq
933,cmovnbw 933,cmovnbw
933,cmovncl
933,cmovncq
933,cmovncw
934,cmovel
934,cmoveq
934,cmovew
934,cmovzl 934,cmovzl
934,cmovzq 934,cmovzq
934,cmovzw 934,cmovzw
935,cmovel
935,cmoveq
935,cmovew
935,cmovzl 935,cmovzl
935,cmovzq 935,cmovzq
935,cmovzw 935,cmovzw
936,cmovnel
936,cmovneq
936,cmovnew
936,cmovnzl 936,cmovnzl
936,cmovnzq 936,cmovnzq
936,cmovnzw 936,cmovnzw
937,cmovnel
937,cmovneq
937,cmovnew
937,cmovnzl 937,cmovnzl
937,cmovnzq 937,cmovnzq
937,cmovnzw 937,cmovnzw
...@@ -1157,15 +1207,27 @@ ...@@ -1157,15 +1207,27 @@
938,cmovbel 938,cmovbel
938,cmovbeq 938,cmovbeq
938,cmovbew 938,cmovbew
938,cmovnal
938,cmovnaq
938,cmovnaw
939,cmovbel 939,cmovbel
939,cmovbeq 939,cmovbeq
939,cmovbew 939,cmovbew
939,cmovnal
939,cmovnaq
939,cmovnaw
940,cmoval
940,cmovaq
940,cmovaw
940,cmovnbel 940,cmovnbel
940,cmovnbeq 940,cmovnbeq
940,cmovnbew 940,cmovnbew
941,cmoval
941,cmovaq
941,cmovaw
941,cmovnbel 941,cmovnbel
941,cmovnbeq 941,cmovnbeq
941,cmovnbew 941,cmovnbew
...@@ -1299,15 +1361,23 @@ ...@@ -1299,15 +1361,23 @@
1032,jno 1032,jno
1034,jb 1034,jb
1034,jc
1034,jnae
1036,jae
1036,jnb 1036,jnb
1036,jnc
1038,je
1038,jz 1038,jz
1040,jne
1040,jnz 1040,jnz
1042,jbe 1042,jbe
1042,jna
1044,ja
1044,jnbe 1044,jnbe
1045,seto 1045,seto
...@@ -1319,27 +1389,43 @@ ...@@ -1319,27 +1389,43 @@
1048,setno 1048,setno
1049,setb 1049,setb
1049,setc
1049,setnae
1050,setb 1050,setb
1050,setc
1050,setnae
1051,setae
1051,setnb 1051,setnb
1051,setnc
1052,setae
1052,setnb 1052,setnb
1052,setnc
1053,sete
1053,setz 1053,setz
1054,sete
1054,setz 1054,setz
1055,setne
1055,setnz 1055,setnz
1056,setne
1056,setnz 1056,setnz
1057,setbe 1057,setbe
1057,setna
1058,setbe 1058,setbe
1058,setna
1059,seta
1059,setnbe 1059,setnbe
1060,seta
1060,setnbe 1060,setnbe
1064,btl 1064,btl
...@@ -1631,31 +1717,55 @@ ...@@ -1631,31 +1717,55 @@
1260,cmovpel 1260,cmovpel
1260,cmovpeq 1260,cmovpeq
1260,cmovpew 1260,cmovpew
1260,cmovpl
1260,cmovpq
1260,cmovpw
1261,cmovpel 1261,cmovpel
1261,cmovpeq 1261,cmovpeq
1261,cmovpew 1261,cmovpew
1261,cmovpl
1261,cmovpq
1261,cmovpw
1262,cmovnpl 1262,cmovnpl
1262,cmovnpq 1262,cmovnpq
1262,cmovnpw 1262,cmovnpw
1262,cmovpol
1262,cmovpoq
1262,cmovpow
1263,cmovnpl 1263,cmovnpl
1263,cmovnpq 1263,cmovnpq
1263,cmovnpw 1263,cmovnpw
1263,cmovpol
1263,cmovpoq
1263,cmovpow
1264,cmovll 1264,cmovll
1264,cmovlq 1264,cmovlq
1264,cmovlw 1264,cmovlw
1264,cmovngel
1264,cmovngeq
1264,cmovngew
1265,cmovll 1265,cmovll
1265,cmovlq 1265,cmovlq
1265,cmovlw 1265,cmovlw
1265,cmovngel
1265,cmovngeq
1265,cmovngew
1266,cmovgel
1266,cmovgeq
1266,cmovgew
1266,cmovnll 1266,cmovnll
1266,cmovnlq 1266,cmovnlq
1266,cmovnlw 1266,cmovnlw
1267,cmovgel
1267,cmovgeq
1267,cmovgew
1267,cmovnll 1267,cmovnll
1267,cmovnlq 1267,cmovnlq
1267,cmovnlw 1267,cmovnlw
...@@ -1663,15 +1773,27 @@ ...@@ -1663,15 +1773,27 @@
1268,cmovlel 1268,cmovlel
1268,cmovleq 1268,cmovleq
1268,cmovlew 1268,cmovlew
1268,cmovngl
1268,cmovngq
1268,cmovngw
1269,cmovlel 1269,cmovlel
1269,cmovleq 1269,cmovleq
1269,cmovlew 1269,cmovlew
1269,cmovngl
1269,cmovngq
1269,cmovngw
1270,cmovgl
1270,cmovgq
1270,cmovgw
1270,cmovnlel 1270,cmovnlel
1270,cmovnleq 1270,cmovnleq
1270,cmovnlew 1270,cmovnlew
1271,cmovgl
1271,cmovgq
1271,cmovgw
1271,cmovnlel 1271,cmovnlel
1271,cmovnleq 1271,cmovnleq
1271,cmovnlew 1271,cmovnlew
...@@ -1875,15 +1997,21 @@ ...@@ -1875,15 +1997,21 @@
1413,jns 1413,jns
1415,jp 1415,jp
1415,jpe
1417,jnp 1417,jnp
1417,jpo
1419,jl 1419,jl
1419,jnge
1421,jge
1421,jnl 1421,jnl
1423,jle
1423,jng 1423,jng
1425,jg
1425,jnle 1425,jnle
1426,sets 1426,sets
...@@ -1895,27 +2023,39 @@ ...@@ -1895,27 +2023,39 @@
1429,setns 1429,setns
1430,setp 1430,setp
1430,setpe
1431,setp 1431,setp
1431,setpe
1432,setnp 1432,setnp
1432,setpo
1433,setnp 1433,setnp
1433,setpo
1434,setl 1434,setl
1434,setnge
1435,setl 1435,setl
1435,setnge
1436,setge
1436,setnl 1436,setnl
1437,setge
1437,setnl 1437,setnl
1438,setle 1438,setle
1438,setng
1439,setle 1439,setle
1439,setng
1440,setg
1440,setnle 1440,setnle
1441,setg
1441,setnle 1441,setnle
1446,btsl 1446,btsl
......
generator/generate-opcode-decoder.py 0 → 100755
+ 69
− 0
View file @ 2f1ad327
#!/usr/bin/python3
import kcodegen
inum_lookup_table = {}
osz_suffixes = ["b", "w", "l", "q", "x", "y", "z"]
with open("datafiles/inum-opcode-map-groups.csv", "r") as f:
for line in f.readlines():
line = line.strip()
comment_start = line.find("#")
if comment_start > 0:
line = line[:(comment_start - 1)]
elif comment_start == 0:
continue
sections = line.split(",")
assert len(sections) <= 2
if len(sections) < 2:
continue # Not a declaration line
inum = int(sections[0])
opcode = sections[1]
assert len(opcode) > 0
existing = inum_lookup_table.get(inum, list())
existing.append(opcode)
inum_lookup_table[inum] = existing
rules = []
rule_template = "rule INumOSZToOpcode({0}, {1}) => {2}"
for (inum, opcodes) in inum_lookup_table.items():
opcode_group = opcodes
if len(opcodes) > 1:
first_opcode = opcodes[0]
has_osz_suffix = first_opcode[-1] in osz_suffixes
no_suffix = first_opcode[:-1]
opcode_group = [first_opcode]
if has_osz_suffix:
for other_opcode in opcodes[1:]:
if other_opcode[-1] in osz_suffixes and no_suffix == other_opcode[:-1]:
opcode_group.append(other_opcode)
if len(opcode_group) > 1:
opcode_group.sort(key=lambda x: osz_suffixes.index(x[-1]))
assert len(opcode_group) <= 3, "Too many opcodes: {0}".format(','.join(opcode_group))
if len(opcode_group) == 1:
rules.append(rule_template.format(inum, "_", opcode_group[0]))
else:
for opcode in opcode_group:
suffix = opcode[-1]
assert suffix in osz_suffixes
rules.append(rule_template.format(inum, osz_suffixes.index(suffix) - 1, opcode))
print("""require "x86-syntax.k"
module INUM-TO-OPCODE-FUNCTION
imports X86-SYNTAX
syntax Opcode ::= INumOSZToOpcode(Int, Int) [function]
{0}
endmodule""".format('\n'.join([' ' + rule for rule in rules])))
inum-to-opcode.k 0 → 100644
+ 2636
− 0
View file @ 2f1ad327
This diff is collapsed.
semantics-glue.k
+ 0
− 2
View file @ 2f1ad327
...@@ -10,9 +10,7 @@ module SEMANTICS-GLUE ...@@ -10,9 +10,7 @@ module SEMANTICS-GLUE
syntax Register ::= UnsupportedRegister syntax Register ::= UnsupportedRegister
syntax Register ::= DissassemblerRegisterToSemanticsRegister(K, Bool) [function] syntax Register ::= DissassemblerRegisterToSemanticsRegister(K, Bool) [function]
syntax Opcode ::= DissassemblerToOpcode(Int, String, String) [function]
rule DisassemblerRegisterToSemanticsRegister(REG_INVALID, _) => %invalid rule DisassemblerRegisterToSemanticsRegister(REG_INVALID, _) => %invalid
rule DisassemblerRegisterToSemanticsRegister(REG_BND0, _) => %bnd0 rule DisassemblerRegisterToSemanticsRegister(REG_BND0, _) => %bnd0
......
test-decoder.k
+ 4
− 2
View file @ 2f1ad327
...@@ -63,8 +63,10 @@ module TEST-DECODER ...@@ -63,8 +63,10 @@ module TEST-DECODER
syntax KResult ::= DecoderResult syntax KResult ::= DecoderResult
syntax K ::= CheckDecodeLen(K, Int) [strict] syntax K ::= CheckDecodeLen(K, Int) [strict]
syntax String ::= OpcodeToString(Opcode) [function, hook(STRING.token2string)]
rule Disassemble(Addr:HexToken, Isn:HexToken) => CheckDecodeLen(Decode(HexTokenToInt(Addr), HexTokenToInts(Isn)), CountInInts(HexTokenToInts(Isn))) rule Disassemble(Addr:HexToken, Isn:HexToken) => CheckDecodeLen(Decode(HexTokenToInt(Addr), HexTokenToInts(Isn)), CountInInts(HexTokenToInts(Isn)))
rule <k> CheckDecodeLen(DecodedInstruction(I:Int, S:String, _:Instruction), I) => . ... </k> rule <k> CheckDecodeLen(DecodedInstruction(I:Int, S:String, O:Opcode _:Operands), I) => . ... </k>
<output> ... (.List => ListItem(S +String "\n")) </output> <output> ... (.List => ListItem(S +String " " +String OpcodeToString(O) +String "\n")) </output>
endmodule endmodule
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment