https://github.com/sdasgup3/binary-decompilation/issues/77

kframework · Jun 29, 2018 · 812c64e · 812c64e
1 parent c255063
commit 812c64e
Show file tree

Hide file tree

Showing 13 changed files with 157 additions and 0 deletions.
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovbe_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovbe_r32_r32.k
@@ -0,0 +1,11 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVBE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovbe R1:R32, R2:R32,  .Operands) => execinstr (cmovbel R1:R32, R2:R32,  .Operands)
+  ...</k>
+
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/cmove_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmove_r32_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmove R1:R32, R2:R32,  .Operands) => execinstr (cmovel R1:R32, R2:R32,  .Operands)
+  ...</k>
+
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovge_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovge_r32_r32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVGE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovge R1:R32, R2:R32,  .Operands) => execinstr (cmovgel R1:R32, R2:R32,  .Operands)
+  ...</k>
+
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovle_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovle_r32_r32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVLE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovle R1:R32, R2:R32,  .Operands) => execinstr (cmovlel R1:R32, R2:R32,  .Operands)
+  ...</k>
+
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovs_r64_r64.k b/tests/gcc.c-torture/instruction_semantics/cmovs_r64_r64.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVS-R64-R64
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovs R1:R64, R2:R64,  .Operands) => execinstr (cmovsq R1:R64, R2:R64,  .Operands)
+  ...</k>
+
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/roll_m32.k b/tests/gcc.c-torture/instruction_semantics/roll_m32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module ROLL-M32
+  imports X86-CONFIGURATION
+
+  context execinstr(roll:Opcode HOLE:Mem,  .Operands) [result(MemOffset)]
+
+  rule <k>
+    execinstr (roll:Opcode  memOffset( MemOff:MInt):MemOffset,  .Operands) => execinstr (roll:Opcode $0x1, memOffset( MemOff:MInt):MemOffset,  .Operands)
+  ...</k>
+
+ endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/sarb_r8.k b/tests/gcc.c-torture/instruction_semantics/sarb_r8.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARB-R8
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarb  R2:R8,  .Operands) => execinstr (sarb $0x1, R2:R8,  .Operands) 
+  ...</k>
+
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/sarl_m32.k b/tests/gcc.c-torture/instruction_semantics/sarl_m32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARL-M32
+  imports X86-CONFIGURATION
+
+  context execinstr(sarl:Opcode HOLE:Mem,  .Operands) [result(MemOffset)]
+
+  rule <k>
+    execinstr (sarl:Opcode memOffset( MemOff:MInt):MemOffset,  .Operands) => execinstr (sarl $0x1, memOffset( MemOff),  .Operands)
+  ...</k>
+
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/sarw_r16.k b/tests/gcc.c-torture/instruction_semantics/sarw_r16.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARW-R16
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarw  R2:R16,  .Operands) => execinstr (sarw $0x1, R2:R16,  .Operands) 
+  ...</k>
+   endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/sarx_r32_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/sarx_r32_r32_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARX-R32-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarx R1:R32, R2:R32, R3:R32,  .Operands) => execinstr (sarxl R1, R2, R3,  .Operands)
+  ...</k>
+
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/shrl_r32.k b/tests/gcc.c-torture/instruction_semantics/shrl_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRL-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrl R2:R32,  .Operands) => execinstr (shrl $0x1, R2:R32,  .Operands)
+  ...</k>
+  endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/shrq_r64.k b/tests/gcc.c-torture/instruction_semantics/shrq_r64.k
@@ -0,0 +1,10 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRQ-R64
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrq R2:R64,  .Operands) => execinstr (shrq $0x1, R2:R64,  .Operands)
+  ...</k>
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/shrx_r32_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/shrx_r32_r32_r32.k
@@ -0,0 +1,11 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRX-R32-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrx R1:R32, R2:R32, R3:R32,  .Operands) => execinstr (shrxl R1:R32, R2:R32, R3:R32,  .Operands)
+  ...</k>
+   endmodule
+