Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
G
gdsl-toolkit
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Packages
Packages
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Lovis J.I. Zenz
gdsl-toolkit
Commits
97512701
Commit
97512701
authored
Sep 20, 2013
by
Julian Kranz
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
RReil: (Started to) move size from sem_arityX to sem_stmt
parent
91953857
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
76 additions
and
94 deletions
+76
-94
specifications/rreil/rreil-cif.ml
specifications/rreil/rreil-cif.ml
+22
-22
specifications/rreil/rreil-liveness.ml
specifications/rreil/rreil-liveness.ml
+3
-3
specifications/rreil/rreil-pretty.ml
specifications/rreil/rreil-pretty.ml
+9
-10
specifications/rreil/rreil.ml
specifications/rreil/rreil.ml
+37
-54
specifications/x86/x86-rreil-translator-m-z.ml
specifications/x86/x86-rreil-translator-m-z.ml
+2
-2
specifications/x86/x86-rreil-translator.ml
specifications/x86/x86-rreil-translator.ml
+3
-3
No files found.
specifications/rreil/rreil-cif.ml
View file @
97512701
...
...
@@ -86,28 +86,28 @@ val rreil-convert-sem-sexpr cbs sexpr = case sexpr of
end
val
rreil
-
convert
-
sem
-
op
-
cmp
cbs
op
-
cmp
=
case
op
-
cmp
of
SEM_CMPEQ
c
:
cbs
.
sem_op_cmp
.
sem_cmpeq
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPNEQ
c
:
cbs
.
sem_op_cmp
.
sem_cmpneq
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLES
c
:
cbs
.
sem_op_cmp
.
sem_cmples
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLEU
c
:
cbs
.
sem_op_cmp
.
sem_cmpleu
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLTS
c
:
cbs
.
sem_op_cmp
.
sem_cmplts
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLTU
c
:
cbs
.
sem_op_cmp
.
sem_cmpltu
c
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
SEM_CMPEQ
c
:
cbs
.
sem_op_cmp
.
sem_cmpeq
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPNEQ
c
:
cbs
.
sem_op_cmp
.
sem_cmpneq
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLES
c
:
cbs
.
sem_op_cmp
.
sem_cmples
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLEU
c
:
cbs
.
sem_op_cmp
.
sem_cmpleu
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLTS
c
:
cbs
.
sem_op_cmp
.
sem_cmplts
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
|
SEM_CMPLTU
c
:
cbs
.
sem_op_cmp
.
sem_cmpltu
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
c
.
opnd2
)
end
val
rreil
-
convert
-
sem
-
expr
cbs
op
=
case
op
of
SEM_SEXPR
s
:
cbs
.
sem_expr
.
sem_sexpr
s
.
size
(
rreil
-
convert
-
sem
-
sexpr
cbs
s
.
opnd1
)
|
SEM_MUL
m
:
cbs
.
sem_expr
.
sem_mul
m
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd2
)
|
SEM_DIV
d
:
cbs
.
sem_expr
.
sem_div
d
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd2
)
|
SEM_DIVS
d
:
cbs
.
sem_expr
.
sem_divs
d
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd2
)
|
SEM_MOD
m
:
cbs
.
sem_expr
.
sem_mod
m
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd2
)
|
SEM_SHL
s
:
cbs
.
sem_expr
.
sem_shl
s
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_SHR
s
:
cbs
.
sem_expr
.
sem_shr
s
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_SHRS
s
:
cbs
.
sem_expr
.
sem_shrs
s
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_AND
a
:
cbs
.
sem_expr
.
sem_and
a
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
a
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
a
.
opnd2
)
|
SEM_OR
o
:
cbs
.
sem_expr
.
sem_or
o
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
o
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
o
.
opnd2
)
|
SEM_XOR
x
:
cbs
.
sem_expr
.
sem_xor
x
.
size
(
rreil
-
convert
-
sem
-
linear
cbs
x
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
x
.
opnd2
)
|
SEM_SX
s
:
cbs
.
sem_expr
.
sem_sx
s
.
size
s
.
fromsize
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
|
SEM_ZX
s
:
cbs
.
sem_expr
.
sem_zx
s
.
size
s
.
fromsize
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
SEM_SEXPR
s
:
cbs
.
sem_expr
.
sem_sexpr
(
rreil
-
convert
-
sem
-
sexpr
cbs
s
)
|
SEM_MUL
m
:
cbs
.
sem_expr
.
sem_mul
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd2
)
|
SEM_DIV
d
:
cbs
.
sem_expr
.
sem_div
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd2
)
|
SEM_DIVS
d
:
cbs
.
sem_expr
.
sem_divs
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
d
.
opnd2
)
|
SEM_MOD
m
:
cbs
.
sem_expr
.
sem_mod
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
m
.
opnd2
)
|
SEM_SHL
s
:
cbs
.
sem_expr
.
sem_shl
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_SHR
s
:
cbs
.
sem_expr
.
sem_shr
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_SHRS
s
:
cbs
.
sem_expr
.
sem_shrs
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd2
)
|
SEM_AND
a
:
cbs
.
sem_expr
.
sem_and
(
rreil
-
convert
-
sem
-
linear
cbs
a
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
a
.
opnd2
)
|
SEM_OR
o
:
cbs
.
sem_expr
.
sem_or
(
rreil
-
convert
-
sem
-
linear
cbs
o
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
o
.
opnd2
)
|
SEM_XOR
x
:
cbs
.
sem_expr
.
sem_xor
(
rreil
-
convert
-
sem
-
linear
cbs
x
.
opnd1
)
(
rreil
-
convert
-
sem
-
linear
cbs
x
.
opnd2
)
|
SEM_SX
s
:
cbs
.
sem_expr
.
sem_sx
s
.
fromsize
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
|
SEM_ZX
s
:
cbs
.
sem_expr
.
sem_zx
s
.
fromsize
(
rreil
-
convert
-
sem
-
linear
cbs
s
.
opnd1
)
end
val
rreil
-
convert
-
branch
-
hint
cbs
hint
=
cbs
.
branch_hint
.
branch_hint_
(
index
hint
)
...
...
@@ -139,9 +139,9 @@ end
val
rreil
-
convert
-
sem
-
flop
cbs
flop
=
cbs
.
sem_flop
.
sem_flop_
(
index
flop
)
val
rreil
-
convert
-
sem
-
stmt
cbs
stmt
=
case
stmt
of
SEM_ASSIGN
s
:
cbs
.
sem_stmt
.
sem_assign
(
rreil
-
convert
-
sem
-
var
cbs
s
.
lhs
)
(
rreil
-
convert
-
sem
-
expr
cbs
s
.
rhs
)
|
SEM_LOAD
l
:
cbs
.
sem_stmt
.
sem_load
(
rreil
-
convert
-
sem
-
var
cbs
l
.
lhs
)
l
.
size
(
rreil
-
convert
-
sem
-
address
cbs
l
.
address
)
|
SEM_STORE
s
:
cbs
.
sem_stmt
.
sem_store
(
rreil
-
convert
-
sem
-
address
cbs
s
.
address
)
(
rreil
-
convert
-
sem
-
expr
cbs
s
.
rhs
)
SEM_ASSIGN
s
:
cbs
.
sem_stmt
.
sem_assign
s
.
size
(
rreil
-
convert
-
sem
-
var
cbs
s
.
lhs
)
(
rreil
-
convert
-
sem
-
expr
cbs
s
.
rhs
)
|
SEM_LOAD
l
:
cbs
.
sem_stmt
.
sem_load
l
.
size
(
rreil
-
convert
-
sem
-
var
cbs
l
.
lhs
)
l
.
size
(
rreil
-
convert
-
sem
-
address
cbs
l
.
address
)
|
SEM_STORE
s
:
cbs
.
sem_stmt
.
sem_store
s
.
size
(
rreil
-
convert
-
sem
-
address
cbs
s
.
address
)
(
rreil
-
convert
-
sem
-
expr
cbs
s
.
rhs
)
|
SEM_ITE
i
:
cbs
.
sem_stmt
.
sem_ite
(
rreil
-
convert
-
sem
-
sexpr
cbs
i
.
cond
)
(
rreil
-
convert
-
sem
-
stmts
cbs
i
.
then_branch
)
(
rreil
-
convert
-
sem
-
stmts
cbs
i
.
else_branch
)
|
SEM_WHILE
w
:
cbs
.
sem_stmt
.
sem_while
(
rreil
-
convert
-
sem
-
sexpr
cbs
w
.
cond
)
(
rreil
-
convert
-
sem
-
stmts
cbs
w
.
body
)
|
SEM_CBRANCH
c
:
cbs
.
sem_stmt
.
sem_cbranch
(
rreil
-
convert
-
sem
-
sexpr
cbs
c
.
cond
)
(
rreil
-
convert
-
sem
-
address
cbs
c
.
target
-
true
)
(
rreil
-
convert
-
sem
-
address
cbs
c
.
target
-
false
)
...
...
specifications/rreil/rreil-liveness.ml
View file @
97512701
...
...
@@ -19,7 +19,7 @@ val lv-kill kills stmt =
val
visit
-
stmt
kills
stmt
=
case
stmt
of
SEM_ASSIGN
x
:
visit
-
semvar
kills
(
rreil
-
sizeOf
x
.
rhs
)
x
.
lhs
SEM_ASSIGN
x
:
visit
-
semvar
kills
x
.
size
x
.
lhs
|
SEM_LOAD
x
:
visit
-
semvar
kills
x
.
size
x
.
lhs
|
SEM_ITE
x
:
lv
-
union
kills
(
lv
-
intersection
(
lv
-
kills
x
.
then_branch
)
(
lv
-
kills
x
.
else_branch
))
|
_
:
kills
...
...
@@ -57,8 +57,8 @@ val lv-gen gens stmt =
val
visit
-
arity2
gens
x
=
lv
-
union
(
visit
-
lin
gens
x
.
size
x
.
opnd1
)
(
visit
-
lin
gens
x
.
size
x
.
opnd2
)
(
visit
-
lin
gens
42
x
.
opnd1
)
#
Todo
(
grammar
)
:
x
.
size
instead
of
42
,
fix
(
visit
-
lin
gens
42
x
.
opnd2
)
#
Todo
(
grammar
)
:
x
.
size
instead
of
42
,
fix
val
visit
-
op
-
cmp
gens
cmp
=
case
cmp
of
...
...
specifications/rreil/rreil-pretty.ml
View file @
97512701
...
...
@@ -42,9 +42,9 @@ val rreil-show-flop f =
val
rreil
-
show
-
stmt
s
=
case
s
of
SEM_ASSIGN
x
:
rreil
-
show
-
var
x
.
lhs
+++
" = "
+++
rreil
-
show
-
expr
x
.
rhs
|
SEM_LOAD
x
:
rreil
-
show
-
var
x
.
lhs
+++
" = "
+++
rreil
-
show
-
ptrderef
x
.
size
x
.
address
|
SEM_STORE
x
:
"*"
+++
rreil
-
show
-
address
x
.
address
+++
" = "
+++
rreil
-
show
-
expr
x
.
rhs
SEM_ASSIGN
x
:
rreil
-
show
-
var
x
.
lhs
+++
" =
:"
+++
show
-
int
x
.
size
+++
"
"
+++
rreil
-
show
-
expr
x
.
rhs
|
SEM_LOAD
x
:
rreil
-
show
-
var
x
.
lhs
+++
" =
:"
+++
show
-
int
x
.
size
+++
"
"
+++
rreil
-
show
-
ptrderef
x
.
size
x
.
address
|
SEM_STORE
x
:
"*"
+++
rreil
-
show
-
address
x
.
address
+++
" =
:"
+++
show
-
int
x
.
size
+++
"
"
+++
rreil
-
show
-
expr
x
.
rhs
|
SEM_ITE
x
:
"if ("
+++
rreil
-
show
-
sexpr
x
.
cond
+++
") {
\n
"
+++
rreil
-
show
-
stmts
x
.
then_branch
+++
"} else {
\n
"
+++
rreil
-
show
-
stmts
x
.
else_branch
+++
"}"
|
SEM_WHILE
x
:
"while ("
+++
rreil
-
show
-
sexpr
x
.
cond
+++
") {
\n
"
+++
rreil
-
show
-
stmts
x
.
body
+++
"}"
|
SEM_CBRANCH
x
:
"if ("
+++
rreil
-
show
-
sexpr
x
.
cond
+++
") goto "
+++
rreil
-
show
-
address
x
.
target
-
true
+++
" else goto "
+++
rreil
-
show
-
address
x
.
target
-
false
...
...
@@ -74,7 +74,7 @@ val rreil-show-op-cmp cmp =
val
rreil
-
show
-
expr
expr
=
case
expr
of
SEM_SEXPR
x
:
rreil
-
show
-
arity1
-
sexpr
x
SEM_SEXPR
x
:
rreil
-
show
-
sexpr
x
|
SEM_MUL
x
:
"mul"
+++
rreil
-
show
-
arity2
x
|
SEM_DIV
x
:
"div"
+++
rreil
-
show
-
arity2
x
|
SEM_DIVS
x
:
"divs"
+++
rreil
-
show
-
arity2
x
...
...
@@ -85,14 +85,13 @@ val rreil-show-expr expr =
|
SEM_AND
x
:
"and"
+++
rreil
-
show
-
arity2
x
|
SEM_OR
x
:
"or"
+++
rreil
-
show
-
arity2
x
|
SEM_XOR
x
:
"xor"
+++
rreil
-
show
-
arity2
x
|
SEM_SX
x
:
"sx["
+++
show
-
int
x
.
fromsize
+++
"->
"
+++
show
-
int
x
.
size
+++
"
]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
|
SEM_ZX
x
:
"zx["
+++
show
-
int
x
.
fromsize
+++
"->
"
+++
show
-
int
x
.
size
+++
"
]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
|
SEM_SX
x
:
"sx["
+++
show
-
int
x
.
fromsize
+++
"->
#
]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
|
SEM_ZX
x
:
"zx["
+++
show
-
int
x
.
fromsize
+++
"->
#
]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
end
val
rreil
-
show
-
arity1
-
sexpr
x
=
"["
+++
show
-
int
x
.
size
+++
"]("
+++
rreil
-
show
-
sexpr
x
.
opnd1
+++
")"
val
rreil
-
show
-
arity1
x
=
"["
+++
show
-
int
x
.
size
+++
"]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
val
rreil
-
show
-
arity2
x
=
"["
+++
show
-
int
x
.
size
+++
"]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
","
+++
rreil
-
show
-
linear
x
.
opnd2
+++
")"
val
rreil
-
show
-
cmp
x
=
"["
+++
show
-
int
x
.
size
+++
"->1]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
","
+++
rreil
-
show
-
linear
x
.
opnd2
+++
")"
val
rreil
-
show
-
arity1
x
=
" ("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
")"
val
rreil
-
show
-
arity2
x
=
" ("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
","
+++
rreil
-
show
-
linear
x
.
opnd2
+++
")"
val
rreil
-
show
-
cmp
x
=
" [*->1]("
+++
rreil
-
show
-
linear
x
.
opnd1
+++
","
+++
rreil
-
show
-
linear
x
.
opnd2
+++
")"
val
rreil
-
show
-
ptrderef
sz
addr
=
"*["
+++
show
-
int
addr
.
size
+++
"->"
+++
show
-
int
sz
+++
"]("
+++
rreil
-
show
-
linear
addr
.
address
+++
")"
val
rreil
-
show
-
address
addr
=
"["
+++
show
-
int
addr
.
size
+++
"]("
+++
rreil
-
show
-
linear
addr
.
address
+++
")"
val
rreil
-
show
-
var
x
=
...
...
specifications/rreil/rreil.ml
View file @
97512701
...
...
@@ -5,9 +5,9 @@ type sem_id =
FLOATING_FLAGS
|
VIRT_T
of
int
type
sem_arity1
=
{
size
:
int
,
opnd1
:
sem_linear
}
type
sem_arity2
=
{
size
:
int
,
opnd1
:
sem_linear
,
opnd2
:
sem_linear
}
type
sem_cmp
=
{
size
:
int
,
opnd1
:
sem_linear
,
opnd2
:
sem_linear
}
type
sem_arity1
=
{
opnd1
:
sem_linear
}
type
sem_arity2
=
{
opnd1
:
sem_linear
,
opnd2
:
sem_linear
}
type
sem_cmp
=
{
opnd1
:
sem_linear
,
opnd2
:
sem_linear
}
type
sem_address
=
{
size
:
int
,
address
:
sem_linear
}
type
sem_var
=
{
id
:
sem_id
,
offset
:
int
}
...
...
@@ -33,7 +33,7 @@ type sem_op_cmp =
|
SEM_CMPLTU
of
sem_cmp
type
sem_expr
=
SEM_SEXPR
of
{
size
:
int
,
opnd1
:
sem_sexpr
}
SEM_SEXPR
of
sem_sexpr
|
SEM_MUL
of
sem_arity2
|
SEM_DIV
of
sem_arity2
|
SEM_DIVS
of
sem_arity2
...
...
@@ -44,8 +44,8 @@ type sem_expr =
|
SEM_AND
of
sem_arity2
|
SEM_OR
of
sem_arity2
|
SEM_XOR
of
sem_arity2
|
SEM_SX
of
{
size
:
int
,
fromsize
:
int
,
opnd1
:
sem_linear
}
|
SEM_ZX
of
{
size
:
int
,
fromsize
:
int
,
opnd1
:
sem_linear
}
|
SEM_SX
of
{
fromsize
:
int
,
opnd1
:
sem_linear
}
|
SEM_ZX
of
{
fromsize
:
int
,
opnd1
:
sem_linear
}
type
sem_varl
=
{
id
:
sem_id
,
offset
:
int
,
size
:
int
}
...
...
@@ -59,9 +59,9 @@ type sem_flop =
|
SEM_FMUL
type
sem_stmt
=
SEM_ASSIGN
of
{
lhs
:
sem_var
,
rhs
:
sem_expr
}
|
SEM_LOAD
of
{
lhs
:
sem_var
,
size
:
int
,
address
:
sem_address
}
|
SEM_STORE
of
{
address
:
sem_address
,
rhs
:
sem_expr
}
SEM_ASSIGN
of
{
size
:
int
,
lhs
:
sem_var
,
rhs
:
sem_expr
}
|
SEM_LOAD
of
{
size
:
int
,
lhs
:
sem_var
,
address
:
sem_address
}
|
SEM_STORE
of
{
size
:
int
,
address
:
sem_address
,
rhs
:
sem_expr
}
|
SEM_ITE
of
{
cond
:
sem_sexpr
,
then_branch
:
sem_stmts
,
else_branch
:
sem_stmts
}
|
SEM_WHILE
of
{
cond
:
sem_sexpr
,
body
:
sem_stmts
}
|
SEM_CBRANCH
of
{
cond
:
sem_sexpr
,
target
-
true
:
sem_address
,
target
-
false
:
sem_address
}
...
...
@@ -78,23 +78,6 @@ type sem_stmts =
SEM_CONS
of
{
hd
:
sem_stmt
,
tl
:
sem_stmts
}
|
SEM_NIL
val
rreil
-
sizeOf
op
=
case
op
of
SEM_SEXPR
x
:
x
.
size
|
SEM_MUL
x
:
x
.
size
|
SEM_DIV
x
:
x
.
size
|
SEM_DIVS
x
:
x
.
size
|
SEM_MOD
x
:
x
.
size
|
SEM_SHL
x
:
x
.
size
|
SEM_SHR
x
:
x
.
size
|
SEM_SHRS
x
:
x
.
size
|
SEM_AND
x
:
x
.
size
|
SEM_OR
x
:
x
.
size
|
SEM_XOR
x
:
x
.
size
|
SEM_SX
x
:
x
.
size
|
SEM_ZX
x
:
x
.
size
end
val
rreil
-
stmts
-
rev
stmts
=
let
val
lp
stmt
acc
=
...
...
@@ -111,7 +94,7 @@ val _var x _offset o = {id=x, offset=o}
val
at
-
offset
v
o
=
@
{
offset
=
o
}
v
val
var
x
=
SEM_LIN_VAR
x
val
lin
-
sum
x
y
=
SEM_LIN_ADD
{
opnd1
=
x
,
opnd2
=
y
}
val
lin
sz
l
=
SEM_SEXPR
{
size
=
sz
,
opnd1
=
SEM_SEXPR_LIN
l
}
val
lin
l
=
SEM_SEXPR
(
SEM_SEXPR_LIN
l
)
val
address
sz
addr
=
{
size
=
sz
,
address
=
addr
}
val
varl
-
from
-
var
sz
v
=
@
{
size
=
sz
}
v
...
...
@@ -159,9 +142,9 @@ val mklabel = do
return
l
end
val
/
ASSIGN
a
b
=
SEM_ASSIGN
{
lhs
=
a
,
rhs
=
b
}
val
/
LOAD
sz
a
b
=
SEM_LOAD
{
lhs
=
a
,
size
=
sz
,
address
=
b
}
val
/
STORE
a
b
=
SEM_STORE
{
address
=
a
,
rhs
=
b
}
val
/
ASSIGN
sz
a
b
=
SEM_ASSIGN
{
size
=
sz
,
lhs
=
a
,
rhs
=
b
}
val
/
LOAD
sz
a
b
=
SEM_LOAD
{
size
=
sz
,
lhs
=
a
,
address
=
b
}
val
/
STORE
sz
a
b
=
SEM_STORE
{
size
=
sz
,
address
=
a
,
rhs
=
b
}
val
/
ADD
a
b
=
SEM_LIN_ADD
{
opnd1
=
a
,
opnd2
=
b
}
val
/
SUB
a
b
=
SEM_LIN_SUB
{
opnd1
=
a
,
opnd2
=
b
}
val
/
ITE
c
t
e
=
SEM_ITE
{
cond
=
c
,
then_branch
=
t
,
else_branch
=
e
}
...
...
@@ -196,31 +179,31 @@ val stack-set stmt = do
update
@
{
stack
=
stmt
}
end
val
mov
sz
a
b
=
push
(
/
ASSIGN
a
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_LIN
b
)}
))
val
undef
sz
a
=
push
(
/
ASSIGN
a
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
SEM_SEXPR_ARB
}
))
val
mov
sz
a
b
=
push
(
/
ASSIGN
sz
a
(
SEM_SEXPR
(
SEM_SEXPR_LIN
b
)
))
val
undef
sz
a
=
push
(
/
ASSIGN
sz
a
(
SEM_SEXPR
SEM_SEXPR_ARB
))
val
load
sz
a
psz
b
=
push
(
/
LOAD
sz
a
{
size
=
psz
,
address
=
b
})
val
store
a
b
=
push
(
/
STORE
a
b
)
val
add
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
SEM_SEXPR_LIN
(
/
ADD
b
c
)}
))
val
sub
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
SEM_SEXPR_LIN
(
/
SUB
b
c
)}
))
val
andb
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_AND
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
orb
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_OR
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
xorb
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_XOR
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
mul
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_MUL
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
div
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_DIV
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
divs
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_DIVS
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
shl
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_SHL
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
shr
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_SHR
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
shrs
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_SHRS
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
modulo
sz
a
b
c
=
push
(
/
ASSIGN
a
(
SEM_MOD
{
size
=
sz
,
opnd1
=
b
,
opnd2
=
c
}))
val
movsx
szA
a
szB
b
=
push
(
/
ASSIGN
a
(
SEM_SX
{
size
=
szA
,
fromsize
=
szB
,
opnd1
=
b
}))
val
movzx
szA
a
szB
b
=
push
(
/
ASSIGN
a
(
SEM_ZX
{
size
=
szA
,
fromsize
=
szB
,
opnd1
=
b
}))
val
convert
szA
a
szB
b
=
push
(
/
ASSIGN
a
(
SEM_ZX
{
size
=
szA
,
fromsize
=
szB
,
opnd1
=
b
}))
val
cmpeq
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPEQ
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
cmpneq
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPNEQ
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
cmples
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPLES
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
cmpleu
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPLEU
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
cmplts
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPLTS
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
cmpltu
sz
f
a
b
=
push
(
/
ASSIGN
f
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
(
SEM_SEXPR_CMP
(
SEM_CMPLTU
{
size
=
sz
,
opnd1
=
a
,
opnd2
=
b
}))}
))
val
store
sz
a
b
=
push
(
/
STORE
sz
a
b
)
val
add
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_SEXPR
(
SEM_SEXPR_LIN
(
/
ADD
b
c
))
))
val
sub
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_SEXPR
(
SEM_SEXPR_LIN
(
/
SUB
b
c
))
))
val
andb
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_AND
{
opnd1
=
b
,
opnd2
=
c
}))
val
orb
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_OR
{
opnd1
=
b
,
opnd2
=
c
}))
val
xorb
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_XOR
{
opnd1
=
b
,
opnd2
=
c
}))
val
mul
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_MUL
{
opnd1
=
b
,
opnd2
=
c
}))
val
div
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_DIV
{
opnd1
=
b
,
opnd2
=
c
}))
val
divs
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_DIVS
{
opnd1
=
b
,
opnd2
=
c
}))
val
shl
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_SHL
{
opnd1
=
b
,
opnd2
=
c
}))
val
shr
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_SHR
{
opnd1
=
b
,
opnd2
=
c
}))
val
shrs
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_SHRS
{
opnd1
=
b
,
opnd2
=
c
}))
val
modulo
sz
a
b
c
=
push
(
/
ASSIGN
sz
a
(
SEM_MOD
{
opnd1
=
b
,
opnd2
=
c
}))
val
movsx
szA
a
szB
b
=
push
(
/
ASSIGN
szA
a
(
SEM_SX
{
fromsize
=
szB
,
opnd1
=
b
}))
val
movzx
szA
a
szB
b
=
push
(
/
ASSIGN
szA
a
(
SEM_ZX
{
fromsize
=
szB
,
opnd1
=
b
}))
val
convert
szA
a
szB
b
=
push
(
/
ASSIGN
szA
a
(
SEM_ZX
{
fromsize
=
szB
,
opnd1
=
b
}))
val
cmpeq
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPEQ
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
cmpneq
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPNEQ
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
cmples
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPLES
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
cmpleu
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPLEU
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
cmplts
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPLTS
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
cmpltu
sz
f
a
b
=
push
(
/
ASSIGN
sz
f
(
SEM_SEXPR
(
SEM_SEXPR_CMP
(
SEM_CMPLTU
{
opnd1
=
a
,
opnd2
=
b
}))
))
val
ite
c
t
e
=
push
(
/
ITE
(
SEM_SEXPR_LIN
c
)
t
e
)
val
while
c
b
=
push
(
/
WHILE
(
SEM_SEXPR_LIN
c
)
b
)
val
jump
address
=
do
...
...
specifications/x86/x86-rreil-translator-m-z.ml
View file @
97512701
...
...
@@ -1768,7 +1768,7 @@ val ps-push opnd-sz opnd = do
sub
sp
.
size
sp
(
var
sp
)
(
imm
2
)
;
segmented
-
store
(
address
sp
.
size
(
var
sp
))
(
lin
opnd
-
sz
opnd
)
(
SEG_OVERRIDE
SS
)
segmented
-
store
opnd
-
sz
(
address
sp
.
size
(
var
sp
))
(
lin
opnd
)
(
SEG_OVERRIDE
SS
)
#
store
(
address
sp
.
size
(
segment
-
add
(
var
sp
)
segment
))
(
lin
opnd
-
sz
opnd
)
end
...
...
@@ -2529,7 +2529,7 @@ val sem-stos size x = let
mem
-
sem
<-
return
(
semantic
-
register
-
of
(
register
-
by
-
size
low
DI_
x
.
addr
-
sz
));
a
<-
return
(
semantic
-
register
-
of
(
register
-
by
-
size
low
A
size
));
segmented
-
store
(
address
x
.
addr
-
sz
(
var
mem
-
sem
))
(
lin
a
.
size
(
var
a
))
(
SEG_OVERRIDE
ES
);
segmented
-
store
a
.
size
(
address
x
.
addr
-
sz
(
var
mem
-
sem
))
(
lin
(
var
a
))
(
SEG_OVERRIDE
ES
);
direction
-
adjust
mem
-
sem
.
size
mem
-
sem
size
end
...
...
specifications/x86/x86-rreil-translator.ml
View file @
97512701
...
...
@@ -120,10 +120,10 @@ val segmented-load dst-sz dst addr-sz address segment = do
load
dst
-
sz
dst
addr
-
sz
address
-
segmented
end
val
segmented
-
store
addr
rhs
segment
=
do
val
segmented
-
store
sz
addr
rhs
segment
=
do
address
-
segmented
<-
segmented
-
lin
addr
.
address
addr
.
size
segment
;
addr
-
sz
<-
real
-
addr
-
sz
;
store
(
address
addr
-
sz
address
-
segmented
)
rhs
store
sz
(
address
addr
-
sz
address
-
segmented
)
rhs
end
#
val
segment
segment
=
do
...
...
@@ -293,7 +293,7 @@ val write-extend avx-encoded sz a b =
case
a
of
SEM_WRITE_MEM
x
:
#
store
x
(
SEM_LIN
{
size
=
sz
,
opnd1
=
b
})
segmented
-
store
x
(
SEM_SEXPR
{
size
=
sz
,
opnd1
=
SEM_SEXPR_LIN
b
}
)
x
.
segment
segmented
-
store
sz
x
(
SEM_SEXPR
(
SEM_SEXPR_LIN
b
)
)
x
.
segment
|
SEM_WRITE_VAR
x
:
do
#
if
mode64
then
#
mov
32
(
semantic
-
register
-
of
EAX
)
(
imm
100
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment