Skip to content

Commit

Permalink
#77: wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@sdasgup3
sdasgup3 committed Jun 6, 2018
1 parent f7827be commit 8c55cd1
Show file tree
Hide file tree
Showing 264 changed files with 667 additions and 645 deletions.
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btcl_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTCL-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), xorMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31))))))))
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), xorMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31)))))), 31, 32)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btcq_r64_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTCQ-R64-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> xorMInt( getParentValue(R2, RSMap), shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))))
convToRegKeys(R2) |-> xorMInt( getParentValue(R2, RSMap), shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))))

"CF" |-> extractMInt( lshrMInt( getParentValue(R2, RSMap), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))), 63, 64)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btcw_r16_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTCW-R16-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), xorMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15))))))))
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), xorMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15)))))), 15, 16)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btrl_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTRL-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), andMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), negMInt( shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31)))))))))
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), andMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), negMInt( shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31)))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31)))))), 31, 32)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btrq_r64_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTRQ-R64-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> andMInt( getParentValue(R2, RSMap), negMInt( shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63))))))))
convToRegKeys(R2) |-> andMInt( getParentValue(R2, RSMap), negMInt( shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63))))))))

"CF" |-> extractMInt( lshrMInt( getParentValue(R2, RSMap), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))), 63, 64)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btrw_r16_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTRW-R16-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), andMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), negMInt( shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15)))))))))
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), andMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), negMInt( shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15)))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15)))))), 15, 16)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btsl_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTSL-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), orMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), shlMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31))))))))
convToRegKeys(R2) |-> concatenateMInt( mi(32, 0), orMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), shiftLeftMInt( mi(32, 1), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 32, 64), uvalueMInt(mi(32, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 31)))))), 31, 32)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btsq_r64_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTSQ-R64-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> orMInt( getParentValue(R2, RSMap), shlMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))))
convToRegKeys(R2) |-> orMInt( getParentValue(R2, RSMap), shiftLeftMInt( mi(64, 1), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))))

"CF" |-> extractMInt( lshrMInt( getParentValue(R2, RSMap), uvalueMInt(mi(64, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 63)))))), 63, 64)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/btsw_r16_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module BTSW-R16-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), orMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), shlMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15))))))))
convToRegKeys(R2) |-> concatenateMInt( extractMInt( getParentValue(R2, RSMap), 0, 48), orMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), shiftLeftMInt( mi(16, 1), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15))))))))

"CF" |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 48, 64), uvalueMInt(mi(16, svalueMInt(andMInt( handleImmediateWithSignExtend(Imm8, 8, 8), mi(8, 15)))))), 15, 16)

Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/extractps_r32_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module EXTRACTPS-R32-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/extractps_r64_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module EXTRACTPS-R64-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/palignr_xmm_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PALIGNR-XMM-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), extractMInt( lshrMInt( concatenateMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), extractMInt( getParentValue(R2, RSMap), 128, 256)), uvalueMInt(shlMInt( concatenateMInt( mi(248, 0), handleImmediateWithSignExtend(Imm8, 8, 8)), uvalueMInt(mi(256, 3))))), 128, 256))
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), extractMInt( lshrMInt( concatenateMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), extractMInt( getParentValue(R2, RSMap), 128, 256)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(248, 0), handleImmediateWithSignExtend(Imm8, 8, 8)), uvalueMInt(mi(256, 3))))), 128, 256))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrb_r32_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRB-R32-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrb_r64_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRB-R64-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(56, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), 120, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrd_r32_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRD-R32-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(32, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrq_r64_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRQ-R64-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(127, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 7, 8)), uvalueMInt(mi(128, 6))))), 64, 128)
convToRegKeys(R3) |-> extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(127, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 7, 8)), uvalueMInt(mi(128, 6))))), 64, 128)
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrw_r32_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRW-R32-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pextrw_r64_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PEXTRW-R64-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
convToRegKeys(R3) |-> concatenateMInt( mi(48, 0), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), 112, 128))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pinsrb_xmm_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PINSRB-XMM-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shlMInt( mi(128, 255), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), shlMInt( mi(128, 255), uvalueMInt(shlMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))))))
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shiftLeftMInt( mi(128, 255), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))), shiftLeftMInt( mi(128, 255), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(124, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 8)), uvalueMInt(mi(128, 3))))))))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pinsrd_xmm_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PINSRD-XMM-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shlMInt( mi(128, 4294967295), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), shlMInt( mi(128, 4294967295), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))))))
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shiftLeftMInt( mi(128, 4294967295), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), shiftLeftMInt( mi(128, 4294967295), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))))))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pinsrw_xmm_r32_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PINSRW-XMM-R32-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shlMInt( mi(128, 65535), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))))), andMInt( shlMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), shlMInt( mi(128, 65535), uvalueMInt(shlMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))))))
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), orMInt( andMInt( extractMInt( getParentValue(R3, RSMap), 128, 256), negMInt( shiftLeftMInt( mi(128, 65535), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))))), andMInt( shiftLeftMInt( concatenateMInt( mi(96, 0), extractMInt( getParentValue(R2, RSMap), 32, 64)), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))), shiftLeftMInt( mi(128, 65535), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(125, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 5, 8)), uvalueMInt(mi(128, 4))))))))
)

</regstate>
Expand Down
2 changes: 1 addition & 1 deletion x86-semantics/semantics/immediateInstructions/pshufd_xmm_xmm_imm8.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module PSHUFD-XMM-XMM-IMM8
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 0, 2)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 2, 4)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 6)), uvalueMInt(mi(128, 5))))), 96, 128), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shlMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128)))))
convToRegKeys(R3) |-> concatenateMInt( extractMInt( getParentValue(R3, RSMap), 0, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 0, 2)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 2, 4)), uvalueMInt(mi(128, 5))))), 96, 128), concatenateMInt( extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 4, 6)), uvalueMInt(mi(128, 5))))), 96, 128), extractMInt( lshrMInt( extractMInt( getParentValue(R2, RSMap), 128, 256), uvalueMInt(shiftLeftMInt( concatenateMInt( mi(126, 0), extractMInt( handleImmediateWithSignExtend(Imm8, 8, 8), 6, 8)), uvalueMInt(mi(128, 5))))), 96, 128)))))
)

</regstate>
Expand Down
Loading

0 comments on commit 8c55cd1

Please sign in to comment.