Commit d1c90aae authored by Julian Kranz's avatar Julian Kranz

X86 RREIL Translator

RREIL Specification

- Bug fixes
- while/ite
parent 2d7b53fa
......@@ -57,6 +57,16 @@ type sem_stmt =
| SEM_CALL of {cond: sem_linear, size:int, target: sem_linear}
| SEM_RETURN of {cond: sem_linear, size:int, target: sem_linear}
| SEM_ITE of {cond: sem_linear, then_branch: sem_stmts, else_branch: sem_stmts}
| SEM_WHILE of {cond: sem_linear, body: sem_stmts}
| SEM_CBRANCH of {cond: sem_linear, target_true: sem_address, target_false: sem_address}
| SEM_BRANCH of {hint: branch_hint, target: sem_address}
type branch_hint =
HINT_JUMP
| HINT_CALL
| HINT_RET
type sem_stmts =
SEM_CONS of {hd:sem_stmt, tl:sem_stmts}
| SEM_NIL
......@@ -127,12 +137,35 @@ val /LABEL l = SEM_LABEL{label=l}
val /IFGOTOLABEL c l = SEM_IF_GOTO_LABEL{cond=c,label=l}
val /IFGOTO c sz t = SEM_IF_GOTO{cond=c,size=sz,target=t}
val /GOTOLABEL l = SEM_IF_GOTO_LABEL{cond=SEM_LIN_IMM{imm=1},label=l}
val /ITE c t e = SEM_ITE{cond=c,then_branch=t,else_branch=e}
val /WHILE c b = SEM_WHILE{cond=c,body=b}
val push insn = do
tl <- query $stack;
update @{stack=SEM_CONS{hd=insn,tl=tl}}
end
val pop-all = do
head <- query $stack;
update @{stack=SEM_NIL};
head
end
#val connect-tail stmt tail =
# case stmt of
# SEM_NIL: tail
# | SEM_CONS x: SEM_CONS{hd=x.hd,tl=(connect-tail x.tl tail)}
# end
#val concat stmt = do
# tail <- query $stack;
# update @{stack=(connect-tail stmt tail)}
#end
val stack-set stmt = do
update @{stack=stmt}
end
val mov sz a b = push (/ASSIGN a (SEM_LIN{size=sz,opnd1=b}))
val undef sz a = push (/ASSIGN a (SEM_ARB{size=sz}))
val load sz a psz b = push (/LOAD sz a {size=psz,address=b})
......@@ -162,6 +195,8 @@ val label l = push (/LABEL l)
val ifgotolabel c l = push (/IFGOTOLABEL c l)
val gotolabel l = push (/GOTOLABEL l)
val ifgoto c sz addr = push (/IFGOTO c sz addr)
val ite c t e = push (/ITE c t e)
val while c b = push (/WHILE c b)
val const i = return (SEM_LIN_IMM{imm=i})
......
......@@ -25,9 +25,17 @@ val guess-sizeof1 op =
| IMM64 i: return 64
end
type signedness =
Signed
| Unsigned
val conv-with conv sz x =
let
val conv-imm conv x = return (SEM_LIN_IMM{imm=conv x})
val conv-imm conv x = case conv of
Signed: return (SEM_LIN_IMM{imm=sx x})
| Unsigned: return (SEM_LIN_IMM{imm=zx x})
end
val conv-reg r = return (SEM_LIN_VAR (semantic-register-of r))
......@@ -54,7 +62,7 @@ val conv-with conv sz x =
end})
end
val conv-mem x = conv-with sx x.psz x.opnd
val conv-mem x = conv-with Signed x.psz x.opnd
in
case x of
IMM8 x: conv-imm conv x
......@@ -73,7 +81,7 @@ val conv-with conv sz x =
end
end
val read sz x = conv-with zx sz x
val read sz x = conv-with Unsigned sz x
val read-flow sz x =
let
val conv-bv v = return (SEM_LIN_IMM{imm=sx v})
......@@ -91,7 +99,7 @@ val read-flow sz x =
val write sz x =
case x of
MEM x:
do address <- conv-with sx x.psz x.opnd;
do address <- conv-with Signed x.psz x.opnd;
return
(SEM_WRITE_MEM
{size= x.psz,
......@@ -139,17 +147,35 @@ val fAF = return (var//0 (ARCH_R ~3)) # AF
val zero = return (SEM_LIN_IMM{imm=0})
val _if c _then a _else b = do
stack <- pop-all;
a;
t <- pop-all;
b;
e <- pop-all;
stack-set stack;
ite c t e
end
val _while c __ b = do
stack <- pop-all;
b;
body <- pop-all;
stack-set stack;
while c body
end
val undef-opnd opnd = do
sz <- guess-sizeof1 opnd;
a <- write sz opnd;
t <- mktemp;
commit sz a t
commit sz a (var t)
end
val sem-undef-arity-ge1 x = do
case x.opnd1 of
REG r: undef-opnd x.opnd1
| MEM x: undef-opnd x.opnd1
| MEM m: undef-opnd x.opnd1
end
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment