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

Simplest: change workflow

Browse source
This commit is contained in:
Théophile Bastian 2018-11-16 13:59:16 +01:00
parent aec0ab59ad
commit 9f09dec677
1 changed files with 63 additions and 124 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

187
DwarfSynth/Simplest.ml
View file

@ -173,11 +173,12 @@ let interpret_var_expr c_var offset expr = BStd.Bil.(
| _ -> None | _ -> None
) )
let process_def def (cur_offset: memory_offset) let process_def def (cur_cfa: cfa_pos)
: ((cfa_pos * memory_offset) option) = : (cfa_pos option) =
let lose_track = Some (CfaLostTrack, Int64.zero) in let lose_track = Some (CfaLostTrack) in
(match Regs.X86_64.of_var (BStd.Def.lhs def) with
| Some reg when reg = Regs.X86_64.rsp -> (match cur_cfa, Regs.X86_64.of_var (BStd.Def.lhs def) with
| RspOffset(cur_offset), Some reg when reg = Regs.X86_64.rsp ->
let exp = BStd.Def.rhs def in let exp = BStd.Def.rhs def in
let free_vars = BStd.Exp.free_vars exp in let free_vars = BStd.Exp.free_vars exp in
let free_x86_regs = Regs.X86_64.map_varset free_vars in let free_x86_regs = Regs.X86_64.map_varset free_vars in
@ -193,7 +194,7 @@ let process_def def (cur_offset: memory_offset)
(match interpreted with (match interpreted with
| None -> lose_track | None -> lose_track
| Some new_offset -> | Some new_offset ->
Some (RspOffset(new_offset), new_offset) Some (RspOffset(new_offset))
) )
| _ -> lose_track | _ -> lose_track
) )
@ -201,11 +202,14 @@ let process_def def (cur_offset: memory_offset)
) )
| _ -> None) | _ -> None)
let process_jmp jmp (cur_offset: memory_offset) let process_jmp jmp (cur_cfa: cfa_pos)
: ((cfa_pos * memory_offset) option) = : (cfa_pos option) =
let gen_change off = let gen_change = match cur_cfa with
let new_offset = Int64.add cur_offset (Int64.of_int off) in | RspOffset cur_offset -> (fun off ->
Some (RspOffset(new_offset), new_offset) let new_offset = Int64.add cur_offset (Int64.of_int off) in
Some (RspOffset(new_offset))
)
| _ -> (fun _ -> None)
in in
match (BStd.Jmp.kind jmp) with match (BStd.Jmp.kind jmp) with
@ -213,14 +217,13 @@ let process_jmp jmp (cur_offset: memory_offset)
| BStd.Ret ret -> gen_change (8) | BStd.Ret ret -> gen_change (8)
| _ -> None | _ -> None
let sym_of_blk next_instr_graph blk : cfa_changes_fde = let process_blk
(** Extracts the symbolic CFA changes of a block. These changes assume that next_instr_graph (block_init: cfa_pos) blk : (cfa_changes_fde * cfa_pos) =
at the beginning of the block, CFA = RspOffset(0) and will be offset (** Extracts the CFA changes of a block. *)
after *)
let apply_offset cur_addr_opt ((accu:cfa_change list), cur_offset) = function let apply_offset cur_addr_opt ((accu:cfa_change list), cur_cfa) = function
| None -> (accu, cur_offset) | None -> (accu, cur_cfa)
| Some (pos, n_offset) -> | Some pos ->
let cur_addr = (match cur_addr_opt with let cur_addr = (match cur_addr_opt with
| None -> assert false | None -> assert false
| Some x -> to_int64_addr x) in | Some x -> to_int64_addr x) in
@ -229,55 +232,27 @@ let sym_of_blk next_instr_graph blk : cfa_changes_fde =
(change :: cur_accu)) (change :: cur_accu))
(AddrMap.find cur_addr next_instr_graph) (AddrMap.find cur_addr next_instr_graph)
accu), accu),
n_offset pos
in in
let fold_elt (accu, cur_offset) elt = match elt with let fold_elt (accu, cur_cfa) elt = match elt with
| `Def(def) -> | `Def(def) ->
apply_offset apply_offset
(opt_addr_of def) (accu, cur_offset) @@ process_def def cur_offset (opt_addr_of def) (accu, cur_cfa) @@ process_def def cur_cfa
| `Jmp(jmp) -> | `Jmp(jmp) ->
apply_offset apply_offset
(opt_addr_of jmp) (accu, cur_offset) @@ process_jmp jmp cur_offset (opt_addr_of jmp) (accu, cur_cfa) @@ process_jmp jmp cur_cfa
| _ -> (accu, cur_offset) | _ -> (accu, cur_cfa)
in in
let elts_seq = BStd.Blk.elts blk in let elts_seq = BStd.Blk.elts blk in
let out, end_offset = BStd.Seq.fold elts_seq let out, end_cfa = BStd.Seq.fold elts_seq
~init:([], Int64.zero) ~init:([], block_init)
~f:fold_elt in ~f:fold_elt in
out out, end_cfa
let end_offset (changelist: cfa_changes_fde): memory_offset option =
match changelist with
| CfaChange(_, RspOffset(x)) :: _ -> Some x
| _ -> None
exception Inconsistent of BStd.tid exception Inconsistent of BStd.tid
let rec dfs_propagate changemap propagated parent_val node graph =
let c_tid = BStd.Term.tid @@ CFG.Node.label node in
match TIdMap.find_opt c_tid propagated with
| Some x ->
if x = parent_val then
(* Already propagated and consistent, all fine *)
propagated
else
(* Already propagated with a different value: inconsistency *)
raise (Inconsistent c_tid)
| None ->
let n_propagated = TIdMap.add c_tid parent_val propagated in
let outwards = CFG.Node.outputs node graph in
let self_entry = TIdMap.find c_tid changemap in
let offset = (match end_offset self_entry with
Some x -> x
| None -> Int64.zero) in
let cur_val = Int64.add parent_val offset in
BStd.Seq.fold outwards
~init:n_propagated
~f:(fun accu edge ->
dfs_propagate changemap accu cur_val (CFG.Edge.dst edge) graph)
let get_entry_blk graph = let get_entry_blk graph =
let entry = BStd.Seq.min_elt (CFG.nodes graph) ~cmp:(fun x y -> let entry = BStd.Seq.min_elt (CFG.nodes graph) ~cmp:(fun x y ->
let ax = opt_addr_of @@ CFG.Node.label x let ax = opt_addr_of @@ CFG.Node.label x
@ -292,14 +267,7 @@ let get_entry_blk graph =
| None -> assert false | None -> assert false
| Some x -> x | Some x -> x
let same_keys map1 map2 = let process_sub sub : cfa_changes_fde =
let exists_in_other other key _ =
TIdMap.mem key other in
TIdMap.for_all (exists_in_other map2) map1
&& TIdMap.for_all (exists_in_other map1) map2
let of_sub sub : cfa_changes_fde =
(** Extracts the `cfa_changes_fde` of a subroutine *) (** Extracts the `cfa_changes_fde` of a subroutine *)
Format.eprintf "Sub %s...@." @@ BStd.Sub.name sub ; Format.eprintf "Sub %s...@." @@ BStd.Sub.name sub ;
@ -308,77 +276,48 @@ let of_sub sub : cfa_changes_fde =
let next_instr_graph = build_next_instr cfg in let next_instr_graph = build_next_instr cfg in
let initial_cfa_rsp_offset = Int64.of_int 8 in let initial_cfa_rsp_offset = Int64.of_int 8 in
let store_sym accu blk =
let blk = CFG.Node.label blk in
let res = sym_of_blk next_instr_graph blk in
TIdMap.add (BStd.Term.tid blk) res accu
in
let node_addr nd = opt_addr_of @@ CFG.Node.label nd in let rec dfs_process
(sub_changes: (cfa_changes_fde * cfa_pos) TIdMap.t) node entry_offset =
(** Processes one block *)
let merge_corrected blk_tid changes offset = match (changes, offset) with let cur_blk = CFG.Node.label node in
| Some changes, Some offset -> let tid = BStd.Term.tid @@ cur_blk in
Some (
List.map (fun (CfaChange(addr, pos)) -> match pos with
RspOffset(off) -> CfaChange(addr,
RspOffset(Int64.add off offset))
| RbpOffset(off) -> CfaChange(addr, RbpOffset(off))
| CfaLostTrack -> CfaChange(addr, CfaLostTrack)
)
changes
)
| _ -> None
in
let tid_match = BStd.Seq.fold (CFG.nodes cfg) match (TIdMap.find_opt tid sub_changes) with
~init:TIdMap.empty | None ->
~f:(fun accu node -> (* Not yet visited: compute the changes *)
let tid = BStd.Term.tid @@ CFG.Node.label node in let cur_blk_changes, end_cfa =
TIdMap.add tid node accu) process_blk next_instr_graph entry_offset cur_blk in
in let n_sub_changes =
TIdMap.add tid (cur_blk_changes, entry_offset) sub_changes in
let blk_sym = BStd.Seq.fold BStd.Seq.fold (CFG.Node.succs node cfg)
~init:TIdMap.empty ~f:(fun accu child -> dfs_process accu child end_cfa)
~f:store_sym ~init:n_sub_changes
@@ CFG.nodes cfg | Some (_, former_entry_offset) ->
(* Already visited: check that entry values are matching *)
if entry_offset <> former_entry_offset then
raise (Inconsistent tid)
else
sub_changes
in in
let entry_blk = get_entry_blk cfg in let entry_blk = get_entry_blk cfg in
let offset_map = dfs_propagate let initial_offset = (RspOffset initial_cfa_rsp_offset) in
blk_sym (TIdMap.empty) initial_cfa_rsp_offset entry_blk cfg in let changes_map = dfs_process TIdMap.empty entry_blk initial_offset in
let corrected = TIdMap.merge merge_corrected blk_sym offset_map in let merged_changes = TIdMap.fold
(fun _ (cfa_changes, _) accu -> cfa_changes @ accu)
changes_map
[CfaChange(int64_addr_of sub, initial_offset)] in
let is_connex = same_keys tid_match corrected in let sorted_changes = List.sort
if not is_connex then (fun (CfaChange (addr1, _)) (CfaChange (addr2, _)) ->
raise InvalidSub ; compare addr1 addr2)
merged_changes
let tid_list = TIdMap.bindings tid_match in
let sorted_blk = List.sort (fun (tid1, bl1) (tid2, bl2) ->
let res = match (node_addr bl1, node_addr bl2) with
| Some addr1, Some addr2 -> compare addr1 addr2
| Some _, None -> 1
| None, Some _ -> -1
| None, None -> compare tid1 tid2
in in
-res)
tid_list
in
let out = List.fold_left sorted_changes
(fun accu blk ->
let changes = TIdMap.find blk corrected in
List.fold_left (fun accu chg -> chg::accu)
accu
changes
)
[]
(List.map (fun (x, y) -> x) sorted_blk) in
let init = [
CfaChange(int64_addr_of sub, RspOffset(initial_cfa_rsp_offset))
] in
init @ out
let cleanup_fde (fde_changes: cfa_changes_fde) : cfa_changes_fde = let cleanup_fde (fde_changes: cfa_changes_fde) : cfa_changes_fde =
(** Cleanup the result of `of_sub`. (** Cleanup the result of `of_sub`.
@ -429,7 +368,7 @@ let of_prog prog : cfa_changes =
(** Extracts the `cfa_changes` of a program *) (** Extracts the `cfa_changes` of a program *)
let fold_step accu sub = let fold_step accu sub =
(try (try
let res = cleanup_fde @@ of_sub sub in let res = cleanup_fde @@ process_sub sub in
StrMap.add (BStd.Sub.name sub) res accu StrMap.add (BStd.Sub.name sub) res accu
with InvalidSub -> accu) with InvalidSub -> accu)
in in