sdasgup3/binary-decompilation#77: wip

sdasgup3 · Jun 6, 2018 · f39cf2a · f39cf2a
1 parent c3d0959
commit f39cf2a
Show file tree

Hide file tree

Showing 197 changed files with 437 additions and 437 deletions.
diff --git a/concrete_instances/immediate-variants/btcl_r32_imm8/btcl_r32_imm8.k.format b/concrete_instances/immediate-variants/btcl_r32_imm8/btcl_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: btcl $0x0, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), xorMInt( extractMInt( %rbx, 32, 64), shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31))))))))
+%rbx   : concatenateMInt( mi(32, 0), xorMInt( extractMInt( %rbx, 32, 64), shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31)))))), 31, 32)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btcq_r64_imm8/btcq_r64_imm8.k.format b/concrete_instances/immediate-variants/btcq_r64_imm8/btcq_r64_imm8.k.format
@@ -10,7 +10,7 @@ code: btcq $0x0, %rbx
 
 Formula:
 
-%rbx   : xorMInt( %rbx, shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))))
+%rbx   : xorMInt( %rbx, shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))))
 
 %cf    : extractMInt( lshrMInt( %rbx, uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))), 63, 64)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btcw_r16_imm8/btcw_r16_imm8.k.format b/concrete_instances/immediate-variants/btcw_r16_imm8/btcw_r16_imm8.k.format
@@ -10,7 +10,7 @@ code: btcw $0x0, %bx
 
 Formula:
 
-%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), xorMInt( extractMInt( %rbx, 48, 64), shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15))))))))
+%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), xorMInt( extractMInt( %rbx, 48, 64), shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15)))))), 15, 16)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btrl_r32_imm8/btrl_r32_imm8.k.format b/concrete_instances/immediate-variants/btrl_r32_imm8/btrl_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: btrl $0x0, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), andMInt( extractMInt( %rbx, 32, 64), negMInt( shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31)))))))))
+%rbx   : concatenateMInt( mi(32, 0), andMInt( extractMInt( %rbx, 32, 64), negMInt( shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31)))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31)))))), 31, 32)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btrq_r64_imm8/btrq_r64_imm8.k.format b/concrete_instances/immediate-variants/btrq_r64_imm8/btrq_r64_imm8.k.format
@@ -10,7 +10,7 @@ code: btrq $0x0, %rbx
 
 Formula:
 
-%rbx   : andMInt( %rbx, negMInt( shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63))))))))
+%rbx   : andMInt( %rbx, negMInt( shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63))))))))
 
 %cf    : extractMInt( lshrMInt( %rbx, uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))), 63, 64)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btrw_r16_imm8/btrw_r16_imm8.k.format b/concrete_instances/immediate-variants/btrw_r16_imm8/btrw_r16_imm8.k.format
@@ -10,7 +10,7 @@ code: btrw $0x0, %bx
 
 Formula:
 
-%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), andMInt( extractMInt( %rbx, 48, 64), negMInt( shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15)))))))))
+%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), andMInt( extractMInt( %rbx, 48, 64), negMInt( shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15)))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15)))))), 15, 16)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btsl_r32_imm8/btsl_r32_imm8.k.format b/concrete_instances/immediate-variants/btsl_r32_imm8/btsl_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: btsl $0x0, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), orMInt( extractMInt( %rbx, 32, 64), shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31))))))))
+%rbx   : concatenateMInt( mi(32, 0), orMInt( extractMInt( %rbx, 32, 64), shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( Imm8, mi(8, 31)))))), 31, 32)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btsq_r64_imm8/btsq_r64_imm8.k.format b/concrete_instances/immediate-variants/btsq_r64_imm8/btsq_r64_imm8.k.format
@@ -10,7 +10,7 @@ code: btsq $0x0, %rbx
 
 Formula:
 
-%rbx   : orMInt( %rbx, shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))))
+%rbx   : orMInt( %rbx, shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))))
 
 %cf    : extractMInt( lshrMInt( %rbx, uvalueMInt(mi(64, svalueMInt(andMInt( Imm8, mi(8, 63)))))), 63, 64)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/btsw_r16_imm8/btsw_r16_imm8.k.format b/concrete_instances/immediate-variants/btsw_r16_imm8/btsw_r16_imm8.k.format
@@ -10,7 +10,7 @@ code: btsw $0x0, %bx
 
 Formula:
 
-%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), orMInt( extractMInt( %rbx, 48, 64), shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15))))))))
+%rbx   : concatenateMInt( extractMInt( %rbx, 0, 48), orMInt( extractMInt( %rbx, 48, 64), shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15))))))))
 
 %cf    : extractMInt( lshrMInt( extractMInt( %rbx, 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( Imm8, mi(8, 15)))))), 15, 16)
 %pf    : (#ifMInt TMP_BOOL_3 #then mi(1, 1) #else mi(1, 0) #fi)

diff --git a/concrete_instances/immediate-variants/extractps_r32_xmm_imm8/extractps_r32_xmm_imm8.k.format b/concrete_instances/immediate-variants/extractps_r32_xmm_imm8/extractps_r32_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: extractps $0x0, %xmm1, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
+%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/extractps_r64_xmm_imm8/extractps_r64_xmm_imm8.k.format b/concrete_instances/immediate-variants/extractps_r64_xmm_imm8/extractps_r64_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: extractps $0x0, %xmm1, %rbx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
+%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/palignr_xmm_xmm_imm8/palignr_xmm_xmm_imm8.k.format b/concrete_instances/immediate-variants/palignr_xmm_xmm_imm8/palignr_xmm_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: palignr $0x0, %xmm2, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), extractMInt( lshrMInt( concatenateMInt( extractMInt( %ymm1, 128, 256), extractMInt( %ymm2, 128, 256)), uvalueMInt(shlMInt( concatenateMInt( mi(248, 0), Imm8), uvalueMInt(mi(256, 3))))), 128, 256))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), extractMInt( lshrMInt( concatenateMInt( extractMInt( %ymm1, 128, 256), extractMInt( %ymm2, 128, 256)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(248, 0), Imm8), uvalueMInt(mi(256, 3))))), 128, 256))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrb_r32_xmm_imm8/pextrb_r32_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrb_r32_xmm_imm8/pextrb_r32_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrb $0x0, %xmm1, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
+%rbx   : concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrb_r64_xmm_imm8/pextrb_r64_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrb_r64_xmm_imm8/pextrb_r64_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrb $0x0, %xmm1, %rbx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
+%rbx   : concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrd_r32_xmm_imm8/pextrd_r32_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrd_r32_xmm_imm8/pextrd_r32_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrd $0x0, %xmm1, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
+%rbx   : concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrq_r64_xmm_imm8/pextrq_r64_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrq_r64_xmm_imm8/pextrq_r64_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrq $0x0, %xmm1, %rbx
 
 Formula:
 
-%rbx   : extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(127, 0), extractMInt( Imm8, 7, 8)), uvalueMInt(mi(128, 6))))), 64, 128)
+%rbx   : extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(127, 0), extractMInt( Imm8, 7, 8)), uvalueMInt(mi(128, 6))))), 64, 128)
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrw_r32_xmm_imm8/pextrw_r32_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrw_r32_xmm_imm8/pextrw_r32_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrw $0x0, %xmm1, %ebx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
+%rbx   : concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pextrw_r64_xmm_imm8/pextrw_r64_xmm_imm8.k.format b/concrete_instances/immediate-variants/pextrw_r64_xmm_imm8/pextrw_r64_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pextrw $0x0, %xmm1, %rbx
 
 Formula:
 
