sdasgup3/binary-decompilation#77: wip

kframework · Jul 1, 2018 · 0124ed3 · 0124ed3
1 parent 125d3d2
commit 0124ed3
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 0 deletions.
diff --git a/semantics/specialInstructions/movl_r32_label.k b/semantics/specialInstructions/movl_r32_label.k
@@ -0,0 +1,15 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module MOVL-R32-LABEL
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (movl $ LabelId:X86Id, R2:R32,  .Operands) => 
+      execinstr (movl $ uvalueMInt(Target), R2:R32,  .Operands)
+  ...</k>
+      <functargets>... LabelId |-> Target:MInt  ...</functargets>
+
+endmodule
+
+
diff --git a/semantics/specialInstructions/movq_m64_label.k b/semantics/specialInstructions/movq_m64_label.k
@@ -0,0 +1,14 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module MOVQ-M64-IMM32
+  imports X86-CONFIGURATION
+
+  context execinstr(movq:Opcode $ LabelId:X86Id, HOLE:Mem,  .Operands) [result(MemOffset)]
+
+  rule <k>
+     execinstr (movq:Opcode $ LabelId:X86Id, memOffset( MemOff:MInt):MemOffset,  .Operands) =>
+      execinstr (movq $ uvalueMInt(Target), memOffset( MemOff),  .Operands)
+  ...</k>
+      <functargets>... LabelId |-> Target:MInt  ...</functargets>
+endmodule