Skip to content

Fixed the assembly names of some instructions which produces ambiguous disassembly. #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Fixed the assembly names of some instructions which produces ambiguous disassembly. #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
51b248c
Fixed the assembly names of some instructions which produces
sdasgup3 Jan 31, 2019
07c5c3c
Merge branch 'master' into disambiguate_mnemonic_names
Andrew-Miranti Feb 2, 2019
7532c1d
Fix some missing opcodes
Andrew-Miranti Feb 3, 2019
956e1df
Make opcodes tokens
Andrew-Miranti Feb 4, 2019
df47ed7
Merge conflict resolve
Andrew-Miranti Feb 4, 2019
c43b75f
Changes to make decoder compile
Andrew-Miranti Feb 6, 2019
9b8787e
Minor syntax updates because I was getting strange kompile errors
Andrew-Miranti Feb 12, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion semantics/common/library/common-c-library-configuration.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ module COMMON-C-LIBRARY-CONFIGURATION
<open-files> .Set </open-files>

<files>
<file multiplicity="*">
<file multiplicity="*" type="Map">
<fid> .K </fid>
<uri> .K </uri>
<pos> 0 </pos>
Expand Down
4 changes: 1 addition & 3 deletions semantics/common/library/common-c-library-stdlib.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,7 @@ module COMMON-C-LIBRARY-STDLIB

rule stdlib_exit(I::Int) => exitExecution(I)

