From 910796a4026b15604f8e14a1c8bb96f2b726b84b Mon Sep 17 00:00:00 2001
From: Andrew Miranti <andrew.h.miranti@gmail.com>
Date: Wed, 9 Jan 2019 14:12:01 -0600
Subject: [PATCH] Temporary commit
---
build.sh | 14 +-
decoder-syntax.k => decoder-configuration.k | 69 +-------
decoder.k | 47 +++--
generator/build.py | 4 +
generator/disasm_to_iclass.py | 11 +-
generator/generate.py | 126 ++++---------
generator/generate_all.py | 186 --------------------
test-decoder.k | 57 ++++++
8 files changed, 144 insertions(+), 370 deletions(-)
rename decoder-syntax.k => decoder-configuration.k (86%)
create mode 100644 generator/build.py
delete mode 100755 generator/generate_all.py
create mode 100644 test-decoder.k
diff --git a/build.sh b/build.sh
index 0569a82..e8afeb9 100755
--- a/build.sh
+++ b/build.sh
@@ -1,9 +1,7 @@
#!/bin/bash
-kompile --backend ocaml decoder.k &
-until ps -f | grep -m 1 "[0-9] ocamlc"; do sleep 10 ; done
-killall -9 java
-#sleep 1
-#wait $(ps -f | grep "[0-9] ocamlc" | grep -Eo "[0-9]+" | head -1)
-#cd decoder-kompiled
-#ocamlfind c -g -passopt stdlib.cma -linkpkg -a -o realdef.cma realdef.cmo
-#cd ..
+CURR=$(pwd)
+cd "$(dirname $0)/generator"
+./generate.py $(< ./disasm_to_iclass.py $@) > ../generated_decoder_rules.k
+cd ..
+kompile decoder.k --backend ocaml -I $X86_SEMANTICS
+cd $CURR
diff --git a/decoder-syntax.k b/decoder-configuration.k
similarity index 86%
rename from decoder-syntax.k
rename to decoder-configuration.k
index 5cb4c61..02e9977 100644
--- a/decoder-syntax.k
+++ b/decoder-configuration.k
@@ -1,59 +1,7 @@
-/*BEGIN_LEGAL
- *
- * Adapted from Intel's XED (Copyright (c) 2018 Intel Corporation)
- *
- * END_LEGAL */
-
-require "registers.k"
-require "categories.k"
-
-module DECODER-SYNTAX
- imports DOMAINS-SYNTAX
-
- syntax HexToken ::= r"0x[0-9a-fA-F]+" [token, prec(2)]
-
- syntax Stmt ::= "Disassemble" "(" HexToken "," HexToken ")"
- syntax Stmts ::= List{Stmt, ";"}
-
- syntax Ints ::= List{Int, " "}
-
- syntax Pgm ::= Stmts ";"
-endmodule
-
-module DECODER-CONVERSIONS
- imports DECODER-SYNTAX
- imports DOMAINS
-
- syntax HexTokens ::= List{HexToken, " "}
-
- syntax Int ::= HexStringToInt(String) [function]
- rule HexStringToInt(S:String) => String2Base(S, 16)
-
- syntax String ::= StringifyHexToken(HexToken) [function, hook(STRING.token2string)]
-
- syntax String ::= removeFirstTwoChars(String) [function]
- rule removeFirstTwoChars(S) => substrString(S, 2, lengthString(S))
-
- syntax String ::= HexTokenToString(HexToken) [function]
- rule HexTokenToString(H) => removeFirstTwoChars(StringifyHexToken(H))
-
- syntax Ints ::= HexTokenToInts(HexToken) [function]
- syntax Ints ::= ImplHexTokenToInts(String) [function]
-
- rule HexTokenToInts(Ht) => ImplHexTokenToInts(HexTokenToString(Ht))
-
- rule ImplHexTokenToInts("") => .Ints
- rule ImplHexTokenToInts(S) => String2Base(substrString(S, 0, 2), 16) ImplHexTokenToInts(substrString(S, 2, lengthString(S))) requires 2 dividesInt lengthString(S) andBool lengthString(S) >Int 0
-
- syntax Int ::= HexTokenToInt(HexToken) [function]
- rule HexTokenToInt(H) => HexStringToInt(HexTokenToString(H))
-
- syntax KResult ::= HexToken
-endmodule
+requires "registers.k"
+requires "categories.k"
module DECODER-CONFIGURATION
- imports DECODER-SYNTAX
- imports DECODER-CONVERSIONS
imports DOMAINS
imports REGISTERS-SYNTAX
imports CATEGORIES-SYNTAX
@@ -201,15 +149,7 @@ module DECODER-CONFIGURATION
</decoderInternal>
- configuration <T color="yellow">
- <k color="green"> $PGM:Pgm </k>
- <MemCache color="purple"> .Map </MemCache>
- <ROM color="red"> .List </ROM>
- <entry color="blue"> 0 </entry>
-
- <output stream="stdout"> .List </output>
-
- <decoder>
+ configuration <decoder>
<mode> mode64 </mode>
<smode> mode64 </smode>
<instructionpointer> 0 </instructionpointer>
@@ -349,7 +289,4 @@ module DECODER-CONFIGURATION
</decoderInternal>
</decoder>
- </T>
-
endmodule
-
diff --git a/decoder.k b/decoder.k
index 60e317e..4fca4ee 100644
--- a/decoder.k
+++ b/decoder.k
@@ -21,26 +21,33 @@ require "has_modrm.k"
require "has_disp_regular.k"
require "registers.k"
require "decoder-syntax.k"
-require "generated_decoder_rules.k" // VERY slow
-//require "generated/generated-header.k"
+require "generated_decoder_rules.k"
+require "x86-syntax.k"
+
+module DECODER-INTERFACE
+ imports DOMAINS
+
+ syntax Ints ::= List{Int, " "}
+
+ syntax K ::= Decode(Int, Ints)
+
+ syntax DecoderError
+ //Len, DisassemblyString, x86-Semantics Instruction
+ syntax DecoderResult ::= DecoderResult(Int, String, Instruction) | DecoderError
+endmodule
module DECODER
- imports DECODER-SYNTAX
- imports DECODER-CONVERSIONS
+ imports DECODER-INTERFACE
imports HAS-MODRM-MAP
imports HAS-DISP-REGULAR
imports DOMAINS
imports DECODER-CONFIGURATION
imports GENERATED-DECODER-RULES
+ imports X86-SYNTAX
- rule S:Stmts ; => S [structural]
- rule S1 ; S2 => S1 ~> S2 [structural]
- rule .Stmts => . [structural]
syntax K ::= "SetMode" | "DecodePrefixes" | "ScanForVEX" | "ScanForEVEX" | "ScanForOpcode" | "ScanForMODRM" | "ScanForSIB" | "Disassemble" | "OutputDisassembly" | "IncrementInstruction"
-
-
syntax Int ::= IntModeFromSymbol(K) [function]
rule IntModeFromSymbol(mode16) => 0
@@ -75,9 +82,9 @@ module DECODER
rule padIntsAux(Is, L) => 0 padIntsAux(Is, L -Int 1) requires L >Int 0
rule padIntsAux(Is, 0) => Is
- rule Disassemble(Addr:HexToken, Isn:HexToken) =>
+ rule Decode(Addr:Int, Bytes:Ints) =>
ResetDecoder ~>
- InitDecoder(HexTokenToInt(Addr), padInts(HexTokenToInts(Isn), 15)) ~>
+ InitDecoder(Addr, Bytes) ~>
SetMode ~>
DecodePrefixes ~>
ScanForVEX ~>
@@ -532,7 +539,9 @@ module DECODER
rule <k> ParseEVEX => DecoderOutOfBytes ... </k>
<decoderBuffer> I1:Int I2:Int I3:Int I4:Int .Ints </decoderBuffer>
- syntax K ::= "CheckUBIT" | "BadUBIT"
+ syntax K ::= "CheckUBIT"
+
+ syntax DecoderError ::= "BadUBIT"
rule <k> CheckUBIT => BadUBIT ... </k>
<UBIT> 0 </UBIT> // We're not going to support KNC for the foreseeable future.
@@ -540,7 +549,9 @@ module DECODER
rule <k> CheckUBIT => . ... </k>
<UBIT> 1 </UBIT>
- syntax K ::= "CheckVEXDEST4" | "BadVEXDEST4"
+ syntax K ::= "CheckVEXDEST4"
+
+ syntax DecoderError ::= "BadVEXDEST4"
rule <k> CheckVEXDEST4 => . ... </k>
<VEXDEST4> V </VEXDEST4>
@@ -552,7 +563,9 @@ module DECODER
<mode> M </mode>
requires M =/=K mode64 andBool I:Int =/=Int 0
- syntax K ::= "CheckMASK" | "BadMASK"
+ syntax K ::= "CheckMASK"
+
+ syntax DecoderError ::= "BadMASK"
rule <k> CheckMASK => . ... </k>
<MASK> I:Int </MASK>
@@ -687,7 +700,7 @@ module DECODER
<REG> _ => (I:Int >>Int 3) &Int 7 </REG>
<RM> _ => (I:Int &Int 7) </RM>
- syntax K ::= "BadLL"
+ syntax DecoderError ::= "BadLL"
rule <k> CheckLL => BadLL ... </k>
<LLRC> L </LLRC>
@@ -785,7 +798,9 @@ module DECODER
syntax K ::= ReadLittleEndian(Int, Int, Int)
- syntax K ::= ReadDisp(Int) | "SetDisp" | "InvalidDisp"
+ syntax K ::= ReadDisp(Int) | "SetDisp"
+
+ syntax DecoderError ::= "InvalidDisp"
rule ReadDisp(0) => .
rule ReadDisp(8) => ReadLittleEndian(1, 0, 0) ~> SetDisp
diff --git a/generator/build.py b/generator/build.py
new file mode 100644
index 0000000..e311a5e
--- /dev/null
+++ b/generator/build.py
@@ -0,0 +1,4 @@
+import sys
+from disasm_to_iclass import get_iclasses_from_disasms
+fromm
+
diff --git a/generator/disasm_to_iclass.py b/generator/disasm_to_iclass.py
index 282d134..39a74ab 100755
--- a/generator/disasm_to_iclass.py
+++ b/generator/disasm_to_iclass.py
@@ -11979,10 +11979,9 @@ lookup_table = {
"vgf2p8mulb": ["VGF2P8MULB"],
}
-result = set()
-for arg in sys.argv[1:]:
- assert arg in lookup_table
- result |= set(lookup_table[arg])
+def get_iclasses_from_disasms(disasms):
+ return list(set([lookup_table[disasm] for disasm in disasms]))
-for ret in result:
- print(ret)
+if __name__ == "__main__":
+ for ret in get_iclasses_from_disasms(sys.argv[1:]):
+ print(ret)
diff --git a/generator/generate.py b/generator/generate.py
index aadda05..a18d2db 100755
--- a/generator/generate.py
+++ b/generator/generate.py
@@ -23,17 +23,8 @@
import instructions
import nonterminals
import sys
-import os
-import shutil
from kcodegen import kRewrite
-out_folder = "generated"
-
-if os.path.exists(out_folder): # https://stackoverflow.com/questions/273192/how-can-i-safely-create-a-nested-directory-in-python Is there a nicer way to do this?
- shutil.rmtree(out_folder)
-
-os.makedirs(out_folder)
-
class FreshVariableGenerator(object):
def __init__(self, prefix="I"):
self._prefix = prefix
@@ -127,45 +118,33 @@ def gen_from_inst(inst):
ret.add_literal_match("VEXVALID", "0")
return ret
-def make_outreg_rule(name):
- return """syntax K ::= "OUTREGTo{0}"
- rule <k> OUTREGTo{0} => . ... </k>
- <OUTREG> M </OUTREG>
- <{0}> _ => M </{0}>
-""".format(name)
-
-def write_to_file(name, contents):
- with open(out_folder + "/" + name, "w") as f:
- f.write(contents.replace("XED_", ""))
-
-generated_syntax_name = "generated-syntax.k"
-generated_syntax_contents = """// GENERATED CODE, DO NOT MODIFY.
-// Generated based on input data from Intel's XED disassembler (in particular, all_dec_instructions.txt)
-require "../decoder-syntax.k"
-module GENERATED-DECODER-RULES-COMMON
- imports DOMAINS
- imports COLLECTIONS
- imports DECODER-SYNTAX
- imports DECODER-CONFIGURATION
-
- syntax K ::= "DecoderError"
-
- syntax K ::= "ScanForDisp"
-
- syntax K ::= "ScanForImmediate"
-
- syntax OperandVisibility ::= "SUPPRESSED" | "IMPLICIT" | "EXPLICIT"
- syntax OperandWidth ::= Int | "AUTO" | "VECTOR" | "SSZ" | "ASZ" // Explicit bit count, AUTO for register arguments whose width is inferred from its value, and VECTOR for NELEM*ELEMSIZE
- syntax KResult ::= OperandWidth
- syntax KItem ::= OperandMetadata(KItem, Bool, OperandVisibility, KItem, OperandWidth, OperandWidth, OperandWidth) // Name, IsWriteMask, Visibility, C-Type, Wdith16, Width32, Width64
-"""
+def print_outreg_to(name):
+ print("syntax K ::= \"OUTREGTo" + name + "\"")
+ print("rule <k> OUTREGTo" + name + " => . ... </k>")
+ print("<OUTREG> M </OUTREG>")
+ print("<" + name + "> _ => M </" + name + ">")
+
+
+print("require \"decoder-syntax.k\"")
+print("module GENERATED-DECODER-RULES")
+print("imports DOMAINS")
+print("imports COLLECTIONS")
+print("imports DECODER-SYNTAX")
+print("imports DECODER-CONFIGURATION")
+print("syntax K ::= \"DecoderError\"")
+print("syntax K ::= \"ScanForDisp\"")
+print("syntax K ::= \"ScanForImmediate\"")
+print('syntax OperandVisibility ::= "SUPPRESSED" | "IMPLICIT" | "EXPLICIT"')
+print('syntax OperandWidth ::= Int | "AUTO" | "VECTOR" | "SSZ" | "ASZ"') # Explicit bit count, AUTO for register arguments whose width is inferred from its value, and VECTOR for NELEM*ELEMSIZE
+print('syntax KResult ::= OperandWidth')
+print("syntax KItem ::= OperandMetadata(KItem, Bool, OperandVisibility, KItem, OperandWidth, OperandWidth, OperandWidth)") # Name, IsWriteMask, Visibility, C-Type, Wdith16, Width32, Width64
outregs_done = set()
for name in nonterminals.nonterminals_map:
for alternative in nonterminals.nonterminals_map[name]:
for assign in alternative.consequent.get(nonterminals.ComplexAssignment.__name__, []):
if assign.name != "OUTREG" and assign.name not in outregs_done:
- generated_syntax_contents += make_outreg_rule(assign.name)
+ print_outreg_to(assign.name)
outregs_done.add(assign.name)
attributes_done = set()
@@ -175,62 +154,33 @@ for inst in instructions.instruction_list:
for operand in inst.operands:
assign = operand[0]
if assign.__class__.__name__ == "ComplexAssignment" and assign.name not in outregs_done:
- generated_syntax_contents += make_outreg_rule(assign.name)
+ print_outreg_to(assign.name)
outregs_done.add(assign.name)
attributes_done |= set(inst.attributes)
operand_metadata_ids |= set([id_ for (_, id_, _, _, _, _, _, _) in inst.operands])
operand_sort_set |= set([sort for (_, _, _, _, sort, _, _, _) in inst.operands])
-generated_syntax_contents += " syntax KItem ::= " + " | ".join(['"A_{0}"'.format(attribute) for attribute in attributes_done]) + "\n"
-generated_syntax_contents += " syntax KItem ::= " + " | ".join(['"{0}"'.format(id_) for id_ in operand_metadata_ids]) + "\n"
-generated_syntax_contents += " syntax KItem ::= " + " | ".join(['"{0}"'.format(sort) for sort in operand_sort_set]) + "\n"
+print("syntax KItem ::= " + " | ".join(['"A_{0}"'.format(attribute) for attribute in attributes_done]))
+print("syntax KItem ::= " + " | ".join(['"{0}"'.format(id_) for id_ in operand_metadata_ids]))
+print("syntax KItem ::= " + " | ".join(['"{0}"'.format(sort) for sort in operand_sort_set]))
-generated_syntax_contents += " syntax K ::= \"Instruction\"\n"
-generated_syntax_contents += " syntax IClass ::= " + " | ".join(list(set(["\"{0}\"".format(inst.iclass) for inst in instructions.instruction_list]))) + "\n"
+print("syntax K ::= \"Instruction\"")
+iclasses = list(set(["\"{0}\"".format(inst.iclass) for inst in instructions.instruction_list]))
+print("syntax IClass ::= " + " | ".join(iclasses))
+
+desired = set([n.upper() for n in sys.argv[1:]])
+
+for inst in instructions.instruction_list:
+ if len(desired) == 0 or inst.iclass in desired:
+ print("// UNAME: " + inst.uname)
+ print(gen_from_inst(inst).generate_rule().replace("XED_", ""))
for name in nonterminals.nonterminals_map:
if "SPLITTER" in name or "PREFIX" in name:
continue
- generated_syntax_contents += " syntax K ::= \"" + name + "\"\n"
+ print("syntax K ::= \"" + name + "\"")
for alternative in nonterminals.nonterminals_map[name]:
- generated_syntax_contents += gen_from_nonterminal(alternative).generate_rule() + "\n"
+ print(gen_from_nonterminal(alternative).generate_rule().replace("XED_", ""))
-generated_syntax_contents += "endmodule\n"
-
-write_to_file(generated_syntax_name, generated_syntax_contents)
-
-definition_name = "{0}-definition.k"
-definition_contents = """require "{0}"
-module {1}-DEFINITION
- imports GENERATED-DECODER-RULES-COMMON
-{2}
-endmodule
-"""
-
-desired_iclasses = set([name.upper() for name in sys.argv[1:]])
-
-inst_map = {}
-for inst in instructions.instruction_list:
- if len(desired_iclasses) == 0 or inst.iclass in desired_iclasses:
- contents = inst_map.get(inst.iclass, "")
- contents += gen_from_inst(inst).generate_rule()
- contents += "\n"
- inst_map[inst.iclass] = contents
-
-definition_modules = []
-for iclass in inst_map:
- name = definition_name.format(iclass)
- write_to_file(name, definition_contents.format(generated_syntax_name, iclass, inst_map[iclass]))
- definition_modules.append((name, "{0}-DEFINITION".format(iclass)))
-
-imported_file_name = "generated-header.k"
-imported_file_contents = """
-require "{0}"
-{1}
-module GENERATED-DECODER-RULES
-{2}
-endmodule
-""".format(generated_syntax_name, "\n".join(["require \"{0}\"".format(filename) for (filename, _) in definition_modules]), "\n".join(["imports {0}".format(module_name) for (_, module_name) in definition_modules]))
-
-write_to_file(imported_file_name, imported_file_contents)
+print("endmodule")
diff --git a/generator/generate_all.py b/generator/generate_all.py
deleted file mode 100755
index a18d2db..0000000
--- a/generator/generate_all.py
+++ /dev/null
@@ -1,186 +0,0 @@
-#!/usr/bin/python3
-
-#BEGIN_LEGAL
-#
-# A Re-Implementation of Intels disassembler from XED in K semantics.
-#
-# Copyright (c) 2018 Intel Corporation
-#
-# Licensed under the Apache License, Version 2.0 (the "License");
-# you may not use this file except in compliance with the License.
-# You may obtain a copy of the License at
-#
-# http://www.apache.org/licenses/LICENSE-2.0
-#
-# Unless required by applicable law or agreed to in writing, software
-# distributed under the License is distributed on an "AS IS" BASIS,
-# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-# See the License for the specific language governing permissions and
-# limitations under the License.
-#
-# END_LEGAL
-
-import instructions
-import nonterminals
-import sys
-from kcodegen import kRewrite
-
-class FreshVariableGenerator(object):
- def __init__(self, prefix="I"):
- self._prefix = prefix
- self._val = 0
- self.next_variable()
-
- def next_variable(self):
- self._current = self._prefix + str(self._val)
- self._val += 1
- return self._current
-
- def last_variable(self):
- return self._current
-
-def gen_from_nonterminal(nonterm, additional = ""):
- rewrite = kRewrite()
- fresh_vars = FreshVariableGenerator()
-
- pattern = nonterm.antecedent
- assignments = nonterm.consequent
-
- literal = " ".join([str(int(match.pattern, 16)) for match in pattern.get(nonterminals.NoncapturingMatch.__name__, [])])
- if len(literal) > 0:
- rewrite.add_literal_match("dynamicDecoderBuffer", literal + " _:Ints ")
-
- reads = [eq for eq in pattern.get(nonterminals.Equation.__name__, [])]
- writes = [assign for assign in assignments.get(nonterminals.SimpleAssignment.__name__, [])]
-
- bound_names = {}
- matches = []
- for read in reads:
- for write in writes:
- if read.name == write.name:
- rewrite.add_rewrite(read.name, read.val, write.val)
- bound_names[read.name] = read.val
-
- for cap in pattern.get(nonterminals.Capture.__name__, []):
- assert len(cap.vars) > 0
- name = cap.name
- value = cap.vars[0].required_val
- if value is not None:
- bound_names[name] = value
- rewrite.add_literal_match(name, value)
-
- inequalities = []
- for eq in pattern.get(nonterminals.Equation.__name__, []):
- if eq.name in bound_names:
- assert (bound_names[eq.name] == eq.val) == eq.is_equal # Either both equal, or both not equal.
- else:
- if eq.is_equal:
- rewrite.add_literal_match(eq.name, eq.val)
- else:
- rewrite.add_variable(eq.name, fresh_vars.next_variable(), "Int")
- inequalities.append((fresh_vars.last_variable(), eq.val))
- if len(inequalities) > 0:
- rewrite.set_condition(" andBool ".join(["{0} =/=Int {1}".format(name, value) for (name, value) in inequalities]))
-
-
- if len(pattern.get(nonterminals.OtherwiseCondition.__name__, [])) > 0:
- rewrite.add_attribute("owise")
-
-
- for assign in assignments.get(nonterminals.SimpleAssignment.__name__, []):
- if assign.name not in bound_names:
- rewrite.add_rewrite(assign.name, "_", assign.val)
-
- decode_nonterminals = " ~> ".join([nonterm.name for nonterm in pattern.get(nonterminals.NonterminalCondition.__name__, [])])
-
- if len(additional) > 0:
- decode_nonterminals += (" ~> " if len(decode_nonterminals) > 0 else "") + additional
-
- for assign in assignments.get(nonterminals.ComplexAssignment.__name__, []):
- decode_nonterminals += (" ~> " if len(decode_nonterminals) > 0 else "") + assign.func_name + (" ~> OUTREGTo" + assign.name if assign.name != "OUTREG" else "")
-
- if len(assignments.get(nonterminals.DecoderError.__name__, [])) > 0:
- rewrite.add_rewrite("k", nonterm.name, "DecoderError", False)
- else:
- rewrite.add_rewrite("k", nonterm.name, decode_nonterminals if len(decode_nonterminals) else ".", False)
-
- return rewrite
-
-def gen_from_inst(inst):
- ret = gen_from_nonterminal(inst, "ScanForDisp ~> ScanForImmediate")
- ret.add_rewrite("ICLASS", "_", inst.iclass)
- ret.add_rewrite("INUM", "_", inst.id)
- ret.add_rewrite("CATEGORY", "_", "\"CATEGORY_{0}\"".format(inst.category))
- ret.add_rewrite("INAME", "_", "\"" + inst.iname + "\"")
- ret.add_rewrite("ATTRIBUTES", "_", "{0}".format(" ".join(["ListItem(A_{0})".format(name) for name in inst.attributes])) if len(inst.attributes) > 0 else ".List")
- ret.add_rewrite("OPERANDS", "_", " ".join(["ListItem(OperandMetadata({0},{1},{2},{3},{4},{5},{6}))".format(name, str(mask).lower(), vis, sort, width16, width32, width64) for (_, name, mask, vis, sort, width16, width32, width64) in inst.operands]) if len(inst.operands) > 0 else ".List")
- if not inst.has_vexvalid:
- ret.add_literal_match("VEXVALID", "0")
- return ret
-
-def print_outreg_to(name):
- print("syntax K ::= \"OUTREGTo" + name + "\"")
- print("rule <k> OUTREGTo" + name + " => . ... </k>")
- print("<OUTREG> M </OUTREG>")
- print("<" + name + "> _ => M </" + name + ">")
-
-
-print("require \"decoder-syntax.k\"")
-print("module GENERATED-DECODER-RULES")
-print("imports DOMAINS")
-print("imports COLLECTIONS")
-print("imports DECODER-SYNTAX")
-print("imports DECODER-CONFIGURATION")
-print("syntax K ::= \"DecoderError\"")
-print("syntax K ::= \"ScanForDisp\"")
-print("syntax K ::= \"ScanForImmediate\"")
-print('syntax OperandVisibility ::= "SUPPRESSED" | "IMPLICIT" | "EXPLICIT"')
-print('syntax OperandWidth ::= Int | "AUTO" | "VECTOR" | "SSZ" | "ASZ"') # Explicit bit count, AUTO for register arguments whose width is inferred from its value, and VECTOR for NELEM*ELEMSIZE
-print('syntax KResult ::= OperandWidth')
-print("syntax KItem ::= OperandMetadata(KItem, Bool, OperandVisibility, KItem, OperandWidth, OperandWidth, OperandWidth)") # Name, IsWriteMask, Visibility, C-Type, Wdith16, Width32, Width64
-
-outregs_done = set()
-for name in nonterminals.nonterminals_map:
- for alternative in nonterminals.nonterminals_map[name]:
- for assign in alternative.consequent.get(nonterminals.ComplexAssignment.__name__, []):
- if assign.name != "OUTREG" and assign.name not in outregs_done:
- print_outreg_to(assign.name)
- outregs_done.add(assign.name)
-
-attributes_done = set()
-operand_metadata_ids = set()
-operand_sort_set = set()
-for inst in instructions.instruction_list:
- for operand in inst.operands:
- assign = operand[0]
- if assign.__class__.__name__ == "ComplexAssignment" and assign.name not in outregs_done:
- print_outreg_to(assign.name)
- outregs_done.add(assign.name)
- attributes_done |= set(inst.attributes)
- operand_metadata_ids |= set([id_ for (_, id_, _, _, _, _, _, _) in inst.operands])
- operand_sort_set |= set([sort for (_, _, _, _, sort, _, _, _) in inst.operands])
-
-print("syntax KItem ::= " + " | ".join(['"A_{0}"'.format(attribute) for attribute in attributes_done]))
-print("syntax KItem ::= " + " | ".join(['"{0}"'.format(id_) for id_ in operand_metadata_ids]))
-print("syntax KItem ::= " + " | ".join(['"{0}"'.format(sort) for sort in operand_sort_set]))
-
-
-print("syntax K ::= \"Instruction\"")
-iclasses = list(set(["\"{0}\"".format(inst.iclass) for inst in instructions.instruction_list]))
-print("syntax IClass ::= " + " | ".join(iclasses))
-
-desired = set([n.upper() for n in sys.argv[1:]])
-
-for inst in instructions.instruction_list:
- if len(desired) == 0 or inst.iclass in desired:
- print("// UNAME: " + inst.uname)
- print(gen_from_inst(inst).generate_rule().replace("XED_", ""))
-
-for name in nonterminals.nonterminals_map:
- if "SPLITTER" in name or "PREFIX" in name:
- continue
- print("syntax K ::= \"" + name + "\"")
- for alternative in nonterminals.nonterminals_map[name]:
- print(gen_from_nonterminal(alternative).generate_rule().replace("XED_", ""))
-
-print("endmodule")
diff --git a/test-decoder.k b/test-decoder.k
new file mode 100644
index 0000000..4f60c32
--- /dev/null
+++ b/test-decoder.k
@@ -0,0 +1,57 @@
+/*BEGIN_LEGAL
+ *
+ * Adapted from Intel's XED (Copyright (c) 2018 Intel Corporation)
+ *
+ * END_LEGAL */
+
+require "decoder.k"
+
+module TEST-DECODER-SYNTAX
+ imports DOMAINS-SYNTAX
+
+ syntax HexToken ::= r"0x[0-9a-fA-F]+" [token, prec(2)]
+
+ syntax Stmt ::= "Disassemble" "(" HexToken "," HexToken ")"
+ syntax Stmts ::= List{Stmt, ";"}
+
+ syntax Pgm ::= Stmts ";"
+endmodule
+
+module TEST-DECODER-CONVERSIONS
+ imports DECODER-INTERFACE
+ imports DOMAINS
+
+ syntax HexTokens ::= List{HexToken, " "}
+
+ syntax Int ::= HexStringToInt(String) [function]
+ rule HexStringToInt(S:String) => String2Base(S, 16)
+
+ syntax String ::= StringifyHexToken(HexToken) [function, hook(STRING.token2string)]
+
+ syntax String ::= removeFirstTwoChars(String) [function]
+ rule removeFirstTwoChars(S) => substrString(S, 2, lengthString(S))
+
+ syntax String ::= HexTokenToString(HexToken) [function]
+ rule HexTokenToString(H) => removeFirstTwoChars(StringifyHexToken(H))
+
+ syntax Ints ::= HexTokenToInts(HexToken) [function]
+ syntax Ints ::= ImplHexTokenToInts(String) [function]
+
+ rule HexTokenToInts(Ht) => ImplHexTokenToInts(HexTokenToString(Ht))
+
+ rule ImplHexTokenToInts("") => .Ints
+ rule ImplHexTokenToInts(S) => String2Base(substrString(S, 0, 2), 16) ImplHexTokenToInts(substrString(S, 2, lengthString(S))) requires 2 dividesInt lengthString(S) andBool lengthString(S) >Int 0
+
+ syntax Int ::= HexTokenToInt(HexToken) [function]
+ rule HexTokenToInt(H) => HexStringToInt(HexTokenToString(H))
+
+ syntax KResult ::= HexToken
+endmodule
+
+module TEST-DECODER
+ imports TEST-DECODER-SYNTAX
+ imports TEST-DECODER-CONVERSIONS
+
+ configuration <k> $PGM:Pgm </k>
+ <decoder/>
+endmodule
--
GitLab