-%rbx   : concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
+%rbx   : concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pinsrb_xmm_r32_imm8/pinsrb_xmm_r32_imm8.k.format b/concrete_instances/immediate-variants/pinsrb_xmm_r32_imm8/pinsrb_xmm_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: pinsrb $0x0, %ebx, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shlMInt( mi(128, 255), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), shlMInt( mi(128, 255), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shiftLeftMInt( mi(128, 255), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))), shiftLeftMInt( mi(128, 255), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( Imm8, 4, 8)), uvalueMInt(mi(128, 3))))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pinsrd_xmm_r32_imm8/pinsrd_xmm_r32_imm8.k.format b/concrete_instances/immediate-variants/pinsrd_xmm_r32_imm8/pinsrd_xmm_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: pinsrd $0x0, %ebx, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shlMInt( mi(128, 4294967295), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), shlMInt( mi(128, 4294967295), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shiftLeftMInt( mi(128, 4294967295), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), shiftLeftMInt( mi(128, 4294967295), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pinsrw_xmm_r32_imm8/pinsrw_xmm_r32_imm8.k.format b/concrete_instances/immediate-variants/pinsrw_xmm_r32_imm8/pinsrw_xmm_r32_imm8.k.format
@@ -10,7 +10,7 @@ code: pinsrw $0x0, %ebx, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shlMInt( mi(128, 65535), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), shlMInt( mi(128, 65535), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), orMInt( andMInt( extractMInt( %ymm1, 128, 256), negMInt( shiftLeftMInt( mi(128, 65535), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( %rbx, 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))), shiftLeftMInt( mi(128, 65535), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( Imm8, 5, 8)), uvalueMInt(mi(128, 4))))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pshufd_xmm_xmm_imm8/pshufd_xmm_xmm_imm8.k.format b/concrete_instances/immediate-variants/pshufd_xmm_xmm_imm8/pshufd_xmm_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pshufd $0x0, %xmm2, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 5))))), 96, 128), extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128)))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 5))))), 96, 128), extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128)))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pshufhw_xmm_xmm_imm8/pshufhw_xmm_xmm_imm8.k.format b/concrete_instances/immediate-variants/pshufhw_xmm_xmm_imm8/pshufhw_xmm_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pshufhw $0x0, %xmm2, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 4))))), 48, 64), extractMInt( %ymm2, 192, 256))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 4))))), 48, 64), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 4))))), 48, 64), extractMInt( %ymm2, 192, 256))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pshuflw_xmm_xmm_imm8/pshuflw_xmm_xmm_imm8.k.format b/concrete_instances/immediate-variants/pshuflw_xmm_xmm_imm8/pshuflw_xmm_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pshuflw $0x0, %xmm2, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( %ymm2, 128, 192), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 4))))), 112, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 4))))), 112, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 4))))), 112, 128), extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 4))))), 112, 128))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), concatenateMInt( extractMInt( %ymm2, 128, 192), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 0, 2)), uvalueMInt(mi(128, 4))))), 112, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 2, 4)), uvalueMInt(mi(128, 4))))), 112, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 4, 6)), uvalueMInt(mi(128, 4))))), 112, 128), extractMInt( lshrMInt( extractMInt( %ymm2, 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( Imm8, 6, 8)), uvalueMInt(mi(128, 4))))), 112, 128))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pslld_xmm_imm8/pslld_xmm_imm8.k.format b/concrete_instances/immediate-variants/pslld_xmm_imm8/pslld_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pslld $0x0, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), (#ifMInt ugtMInt( concatenateMInt( mi(56, 0), Imm8), mi(64, 31)) #then mi(128, 0) #else concatenateMInt( shlMInt( extractMInt( %ymm1, 128, 160), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), concatenateMInt( shlMInt( extractMInt( %ymm1, 160, 192), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), concatenateMInt( shlMInt( extractMInt( %ymm1, 192, 224), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), shlMInt( extractMInt( %ymm1, 224, 256), uvalueMInt(concatenateMInt( mi(24, 0), Imm8)))))) #fi))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), (#ifMInt ugtMInt( concatenateMInt( mi(56, 0), Imm8), mi(64, 31)) #then mi(128, 0) #else concatenateMInt( shiftLeftMInt( extractMInt( %ymm1, 128, 160), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), concatenateMInt( shiftLeftMInt( extractMInt( %ymm1, 160, 192), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), concatenateMInt( shiftLeftMInt( extractMInt( %ymm1, 192, 224), uvalueMInt(concatenateMInt( mi(24, 0), Imm8))), shiftLeftMInt( extractMInt( %ymm1, 224, 256), uvalueMInt(concatenateMInt( mi(24, 0), Imm8)))))) #fi))
 
 sigfpe  : sigfpe
 sigbus  : sigbus

diff --git a/concrete_instances/immediate-variants/pslldq_xmm_imm8/pslldq_xmm_imm8.k.format b/concrete_instances/immediate-variants/pslldq_xmm_imm8/pslldq_xmm_imm8.k.format
@@ -10,7 +10,7 @@ code: pslldq $0x0, %xmm1
 
 Formula:
 
-%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), shlMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shlMInt( (#ifMInt ugtMInt( Imm8, mi(8, 15)) #then concatenateMInt( mi(120, 0), mi(8, 16)) #else concatenateMInt( mi(120, 0), Imm8) #fi), uvalueMInt(mi(128, 3))))))
+%ymm1  : concatenateMInt( extractMInt( %ymm1, 0, 128), shiftLeftMInt( extractMInt( %ymm1, 128, 256), uvalueMInt(shiftLeftMInt( (#ifMInt ugtMInt( Imm8, mi(8, 15)) #then concatenateMInt( mi(120, 0), mi(8, 16)) #else concatenateMInt( mi(120, 0), Imm8) #fi), uvalueMInt(mi(128, 3))))))
 
 sigfpe  : sigfpe
 sigbus  : sigbus