rule stdlib_abort ~> _
=>
writeFD(#stdout, "Aborted\n") ~> flush(#stdout) ~> asCInt(134)
rule <k> stdlib_abort ~> _ => writeFD(#stdout, "Aborted\n") ~> flush(#stdout) ~> asCInt(134) </k>

rule <k> stdlib_atexit(FP::VoidFunctionPointer) => success ...</k>
<atexit> (.K => callExitHandler(FP)) ...</atexit>
Expand Down
10 changes: 5 additions & 5 deletions ...memoryInstructions/vpinsrq_xmm_m64_imm8.k → .../memoryInstructions/pinsrq_xmm_m64_imm8.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VPINSRQ-XMM-M64-IMM8
module PINSRQ-XMM-M64-IMM8
imports X86-CONFIGURATION

context execinstr(vpinsrq:Opcode Imm8:Imm, HOLE:Mem, R3:Xmm, R4:Xmm, .Operands) [result(MemOffset)]
context execinstr(pinsrq:Opcode Imm8:Imm, HOLE:Mem, R3:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vpinsrq:Opcode Imm8:Imm, memOffset( MemOff:MInt):MemOffset, R3:Xmm, .Operands) =>
execinstr (pinsrq:Opcode Imm8:Imm, memOffset( MemOff:MInt):MemOffset, R3:Xmm, .Operands) =>
loadFromMemory( MemOff, 64) ~>
execinstr (vpinsrq Imm8, memOffset( MemOff), R3:Xmm, .Operands)
execinstr (pinsrq Imm8, memOffset( MemOff), R3:Xmm, .Operands)
...</k>
<regstate> RSMap:Map </regstate>

rule <k>
memLoadValue(Mem64:MInt):MemLoadValue ~> execinstr (vpinsrq:Opcode Imm8:Imm, memOffset( MemOff:MInt):MemOffset, R3:Xmm, .Operands) =>
memLoadValue(Mem64:MInt):MemLoadValue ~> execinstr (pinsrq:Opcode Imm8:Imm, memOffset( MemOff:MInt):MemOffset, R3:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
8 changes: 4 additions & 4 deletions ...s/memoryInstructions/vcvtpd2dq_xmm_m256.k → .../memoryInstructions/vcvtpd2dqy_xmm_m256.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,17 @@ requires "x86-configuration.k"
module VCVTPD2DQ-XMM-M256
imports X86-CONFIGURATION

context execinstr(vcvtpd2dq:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]
context execinstr(vcvtpd2dqy:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vcvtpd2dq:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
execinstr (vcvtpd2dqy:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
loadFromMemory( MemOff, 256) ~>
execinstr (vcvtpd2dq memOffset( MemOff), R2:Xmm, .Operands)
execinstr (vcvtpd2dqy memOffset( MemOff), R2:Xmm, .Operands)
...</k>
<regstate> RSMap:Map </regstate>

rule <k>
memLoadValue(Mem256:MInt):MemLoadValue ~> execinstr (vcvtpd2dq:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
memLoadValue(Mem256:MInt):MemLoadValue ~> execinstr (vcvtpd2dqy:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
10 changes: 5 additions & 5 deletions ...s/memoryInstructions/vcvtpd2ps_xmm_m128.k → .../memoryInstructions/vcvtpd2psx_xmm_m128.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VCVTPD2PS-XMM-M128
module VCVTPD2PSX-XMM-M128
imports X86-CONFIGURATION

context execinstr(vcvtpd2ps:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]
context execinstr(vcvtpd2psx:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vcvtpd2ps:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
execinstr (vcvtpd2psx:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
loadFromMemory( MemOff, 128) ~>
execinstr (vcvtpd2ps memOffset( MemOff), R2:Xmm, .Operands)
execinstr (vcvtpd2psx memOffset( MemOff), R2:Xmm, .Operands)
...</k>
<regstate> RSMap:Map </regstate>

rule <k>
memLoadValue(Mem128:MInt):MemLoadValue ~> execinstr (vcvtpd2ps:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
memLoadValue(Mem128:MInt):MemLoadValue ~> execinstr (vcvtpd2psx:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
6 changes: 3 additions & 3 deletions ...s/memoryInstructions/vcvtpd2ps_xmm_m256.k → .../memoryInstructions/vcvtpd2psy_xmm_m256.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VCVTPD2PS-XMM-M256
module VCVTPD2PSY-XMM-M256
imports X86-CONFIGURATION

context execinstr(vcvtpd2ps:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]
context execinstr(vcvtpd2psy:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vcvtpd2ps:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
execinstr (vcvtpd2psy:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
10 changes: 5 additions & 5 deletions .../memoryInstructions/vcvttpd2dq_xmm_m128.k → ...memoryInstructions/vcvttpd2dqx_xmm_m128.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VCVTTPD2DQ-XMM-M128
module VCVTTPD2DQX-XMM-M128
imports X86-CONFIGURATION

context execinstr(vcvttpd2dq:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]
context execinstr(vcvttpd2dqx:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vcvttpd2dq:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
execinstr (vcvttpd2dqx:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
loadFromMemory( MemOff, 128) ~>
execinstr (vcvttpd2dq memOffset( MemOff), R2:Xmm, .Operands)
execinstr (vcvttpd2dqx memOffset( MemOff), R2:Xmm, .Operands)
...</k>
<regstate> RSMap:Map </regstate>

rule <k>
memLoadValue(Mem128:MInt):MemLoadValue ~> execinstr (vcvttpd2dq:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
memLoadValue(Mem128:MInt):MemLoadValue ~> execinstr (vcvttpd2dqx:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
6 changes: 3 additions & 3 deletions .../memoryInstructions/vcvttpd2dq_xmm_m256.k → ...memoryInstructions/vcvttpd2dqy_xmm_m256.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VCVTTPD2DQ-XMM-M256
module VCVTTPD2DQY-XMM-M256
imports X86-CONFIGURATION

context execinstr(vcvttpd2dq:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]
context execinstr(vcvttpd2dqy:Opcode HOLE:Mem, R2:Xmm, .Operands) [result(MemOffset)]

rule <k>
execinstr (vcvttpd2dq:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
execinstr (vcvttpd2dqy:Opcode memOffset( MemOff:MInt):MemOffset, R2:Xmm, .Operands) =>
.
...</k>
<regstate>
Expand Down
4 changes: 2 additions & 2 deletions .../registerInstructions/vcvtdq2pd_ymm_ymm.k → .../registerInstructions/vcvtdq2pd_ymm_xmm.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
// Autogenerated using stratification.
requires "x86-configuration.k"

module VCVTDQ2PD-YMM-YMM
module VCVTDQ2PD-YMM-XMM
imports X86-CONFIGURATION

rule <k>
execinstr (vcvtdq2pd R1:Ymm, R2:Ymm, .Operands) => .
execinstr (vcvtdq2pd R1:Xmm, R2:Ymm, .Operands) => .
...</k>
<regstate>
RSMap:Map => updateMap(RSMap,
Expand Down
Loading