m2-internship/dwarf-synthesis
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Simplify evaluation of affine rsp setting expr

Browse source
This commit is contained in:
Théophile Bastian 2018-11-15 17:23:20 +01:00
parent 745e0d96d9
commit b7a5caf87f
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
DwarfSynth/Simplest.ml
View file

@ -163,13 +163,13 @@ let build_next_instr graph =
let interpret_var_expr c_var offset expr = BStd.Bil.( let interpret_var_expr c_var offset expr = BStd.Bil.(
let closed_form = BStd.Exp.substitute let closed_form = BStd.Exp.substitute
(var c_var) (var c_var)
(int (BStd.Word.of_int64 offset)) (int (BStd.Word.of_int64 (Int64.neg offset)))
expr expr
in in
let res = BStd.Exp.eval closed_form in let res = BStd.Exp.eval closed_form in
match res with match res with
| Imm value -> | Imm value ->
Some (BStd.Word.to_int64_exn @@ BStd.Word.signed value) Some (Int64.neg @@ BStd.Word.to_int64_exn @@ BStd.Word.signed value)
| _ -> None | _ -> None
) )
@ -192,9 +192,7 @@ let process_def def (cur_offset: memory_offset)
let interpreted = interpret_var_expr bil_var cur_offset exp in let interpreted = interpret_var_expr bil_var cur_offset exp in
(match interpreted with (match interpreted with
| None -> lose_track | None -> lose_track
| Some interp_val -> | Some new_offset ->
let gap = Int64.sub interp_val cur_offset in
let new_offset = Int64.sub cur_offset gap in
Some (RspOffset(new_offset), new_offset) Some (RspOffset(new_offset), new_offset)
) )
| _ -> lose_track | _ -> lose_track