From 3f8d5ace6e871d32d7f8eb2caf1b3e25dbfe4f8d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 23 Aug 2019 07:19:48 -0700 Subject: [PATCH] [sledge] Eliminate SSA Summary: While SSA can be useful for code transformation purposes, it offers little for semantic static analyses. Essentially, such analyses explore the dynamic semantics of code, and the *static* single assignment property does not buy much. For example, once an execution visits a loop body that assigns a variable, there are multiple assignments that the analysis must deal with. This leads to the need to treat blocks as if they assign all their local variables, renaming to avoid name clashes a la Floyd's assignment axiom. That is fine, but it makes it much more involved to implement a version that is economical with respect to renaming only when necessary. Additionally the scoping constraints of SSA are cumbersome and significantly complicate interprocedural analysis (where there is a long history of incorrect proof rules for procedures, and SSA pushes the interprocedural analysis away from being able to use known-good ones). So this diff changes Llair from a functional SSA form to a traditional imperative language. Reviewed By: jvillard Differential Revision: D16905898 fbshipit-source-id: 0fd835220 --- sledge/src/control.ml | 193 ++++++-------- sledge/src/import/import.ml | 1 + sledge/src/import/import.mli | 1 + sledge/src/llair/exp.ml | 1 + sledge/src/llair/exp.mli | 1 + sledge/src/llair/frontend.ml | 371 ++++++++++----------------- sledge/src/llair/llair.ml | 296 +++++++++++---------- sledge/src/llair/llair.mli | 83 +++--- sledge/src/report.ml | 6 +- sledge/src/symbheap/domain.ml | 28 +- sledge/src/symbheap/domain.mli | 7 +- sledge/src/symbheap/exec.ml | 15 +- sledge/src/symbheap/exec.mli | 3 +- sledge/src/symbheap/solver.ml | 2 +- sledge/src/symbheap/state_domain.ml | 58 ++--- sledge/src/symbheap/state_domain.mli | 9 +- 16 files changed, 463 insertions(+), 612 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 47f110303..b3dadf0d1 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -18,14 +18,7 @@ module Stack : sig val empty : t val push_call : - Llair.block - -> retreating:bool - -> bound:int - -> return:Llair.jump - -> Domain.from_call - -> ?throw:Llair.jump - -> t - -> t option + Llair.func Llair.call -> bound:int -> Domain.from_call -> t -> t option val pop_return : t -> (Domain.from_call * Llair.jump * t) option @@ -37,8 +30,7 @@ module Stack : sig end = struct type t = | Return of - { retreating: bool - (** return from a call not known to be nonrecursive *) + { recursive: bool (** return from a possibly-recursive call *) ; dst: Llair.Jump.t ; params: Var.t list ; locals: Var.Set.t @@ -59,8 +51,8 @@ end = struct if x == y then 0 else match (x, y) with - | Return {retreating= true; stk= x}, y - |x, Return {retreating= true; stk= y} -> + | Return {recursive= true; stk= x}, y + |x, Return {recursive= true; stk= y} -> compare_as_inlined_location x y | Return {dst= j; stk= x}, Return {dst= k; stk= y} -> ( match Llair.Jump.compare j k with @@ -77,10 +69,10 @@ end = struct | Empty, Empty -> 0 let rec print_abbrev fs = function - | Return {retreating= false; stk= s} -> + | Return {recursive= false; stk= s} -> print_abbrev fs s ; Format.pp_print_char fs 'R' - | Return {retreating= true; stk= s} -> + | Return {recursive= true; stk= s} -> print_abbrev fs s ; Format.pp_print_string fs "R↑" | Throw (_, s) -> @@ -97,16 +89,16 @@ end = struct let empty = Empty |> check invariant - let push_return ~retreating dst params locals from_call stk = - Return {retreating; dst; params; locals; from_call; stk} + let push_return Llair.{callee= {params; locals}; return; recursive} + from_call stk = + Return {recursive; dst= return; params; locals; from_call; stk} |> check invariant let push_throw jmp stk = (match jmp with None -> stk | Some jmp -> Throw (jmp, stk)) |> check invariant - let push_call (entry : Llair.block) ~retreating ~bound ~return from_call - ?throw stk = + let push_call (Llair.{return; throw} as call) ~bound from_call stk = [%Trace.call fun {pf} -> pf "%a" print_abbrev stk] ; let rec count_f_in_stack acc f = function @@ -118,11 +110,7 @@ end = struct in let n = count_f_in_stack 0 return stk in ( if n > bound then None - else - Some - (push_throw throw - (push_return ~retreating return entry.params entry.parent.locals - from_call stk)) ) + else Some (push_throw throw (push_return call from_call stk)) ) |> [%Trace.retn fun {pf} _ -> pf "%d of %a on stack" n Llair.Jump.pp return] @@ -246,55 +234,52 @@ end = struct | None -> [%Trace.info "queue empty"] ; () end -let exec_goto stk state block ({dst; retreating} : Llair.jump) = +let exec_jump stk state block Llair.{dst; retreating} = Work.add ~prev:block ~retreating stk state dst -let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) = - let state = Domain.jump args dst.params ?temps state in - exec_goto stk state block jmp - let summary_table = Hashtbl.create (module Var) -let exec_call opts stk state block ({dst; args; retreating} : Llair.jump) - (return : Llair.jump) throw globals = +let exec_call opts stk state block call globals = + let Llair.{callee; args; areturn; return; recursive} = call in + let Llair.{name; params; freturn; locals; entry} = callee in [%Trace.call fun {pf} -> - pf "%a from %a" Var.pp dst.parent.name.var Var.pp - return.dst.parent.name.var] + pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var] ; let dnf_states = if opts.function_summaries then Domain.dnf state else [state] in - let locals = dst.parent.locals in - let domain_call = Domain.call args dst.params locals globals in + let domain_call = + Domain.call args areturn params (Set.add_option freturn locals) globals + in List.fold ~init:Work.skip dnf_states ~f:(fun acc state -> - let maybe_summary_post = - if opts.function_summaries then - let state = fst (domain_call ~summaries:false state) in - Hashtbl.find summary_table dst.parent.name.var - >>= List.find_map ~f:(Domain.apply_summary state) - else None - in - [%Trace.info - "Maybe summary post: %a" - (Option.pp "%a" Domain.pp) - maybe_summary_post] ; - match maybe_summary_post with + match + if not opts.function_summaries then None + else + let maybe_summary_post = + let state = fst (domain_call ~summaries:false state) in + Hashtbl.find summary_table name.var + >>= List.find_map ~f:(Domain.apply_summary state) + in + [%Trace.info + "Maybe summary post: %a" + (Option.pp "%a" Domain.pp) + maybe_summary_post] ; + maybe_summary_post + with | None -> let state, from_call = domain_call ~summaries:opts.function_summaries state in Work.seq acc - ( match - Stack.push_call ~bound:opts.bound dst ~retreating ~return - from_call ?throw stk - with - | Some stk -> Work.add stk ~prev:block ~retreating state dst + ( match Stack.push_call call ~bound:opts.bound from_call stk with + | Some stk -> + Work.add stk ~prev:block ~retreating:recursive state entry | None -> Work.skip ) - | Some post -> Work.seq acc (exec_goto stk post block return) ) + | Some post -> Work.seq acc (exec_jump stk post block return) ) |> [%Trace.retn fun {pf} _ -> pf ""] -let pp_st _ = +let pp_st () = [%Trace.printf "@[%t@]" (fun fs -> Hashtbl.iteri summary_table ~f:(fun ~key ~data -> @@ -303,88 +288,72 @@ let pp_st _ = data ) )] let exec_return ~opts stk pre_state (block : Llair.block) exp globals = - [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var] + let Llair.{name; params; freturn; locals} = block.parent in + [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var] ; ( match Stack.pop_return stk with | Some (from_call, retn_site, stk) -> - let freturn = block.parent.freturn in let exit_state = match (freturn, exp) with | Some freturn, Some return_val -> - Domain.exec_return pre_state freturn return_val + Domain.exec_move pre_state freturn return_val | None, None -> pre_state | _ -> violates Llair.Func.invariant block.parent in - let exit_state = + let post_state = Domain.post locals from_call exit_state in + let post_state = if opts.function_summaries then ( let globals = Var.Set.of_vector (Vector.map globals ~f:(fun (g : Global.t) -> g.var)) in - let function_summary, exit_state = - Domain.create_summary ~locals:block.parent.locals exit_state - ~formals: - (Set.union - (Var.Set.of_list block.parent.entry.params) - globals) + let function_summary, post_state = + Domain.create_summary ~locals post_state + ~formals:(Set.union (Var.Set.of_list params) globals) in - Hashtbl.add_multi summary_table ~key:block.parent.name.var + Hashtbl.add_multi summary_table ~key:name.var ~data:function_summary ; pp_st () ; - exit_state ) - else exit_state + post_state ) + else post_state in - let post_state = - Domain.post block.parent.locals from_call exit_state - in - let retn_state = - Domain.retn block.parent.entry.params from_call post_state - in - exec_jump stk retn_state block - ~temps:(Option.fold ~f:Set.add freturn ~init:Var.Set.empty) - ( match freturn with - | Some freturn -> Llair.Jump.push_arg (Exp.var freturn) retn_site - | None -> retn_site ) + let retn_state = Domain.retn params freturn from_call post_state in + exec_jump stk retn_state block retn_site | None -> Work.skip ) |> [%Trace.retn fun {pf} _ -> pf ""] let exec_throw stk pre_state (block : Llair.block) exc = - [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var] + let func = block.parent in + [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var] ; let unwind params scope from_call state = - Domain.retn params from_call (Domain.post scope from_call state) + Domain.retn params (Some func.fthrow) from_call + (Domain.post scope from_call state) in ( match Stack.pop_throw stk ~unwind ~init:pre_state with | Some (from_call, retn_site, stk, unwind_state) -> - let fthrow = block.parent.fthrow in - let exit_state = Domain.exec_return unwind_state fthrow exc in - let post_state = - Domain.post block.parent.locals from_call exit_state - in + let fthrow = func.fthrow in + let exit_state = Domain.exec_move unwind_state fthrow exc in + let post_state = Domain.post func.locals from_call exit_state in let retn_state = - Domain.retn block.parent.entry.params from_call post_state + Domain.retn func.params func.freturn from_call post_state in - exec_jump stk retn_state block - ~temps:(Set.add Var.Set.empty fthrow) - (Llair.Jump.push_arg (Exp.var fthrow) retn_site) + exec_jump stk retn_state block retn_site | None -> Work.skip ) |> [%Trace.retn fun {pf} _ -> pf ""] let exec_skip_func : - Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x = - fun stk state block ({dst; args} as return) -> + Stack.t + -> Domain.t + -> Llair.block + -> Var.t option + -> Llair.jump + -> Work.x = + fun stk state block areturn return -> Report.unknown_call block.term ; - let return = - if List.is_empty dst.params then return - else - let args = - List.fold_right dst.params ~init:args ~f:(fun param args -> - Exp.nondet (Var.name param) :: args ) - in - {return with args} - in + let state = Option.fold ~f:Domain.exec_kill ~init:state areturn in exec_jump stk state block return let exec_term : @@ -417,32 +386,30 @@ let exec_term : with | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) - | Call {call= {dst; args; retreating}; return; throw} -> ( + | Call ({callee; args; areturn; return} as call) -> ( match let lookup name = Option.to_list (Llair.Func.find pgm.functions name) in - Domain.resolve_callee lookup dst state + Domain.resolve_callee lookup callee state with - | [] -> exec_skip_func stk state block return + | [] -> exec_skip_func stk state block areturn return | callees -> List.fold callees ~init:Work.skip ~f:(fun x callee -> ( match Domain.exec_intrinsic ~skip_throw:opts.skip_throw state - (List.hd return.dst.params) - callee.name.var args + areturn callee.name.var args with | Some (Error ()) -> Report.invalid_access_term (Domain.project state) block.term ; Work.skip | Some (Ok state) when Domain.is_false state -> Work.skip - | Some (Ok state) -> exec_goto stk state block return + | Some (Ok state) -> exec_jump stk state block return | None when Llair.Func.is_undefined callee -> - exec_skip_func stk state block return + exec_skip_func stk state block areturn return | None -> - exec_call opts stk state block - {dst= callee.entry; args; retreating} - return throw pgm.globals ) + exec_call opts stk state block {call with callee} + pgm.globals ) |> Work.seq x ) ) | Return {exp} -> exec_return ~opts stk state block exp pgm.globals | Throw {exc} -> @@ -471,13 +438,13 @@ let harness : exec_opts -> Llair.t -> (int -> Work.t) option = List.find_map entry_points ~f:(fun name -> Llair.Func.find pgm.functions (Var.program name) ) |> function - | Some {locals; entry= {params= []} as block} -> + | Some {locals; params= []; entry} -> Some (Work.init (fst - (Domain.call ~summaries:opts.function_summaries [] [] locals - pgm.globals (Domain.init pgm.globals))) - block) + (Domain.call ~summaries:opts.function_summaries [] None [] + locals pgm.globals (Domain.init pgm.globals))) + entry) | _ -> None let exec_pgm : exec_opts -> Llair.t -> unit = diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 32467f953..f28876b77 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -264,6 +264,7 @@ module Set = struct let equal_m__t (module Elt : Compare_m) = equal let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x) let disjoint x y = is_empty (inter x y) + let add_option yo x = Option.fold ~f:add ~init:x yo let add_list ys x = List.fold ~f:add ~init:x ys let diff_inter_diff x y = (diff x y, inter x y, diff y x) let inter_diff x y = (inter x y, diff y x) diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index 18cf60a39..0d80c9536 100644 --- a/sledge/src/import/import.mli +++ b/sledge/src/import/import.mli @@ -212,6 +212,7 @@ module Set : sig val pp : 'e pp -> ('e, 'c) t pp val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool + val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t val diff_inter_diff : diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index c9c01dc5e..08b3d58eb 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -520,6 +520,7 @@ module Var = struct let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs let pp = pp_full ?is_x:None let empty = Set.empty (module T) + let of_option = Option.fold ~f:Set.add ~init:empty let of_list = Set.of_list (module T) let of_vector = Set.of_vector (module T) end diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index f8070f81b..a7edf4a6d 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -99,6 +99,7 @@ module Var : sig val pp_full : ?is_x:(exp -> bool) -> t pp val pp : t pp val empty : t + val of_option : var option -> t val of_list : var list -> t val of_vector : var vector -> t end diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 5a8243c07..ae8b8d6de 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -675,150 +675,49 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype = let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in (i32, xlate_type x tip, cxa_exception) -(** construct the argument of a landingpad block, mainly fix the encoding - scheme for landingpad instruction name to block arg name *) -let landingpad_arg : Llvm.llvalue -> Var.t = - fun instr -> Var.program (find_name instr ^ ".exc") - -(** [rev_map_phis ~f blk] returns [(retn_arg, rev_args, pos)] by rev_mapping - over the prefix of [PHI] instructions at the beginning of [blk]. - [retn_arg], if any, is [f] applied to the [PHI] instruction which takes - the return value of every [Invoke] predecessor of [blk]. [rev_args] is - the result of applying [f] to each of the other [PHI] instructions. - [pos] is the instruction iterator position before the first non-[PHI] - instruction of [blk]. *) -let rev_map_phis : - f:(Llvm.llvalue -> 'a) +(** Translate a control transfer from instruction [instr] to block [dst] to + a jump, if necessary by extending [blocks] with a trampoline containing + the PHIs of [dst] translated to a move. *) +let xlate_jump : + x + -> ?reg_exps:(Var.var * Exp.t) list + -> Llvm.llvalue -> Llvm.llbasicblock - -> 'a option * 'a list * _ Llvm.llpos = - fun ~f blk -> - let rec block_args_ found_invoke_pred retn_arg rev_args pos = - match (pos : _ Llvm.llpos) with - | Before instr -> ( - match Llvm.instr_opcode instr with + -> Loc.t + -> Llair.block list + -> Llair.jump * Llair.block list = + fun x ?(reg_exps = []) instr dst loc blocks -> + let src = Llvm.instr_parent instr in + let rec xlate_jump_ reg_exps (pos : _ Llvm.llpos) = + match pos with + | Before dst_instr -> ( + match Llvm.instr_opcode dst_instr with | PHI -> - (* [has_invoke_pred] holds if some value selected by this PHI is - the return value of an [invoke] instr. [is_retn_arg] holds if - for each predecessor terminated by an invoke instr, this PHI - instr takes the value of the invoke's return value. *) - let has_invoke_pred, is_retn_arg = - List.fold (Llvm.incoming instr) ~init:(false, true) - ~f:(fun (has_invoke_pred, is_retn_arg) (arg, pred) -> - match Llvm.block_terminator pred with - | Some instr -> ( - match Llvm.instr_opcode instr with - | Invoke when Poly.equal arg instr -> (true, is_retn_arg) - | Invoke -> (has_invoke_pred, false) - | _ -> (has_invoke_pred, is_retn_arg) ) - | None -> fail "rev_map_phis: %a" pp_llblock blk () ) - in - if found_invoke_pred && has_invoke_pred then - (* Supporting multiple PHI instructions that take the return - values of invoke instructions will require adding trampolines - for the invoke instructions to return to, that each reorder - arguments and invoke the translation of this block. *) - todo "multiple PHI instructions taking invoke return values: %a" - pp_llblock blk () ; - let retn_arg, rev_args = - if has_invoke_pred && is_retn_arg then (Some (f instr), rev_args) - else (None, f instr :: rev_args) + let reg_exp = + List.find_map_exn (Llvm.incoming dst_instr) + ~f:(fun (arg, pred) -> + if Poly.equal pred src then + Some (xlate_name dst_instr, xlate_value x arg) + else None ) in - block_args_ has_invoke_pred retn_arg rev_args - (Llvm.instr_succ instr) - | LandingPad when Option.is_some retn_arg -> - (* Supporting returning and throwing to the same block, with - different arguments, will require adding trampolines. *) - todo - "return and throw to the same block with different arguments: %a" - pp_llblock blk () - | _ -> (retn_arg, rev_args, pos) ) - | At_end blk -> fail "rev_map_phis: %a" pp_llblock blk () + xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr) + | _ -> reg_exps ) + | At_end blk -> fail "xlate_jump: %a" pp_llblock blk () in - block_args_ false None [] (Llvm.instr_begin blk) - -(** [trampoline_args jump_instr dest_block] is the actual arguments to which - the translation of [dest_block] should be partially-applied, to yield a - trampoline accepting the return parameter of the block and then jumping - with all the args. *) -let trampoline_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list = - fun x jmp dst -> - let src = Llvm.instr_parent jmp in - rev_map_phis dst ~f:(fun instr -> - List.find_map_exn (Llvm.incoming instr) ~f:(fun (arg, pred) -> - if Poly.equal pred src then Some (xlate_value x arg) else None ) - ) - |> snd3 - -(** [unique_pred blk] is the unique predecessor of [blk], or [None] if there - are 0 or >1 predecessors. *) -let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option = - fun blk -> - match Llvm.use_begin (Llvm.value_of_block blk) with - | Some use -> ( - match Llvm.use_succ use with - | None -> Some (Llvm.user use) - | Some _ -> None ) - | None -> None - -(** [return_formal_is_used instr] holds if the return value of [instr] is - used anywhere. *) -let return_formal_is_used : Llvm.llvalue -> bool = - fun instr -> Option.is_some (Llvm.use_begin instr) - -(** [need_return_trampoline instr blk] holds when the return formal of - [instr] is used, but the returned to block [blk] does not take it as an - argument (e.g. if it has multiple predecessors and no PHI node). *) -let need_return_trampoline : Llvm.llvalue -> Llvm.llbasicblock -> bool = - fun instr blk -> - Option.is_none (fst3 (rev_map_phis blk ~f:Fn.id)) - && Option.is_none (unique_pred blk) - && return_formal_is_used instr - -(** [unique_used_invoke_pred blk] is the unique predecessor of [blk], if it - is an [Invoke] instruction, whose return value is used. *) -let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option = - fun blk -> - let is_invoke i = Poly.equal (Llvm.instr_opcode i) Invoke in - match unique_pred blk with - | Some instr when is_invoke instr && return_formal_is_used instr -> - Some instr - | _ -> None - -(** formal parameters accepted by a block *) -let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos = - fun blk -> - let retn_arg, rev_args, pos = rev_map_phis blk ~f:xlate_name in - match pos with - | Before instr -> - let instr_arg = - match Llvm.instr_opcode instr with - | LandingPad -> - assert (Option.is_none retn_arg (* ensured by rev_map_phis *)) ; - Some (landingpad_arg instr) - | _ -> - Option.first_some retn_arg - (Option.map (unique_used_invoke_pred blk) ~f:xlate_name) + let jmp = Llair.Jump.mk (label_of_block dst) in + match xlate_jump_ reg_exps (Llvm.instr_begin dst) with + | [] -> (jmp, blocks) + | reg_exps -> + let mov = + Llair.Inst.move ~reg_exps:(Vector.of_list_rev reg_exps) ~loc in - (Option.cons instr_arg rev_args, pos) - | At_end blk -> fail "block_formals: %a" pp_llblock blk () - -(** actual arguments passed by a jump to a block *) -let jump_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list = - fun x jmp dst -> - let src = Llvm.instr_parent jmp in - let retn_arg, rev_args, _ = - rev_map_phis dst ~f:(fun phi -> - Option.value_exn - (List.find_map (Llvm.incoming phi) ~f:(fun (arg, pred) -> - if Poly.equal pred src then Some (xlate_value x arg) - else None )) ) - in - let retn_arg = - Option.first_some retn_arg - (Option.map (unique_used_invoke_pred dst) ~f:(fun invoke -> - Exp.var (xlate_name invoke) )) - in - Option.cons retn_arg rev_args + let lbl = find_name instr ^ ".jmp" in + let blk = + Llair.Block.mk ~lbl + ~cmnd:(Vector.of_array [|mov|]) + ~term:(Llair.Term.goto ~dst:jmp ~loc) + in + (Llair.Jump.mk lbl, blk :: blocks) (** An LLVM instruction is translated to a sequence of LLAIR instructions and a terminator, plus some additional blocks to which it may refer @@ -1025,24 +924,21 @@ let xlate_instr : List.rev_init num_args ~f:(fun i -> xlate_value x (Llvm.operand instr i) ) in - let return = Llair.Jump.mk lbl [] in - Llair.Term.call ~func ~typ ~args ~loc ~return ~throw:None - ~ignore_result:false + let areturn = xlate_name_opt instr in + let return = Llair.Jump.mk lbl in + Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw:None + ~ignore_result:false ~loc in - let params = Option.to_list (xlate_name_opt instr) in continue (fun (insts, term) -> let cmnd = Vector.of_list insts in - ([], call, [Llair.Block.mk ~lbl ~params ~cmnd ~term]) ) ) + ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) ) | Invoke -> ( - let reg = xlate_name_opt instr in let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in let lltyp = Llvm.type_of llfunc in assert (Poly.(Llvm.classify_type lltyp = Pointer)) ; let fname = Llvm.value_name llfunc in let return_blk = Llvm.get_normal_dest instr in - let return_dst = label_of_block return_blk in let unwind_blk = Llvm.get_unwind_dest instr in - let unwind_dst = label_of_block unwind_blk in let num_args = if not (Llvm.is_var_arg (Llvm.element_type lltyp)) then Llvm.num_arg_operands instr @@ -1058,15 +954,15 @@ let xlate_instr : List.rev_init num_args ~f:(fun i -> xlate_value x (Llvm.operand instr i) ) in + let areturn = xlate_name_opt instr in (* intrinsics *) match String.split fname ~on:'.' with | _ when Option.is_some (xlate_intrinsic_exp fname) -> - let arg = Option.to_list (Option.map ~f:Exp.var reg) in - let dst = Llair.Jump.mk return_dst arg in - emit_term (Llair.Term.goto ~dst ~loc) + let dst, blocks = xlate_jump x instr return_blk loc [] in + emit_term (Llair.Term.goto ~dst ~loc) ~blocks | ["__llair_throw"] -> - let dst = Llair.Jump.mk unwind_dst args in - emit_term (Llair.Term.goto ~dst ~loc) + let dst, blocks = xlate_jump x instr unwind_blk loc [] in + emit_term (Llair.Term.goto ~dst ~loc) ~blocks | ["abort"] -> emit_term ~prefix:[Llair.Inst.abort ~loc] Llair.Term.unreachable | ["_Znwm" (* operator new(size_t num) *)] @@ -1077,11 +973,11 @@ let xlate_instr : let num = xlate_value x (Llvm.operand instr 0) in let llt = Llvm.type_of instr in let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in - let args = jump_args x instr return_blk in - let dst = Llair.Jump.mk return_dst args in + let dst, blocks = xlate_jump x instr return_blk loc [] in emit_term ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc] (Llair.Term.goto ~dst ~loc) + ~blocks (* unimplemented *) | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ -> todo "statepoints:@ %a" pp_llvalue instr () @@ -1089,37 +985,18 @@ let xlate_instr : | _ -> let func = xlate_func_name x llfunc in let typ = xlate_type x (Llvm.type_of llfunc) in + let return, blocks = xlate_jump x instr return_blk loc [] in + let throw, blocks = xlate_jump x instr unwind_blk loc blocks in + let throw = Some throw in let ignore_result = match typ with | Pointer {elt= Function {return= Some _}} -> - not (return_formal_is_used instr) + Option.is_none (Llvm.use_begin instr) | _ -> false in - let return, blocks = - let args = trampoline_args x instr return_blk in - if not (need_return_trampoline instr return_blk) then - (Llair.Jump.mk return_dst args, []) - else - let lbl = name ^ ".ret" in - let block = - let params = [xlate_name instr] in - let cmnd = Vector.empty in - let term = - let dst = Llair.Jump.mk return_dst args in - Llair.Term.goto ~dst ~loc - in - Llair.Block.mk ~lbl ~params ~cmnd ~term - in - (Llair.Jump.mk lbl [], [block]) - in - let throw = - let dst = unwind_dst in - let args = trampoline_args x instr unwind_blk in - Some (Llair.Jump.mk dst args) - in emit_term - (Llair.Term.call ~func ~typ ~args ~loc ~return ~throw - ~ignore_result) + (Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw + ~ignore_result ~loc) ~blocks ) | Ret -> let exp = @@ -1130,61 +1007,53 @@ let xlate_instr : | Br -> ( match Option.value_exn (Llvm.get_branch instr) with | `Unconditional blk -> - let args = jump_args x instr blk in - let dst = Llair.Jump.mk (label_of_block blk) args in - emit_term (Llair.Term.goto ~dst ~loc) + let dst, blocks = xlate_jump x instr blk loc [] in + emit_term (Llair.Term.goto ~dst ~loc) ~blocks | `Conditional (cnd, thn, els) -> let key = xlate_value x cnd in - let thn_lbl = label_of_block thn in - let thn_args = jump_args x instr thn in - let thn = Llair.Jump.mk thn_lbl thn_args in - let els_lbl = label_of_block els in - let els_args = jump_args x instr els in - let els = Llair.Jump.mk els_lbl els_args in - emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ) + let thn, blocks = xlate_jump x instr thn loc [] in + let els, blocks = xlate_jump x instr els loc blocks in + emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks + ) | Switch -> let key = xlate_value x (Llvm.operand instr 0) in - let cases = + let cases, blocks = let num_cases = (Llvm.num_operands instr / 2) - 1 in - let rec xlate_cases i = + let rec xlate_cases i blocks = if i <= num_cases then let idx = Llvm.operand instr (2 * i) in let blk = Llvm.block_of_value (Llvm.operand instr ((2 * i) + 1)) in let num = xlate_value x idx in - let dst = label_of_block blk in - let args = jump_args x instr blk in - let rest = xlate_cases (i + 1) in - (num, Llair.Jump.mk dst args) :: rest - else [] + let jmp, blocks = xlate_jump x instr blk loc blocks in + let rest, blocks = xlate_cases (i + 1) blocks in + ((num, jmp) :: rest, blocks) + else ([], blocks) in - xlate_cases 1 + xlate_cases 1 [] in let tbl = Vector.of_list cases in let blk = Llvm.block_of_value (Llvm.operand instr 1) in - let dst = label_of_block blk in - let args = jump_args x instr blk in - let els = Llair.Jump.mk dst args in - emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) + let els, blocks = xlate_jump x instr blk loc blocks in + emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks | IndirectBr -> let ptr = xlate_value x (Llvm.operand instr 0) in let num_dests = Llvm.num_operands instr - 1 in - let lldests = - let rec dests i = + let lldests, blocks = + let rec dests i blocks = if i <= num_dests then let v = Llvm.operand instr i in let blk = Llvm.block_of_value v in - let dst = label_of_block blk in - let args = jump_args x instr blk in - let rest = dests (i + 1) in - Llair.Jump.mk dst args :: rest - else [] + let jmp, blocks = xlate_jump x instr blk loc blocks in + let rest, blocks = dests (i + 1) blocks in + (jmp :: rest, blocks) + else ([], blocks) in - dests 1 + dests 1 [] in let tbl = Vector.of_list lldests in - emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) + emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks | LandingPad -> (* Translate the landingpad clauses to code to load the type_info from the thrown exception, and test the type_info against the clauses, @@ -1192,7 +1061,7 @@ let xlate_instr : passing a value for the selector which the handler code tests to e.g. either cleanup or rethrow. *) let i32, tip, cxa_exception = landingpad_typs x instr in - let exc = Exp.var (landingpad_arg instr) in + let exc = Exp.var (Var.program (find_name instr ^ ".exc")) in let ti = Var.program (name ^ ".ti") in (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *) let load_ti = @@ -1213,33 +1082,44 @@ let xlate_instr : let typeid = xlate_llvm_eh_typeid_for x tip ti in let lbl = name ^ ".unwind" in let param = xlate_name instr in - let params = [param] in - let jump_unwind sel = - let dst = lbl in - let args = [Exp.record [exc; sel]] in - Llair.Jump.mk dst args + let jump_unwind i sel rev_blocks = + let arg = Exp.record [exc; sel] in + let mov = + Llair.Inst.move ~reg_exps:(Vector.of_array [|(param, arg)|]) ~loc + in + let lbl = lbl ^ "." ^ Int.to_string i in + let blk = + Llair.Block.mk ~lbl + ~cmnd:(Vector.of_array [|mov|]) + ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc) + in + (Llair.Jump.mk lbl, blk :: rev_blocks) in - let goto_unwind sel = - let dst = jump_unwind sel in - Llair.Term.goto ~dst ~loc + let goto_unwind i sel blocks = + let dst, blocks = jump_unwind i sel blocks in + (Llair.Term.goto ~dst ~loc, blocks) in let term_unwind, rev_blocks = if Llvm.is_cleanup instr then - (goto_unwind (Exp.integer Z.zero i32), []) + goto_unwind 0 (Exp.integer Z.zero i32) [] else let num_clauses = Llvm.num_operands instr in let lbl i = name ^ "." ^ Int.to_string i in - let jump i = Llair.Jump.mk (lbl i) [] in + let jump i = Llair.Jump.mk (lbl i) in let block i term = - Llair.Block.mk ~lbl:(lbl i) ~params:[] ~cmnd:Vector.empty ~term + Llair.Block.mk ~lbl:(lbl i) ~cmnd:Vector.empty ~term in - let match_filter = - jump_unwind (Exp.sub i32 (Exp.integer Z.zero i32) typeid) + let match_filter i rev_blocks = + jump_unwind i + (Exp.sub i32 (Exp.integer Z.zero i32) typeid) + rev_blocks in - let xlate_clause i = + let xlate_clause i rev_blocks = let clause = Llvm.operand instr i in let num_tis = Llvm.num_operands clause in - if num_tis = 0 then Llair.Term.goto ~dst:match_filter ~loc + if num_tis = 0 then + let dst, rev_blocks = match_filter i rev_blocks in + (Llair.Term.goto ~dst ~loc, rev_blocks) else match Llvm.classify_type (Llvm.type_of clause) with | Array (* filter *) -> ( @@ -1252,30 +1132,32 @@ let xlate_instr : else Exp.dq tiI ti in let key = xlate_filter 0 in - Llair.Term.branch ~loc ~key ~nzero:match_filter - ~zero:(jump (i + 1)) + let nzero, rev_blocks = match_filter i rev_blocks in + ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + , rev_blocks ) | _ -> fail "xlate_instr: %a" pp_llvalue instr () ) | _ (* catch *) -> let clause = xlate_value x clause in let key = Exp.or_ (Exp.eq clause Exp.null) (Exp.eq clause ti) in - Llair.Term.branch ~loc ~key ~nzero:(jump_unwind typeid) - ~zero:(jump (i + 1)) + let nzero, rev_blocks = jump_unwind i typeid rev_blocks in + ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1)) + , rev_blocks ) in let rec rev_blocks i z = if i < num_clauses then - rev_blocks (i + 1) (block i (xlate_clause i) :: z) + let term, z = xlate_clause i z in + rev_blocks (i + 1) (block i term :: z) else block i Llair.Term.unreachable :: z in - (xlate_clause 0, rev_blocks 1 []) + xlate_clause 0 (rev_blocks 1 []) in continue (fun (insts, term) -> ( [load_ti] , term_unwind , List.rev_append rev_blocks - [ Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts) - ~term ] ) ) + [Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term] ) ) | Resume -> let rcd = xlate_value x (Llvm.operand instr 0) in let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero Typ.siz) in @@ -1298,6 +1180,18 @@ let xlate_instr : fail "xlate_instr: %a" pp_llvalue instr () | PHI | Invalid | Invalid2 | UserOp1 | UserOp2 -> assert false +let skip_phis : Llvm.llbasicblock -> _ Llvm.llpos = + fun blk -> + let rec skip_phis_ (pos : _ Llvm.llpos) = + match pos with + | Before instr -> ( + match Llvm.instr_opcode instr with + | PHI -> skip_phis_ (Llvm.instr_succ instr) + | _ -> pos ) + | _ -> pos + in + skip_phis_ (Llvm.instr_begin blk) + let rec xlate_instrs : pop_thunk -> x -> _ Llvm.llpos -> code = fun pop x -> function | Before instrI -> @@ -1313,9 +1207,9 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list = [%Trace.call fun {pf} -> pf "%a" pp_llblock blk] ; let lbl = label_of_block blk in - let params, pos = block_formals blk in + let pos = skip_phis blk in let insts, term, blocks = xlate_instrs pop x pos in - Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts) ~term :: blocks + Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term :: blocks |> [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl] @@ -1341,8 +1235,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = in let entry = let {Llair.lbl; cmnd; term} = entry_block in - assert (List.is_empty entry_block.params) ; - Llair.Block.mk ~lbl ~params ~cmnd ~term + Llair.Block.mk ~lbl ~cmnd ~term in let cfg = let rec trav_blocks rev_cfg prev = @@ -1355,7 +1248,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = in trav_blocks (List.rev entry_blocks) entry_blk in - Llair.Func.mk ~name ~entry ~cfg + Llair.Func.mk ~name ~params ~entry ~cfg | At_end _ -> report_undefined llf name ; Llair.Func.mk_undefined ~name ~params ) diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index a0aadf903..146cb06b2 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -5,7 +5,9 @@ * LICENSE file in the root directory of this source tree. *) -(** Translation units *) +(** LLAIR (Low-Level Analysis Internal Representation) *) + +[@@@warning "+9"] type inst = | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t} @@ -23,29 +25,29 @@ type inst = type cmnd = inst vector [@@deriving sexp] type label = string [@@deriving sexp] -type 'a control_transfer = - {mutable dst: 'a; args: Exp.t list; mutable retreating: bool} -[@@deriving compare, equal, sexp_of] +type jump = {mutable dst: block; mutable retreating: bool} -type jump = block control_transfer +and 'a call = + { callee: 'a + ; typ: Typ.t + ; args: Exp.t list + ; areturn: Var.t option + ; return: jump + ; throw: jump option + ; ignore_result: bool + ; mutable recursive: bool + ; loc: Loc.t } and term = | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t} | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t} - | Call of - { call: Exp.t control_transfer - ; typ: Typ.t - ; return: jump - ; throw: jump option - ; ignore_result: bool - ; loc: Loc.t } + | Call of Exp.t call | Return of {exp: Exp.t option; loc: Loc.t} | Throw of {exc: Exp.t; loc: Loc.t} | Unreachable and block = { lbl: label - ; params: Var.t list ; cmnd: cmnd ; term: term ; mutable parent: func @@ -53,15 +55,15 @@ and block = and cfg = block vector -(* [entry] is not part of [cfg] since it is special in several ways: its - params are the func params, and it cannot be jumped to, only called. *) +(* [entry] is not part of [cfg] since it cannot be jumped to, only called. *) and func = { name: Global.t + ; params: Var.t list + ; freturn: Var.t option + ; fthrow: Var.t ; locals: Var.Set.t ; entry: block - ; cfg: cfg - ; freturn: Var.t option - ; fthrow: Var.t } + ; cfg: cfg } let sexp_cons (hd : Sexp.t) (tl : Sexp.t) = match tl with @@ -70,8 +72,8 @@ let sexp_cons (hd : Sexp.t) (tl : Sexp.t) = let sexp_ctor label args = sexp_cons (Sexp.Atom label) args -let sexp_of_jump {dst; args; retreating} = - [%sexp {dst: label = dst.lbl; args: Exp.t list; retreating: bool}] +let sexp_of_jump {dst; retreating} = + [%sexp {dst: label = dst.lbl; retreating: bool}] let sexp_of_term = function | Switch {key; tbl; els; loc} -> @@ -80,24 +82,35 @@ let sexp_of_term = function {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}] | Iswitch {ptr; tbl; loc} -> sexp_ctor "Iswitch" [%sexp {ptr: Exp.t; tbl: jump vector; loc: Loc.t}] - | Call {call; typ; return; throw; ignore_result; loc} -> + | Call + { callee + ; typ + ; args + ; areturn + ; return + ; throw + ; ignore_result + ; recursive + ; loc } -> sexp_ctor "Call" [%sexp - { call: Exp.t control_transfer + { callee: Exp.t ; typ: Typ.t + ; args: Exp.t list + ; areturn: Var.t option ; return: jump ; throw: jump option ; ignore_result: bool + ; recursive: bool ; loc: Loc.t }] | Return {exp; loc} -> sexp_ctor "Return" [%sexp {exp: Exp.t option; loc: Loc.t}] | Throw {exc; loc} -> sexp_ctor "Throw" [%sexp {exc: Exp.t; loc: Loc.t}] | Unreachable -> Sexp.Atom "Unreachable" -let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} = +let sexp_of_block {lbl; cmnd; term; parent; sort_index} = [%sexp { lbl: label - ; params: Var.t list ; cmnd: cmnd ; term: term ; parent: Var.t = parent.name.var @@ -105,8 +118,15 @@ let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} = let sexp_of_cfg v = [%sexp_of: block vector] v -let sexp_of_func {name; locals; entry; cfg} = - [%sexp {name: Global.t; locals: Var.Set.t; entry: block; cfg: cfg}] +let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} = + [%sexp + { name: Global.t + ; params: Var.t list + ; freturn: Var.t option + ; fthrow: Var.t + ; locals: Var.Set.t + ; entry: block + ; cfg: cfg }] (* blocks in a [t] are uniquely identified by [sort_index] *) let compare_block x y = Int.compare x.sort_index y.sort_index @@ -125,7 +145,7 @@ let pp_inst fs inst = pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs (Vector.pp ",@ " Exp.pp) exps Loc.pp loc | Load {reg; ptr; len; loc} -> - pf "@[<2>load %a@ %a@ %a;@]\t%a" Exp.pp len Var.pp reg Exp.pp ptr + pf "@[<2>%a@ := load %a@ %a;@]\t%a" Var.pp reg Exp.pp len Exp.pp ptr Loc.pp loc | Store {ptr; exp; len; loc} -> pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp @@ -140,12 +160,13 @@ let pp_inst fs inst = pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src Loc.pp loc | Alloc {reg; num; len; loc} -> - pf "@[<2>alloc %a@ [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp len - Loc.pp loc + pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp + len Loc.pp loc | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc | Nondet {reg; msg; loc} -> - pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg - Loc.pp loc + pf "@[<2>%anondet \"%s\";@]\t%a" + (Option.pp "%a := " Var.pp) + reg msg Loc.pp loc | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc let pp_args pp_arg fs args = @@ -153,10 +174,10 @@ let pp_args pp_arg fs args = let pp_param fs var = Var.pp fs var -let pp_jump fs {dst= {lbl}; args; retreating} = - Format.fprintf fs "@[<2>%s%%%s%a@]" +let pp_jump fs {dst; retreating} = + Format.fprintf fs "@[<2>%s%%%s@]" (if retreating then "↑" else "") - lbl (pp_args Exp.pp) args + dst.lbl let pp_term fs term = let pf pp = Format.fprintf fs pp in @@ -175,13 +196,15 @@ let pp_term fs term = tbl pp_goto els Loc.pp loc ) | Iswitch {ptr; tbl; loc} -> pf "@[<2>iswitch %a@ @[%a@]@]\t%a" Exp.pp ptr - (Vector.pp "@ " (fun fs ({dst= {lbl}; _} as jmp) -> - Format.fprintf fs "%s: %a" lbl pp_goto jmp )) + (Vector.pp "@ " (fun fs jmp -> + Format.fprintf fs "%s: %a" jmp.dst.lbl pp_goto jmp )) tbl Loc.pp loc - | Call {call= {dst; args; retreating}; return; throw; loc} -> - pf "@[<2>@[<7>call @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a" - (if retreating then "↑" else "") - Exp.pp dst (pp_args Exp.pp) args pp_jump return + | Call {callee; args; areturn; return; throw; recursive; loc; _} -> + pf "@[<2>@[<7>%acall @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a" + (Option.pp "%a := " Var.pp) + areturn + (if recursive then "↑" else "") + Exp.pp callee (pp_args Exp.pp) args pp_jump return (Option.pp "@ throwto %a" pp_jump) throw Loc.pp loc | Return {exp; loc} -> @@ -191,9 +214,9 @@ let pp_term fs term = let pp_cmnd = Vector.pp "@ " pp_inst -let pp_block fs {lbl; params; cmnd; term; sort_index} = - Format.fprintf fs "@[@[<4>%s%a@]: #%i@ @[%a%t%a@]@]" lbl - (pp_args pp_param) params sort_index pp_cmnd cmnd +let pp_block fs {lbl; cmnd; term; parent= _; sort_index} = + Format.fprintf fs "@[%s: #%i@ @[%a%t%a@]@]" lbl sort_index pp_cmnd + cmnd (fun fs -> if Vector.is_empty cmnd then () else Format.fprintf fs "@ ") pp_term term @@ -201,7 +224,6 @@ let pp_block fs {lbl; params; cmnd; term; sort_index} = let rec dummy_block = { lbl= "dummy" - ; params= [] ; cmnd= Vector.empty ; term= Unreachable ; parent= dummy_func @@ -211,11 +233,12 @@ and dummy_func = let dummy_var = Var.program "dummy" in let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in { name= Global.mk dummy_var dummy_ptr_typ Loc.none + ; params= [] + ; freturn= None + ; fthrow= dummy_var ; locals= Var.Set.empty ; entry= dummy_block - ; cfg= Vector.empty - ; freturn= None - ; fthrow= dummy_var } + ; cfg= Vector.empty } (** Instructions *) @@ -235,25 +258,26 @@ module Inst = struct let abort ~loc = Abort {loc} let loc = function - | Move {loc} - |Load {loc} - |Store {loc} - |Memset {loc} - |Memcpy {loc} - |Memmov {loc} - |Alloc {loc} - |Free {loc} - |Nondet {loc} - |Abort {loc} -> + | Move {loc; _} + |Load {loc; _} + |Store {loc; _} + |Memset {loc; _} + |Memcpy {loc; _} + |Memmov {loc; _} + |Alloc {loc; _} + |Free {loc; _} + |Nondet {loc; _} + |Abort {loc; _} -> loc let union_locals inst vs = match inst with - | Move {reg_exps} -> + | Move {reg_exps; _} -> Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps - | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} -> Set.add vs reg + | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} -> + Set.add vs reg | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ - |Nondet {reg= None} + |Nondet {reg= None; _} |Abort _ -> vs @@ -265,26 +289,10 @@ end module Jump = struct type t = jump [@@deriving sexp_of] - let compare = compare_control_transfer compare_block - let equal = equal_control_transfer equal_block + let compare x y = compare_block x.dst y.dst + let equal x y = equal_block x.dst y.dst let pp = pp_jump - - let invariant ?(accept_return = false) jmp = - Invariant.invariant [%here] (jmp, accept_return) [%sexp_of: t * bool] - @@ fun () -> - let {dst= {params; parent}; args} = jmp in - if parent == dummy_func then - (* jmp not yet backpatched by Func.mk *) - assert true - else - assert ( - List.length params = List.length args + Bool.to_int accept_return ) - - let mk lbl args = - {dst= {dummy_block with lbl}; args; retreating= false} - |> check invariant - - let push_arg arg jmp = {jmp with args= arg :: jmp.args} + let mk lbl = {dst= {dummy_block with lbl}; retreating= false} end (** Basic-Block Terminators *) @@ -298,19 +306,14 @@ module Term = struct Invariant.invariant [%here] term [%sexp_of: t] @@ fun () -> match term with - | Switch {tbl; els} -> - Vector.iter tbl ~f:(fun (_, jmp) -> Jump.invariant jmp) ; - Jump.invariant els - | Iswitch {tbl} -> Vector.iter tbl ~f:Jump.invariant - | Call {call= {args= actls}; typ; return; throw; ignore_result} -> ( + | Switch _ | Iswitch _ -> assert true + | Call {typ; args= actls; areturn; _} -> ( match typ with - | Pointer {elt= Function {args= frmls; return= retn_typ}} -> + | Pointer {elt= Function {args= frmls; return= retn_typ; _}} -> assert (Vector.length frmls = List.length actls) ; - Jump.invariant return - ~accept_return:(Option.is_some retn_typ && not ignore_result) ; - Option.iter throw ~f:(Jump.invariant ~accept_return:true) + assert (Option.is_some retn_typ || Option.is_none areturn) | _ -> assert false ) - | Return {exp} -> ( + | Return {exp; _} -> ( match parent with | Some parent -> assert (Bool.(Option.is_some exp = Option.is_some parent.freturn)) @@ -331,19 +334,36 @@ module Term = struct let iswitch ~ptr ~tbl ~loc = Iswitch {ptr; tbl; loc} |> check invariant - let call ~func ~typ ~args ~return ~throw ~ignore_result ~loc = - let call = {dst= func; args; retreating= false} in - Call {call; typ; return; throw; ignore_result; loc} |> check invariant + let call ~func ~typ ~args ~areturn ~return ~throw ~ignore_result ~loc = + Call + { callee= func + ; typ + ; args + ; areturn + ; return + ; throw + ; ignore_result + ; recursive= false + ; loc } + |> check invariant let return ~exp ~loc = Return {exp; loc} |> check invariant let throw ~exc ~loc = Throw {exc; loc} |> check invariant let unreachable = Unreachable |> check invariant let loc = function - | Switch {loc} | Iswitch {loc} | Call {loc} | Return {loc} | Throw {loc} - -> + | Switch {loc; _} + |Iswitch {loc; _} + |Call {loc; _} + |Return {loc; _} + |Throw {loc; _} -> loc | Unreachable -> Loc.none + + let union_locals term vs = + match term with + | Call {areturn; _} -> Set.add_option areturn vs + | _ -> vs end (** Basic-Blocks *) @@ -355,19 +375,12 @@ module Block = struct let pp = pp_block - let invariant blk = - Invariant.invariant [%here] blk [%sexp_of: t] - @@ fun () -> - assert (not (List.contains_dup blk.params ~compare:Var.compare)) - - let mk ~lbl ~params ~cmnd ~term = + let mk ~lbl ~cmnd ~term = { lbl - ; params ; cmnd ; term ; parent= dummy_block.parent ; sort_index= dummy_block.sort_index } - |> check invariant end (** Functions *) @@ -376,16 +389,25 @@ module Func = struct type t = func [@@deriving sexp_of] let is_undefined = function - | {entry= {cmnd; term= Unreachable}} -> Vector.is_empty cmnd + | {entry= {cmnd; term= Unreachable; _}; _} -> Vector.is_empty cmnd | _ -> false - let pp fs ({name; entry= {params; cmnd; term; sort_index}; cfg} as func) = + let pp fs + ( { name + ; params + ; freturn + ; fthrow= _ + ; locals= _ + ; entry= {cmnd; term; sort_index; _} + ; cfg } as func ) = let pp_if cnd str fs = if cnd then Format.fprintf fs str in - Format.fprintf fs "@[@[%a@[<2>%a%a@]%t@]" (Option.pp "%a " Typ.pp) + Format.fprintf fs "@[@[%a%a@[<2>%a%a@]%t@]" + (Option.pp "%a " Typ.pp) ( match name.typ with - | Pointer {elt= Function {return}} -> return + | Pointer {elt= Function {return; _}} -> return | _ -> None ) - Global.pp name (pp_args pp_param) params + (Option.pp " %a := " Var.pp) + freturn Global.pp name (pp_args pp_param) params (fun fs -> if is_undefined func then Format.fprintf fs " #%i@]" sort_index else @@ -395,57 +417,51 @@ module Func = struct (Vector.pp "@\n@\n " Block.pp) cfg ) - let fold_term {entry= {term}; cfg} ~init ~f = - Vector.fold cfg ~init:(f init term) ~f:(fun a {term} -> f a term) + let fold_term {entry; cfg; _} ~init ~f = + Vector.fold cfg ~init:(f init entry.term) ~f:(fun a blk -> f a blk.term) - let iter_term {entry= {term}; cfg} ~f = - f term ; - Vector.iter cfg ~f:(fun {term} -> f term) + let iter_term {entry; cfg; _} ~f = + f entry.term ; + Vector.iter cfg ~f:(fun blk -> f blk.term) let invariant func = Invariant.invariant [%here] func [%sexp_of: t] @@ fun () -> assert (func == func.entry.parent) ; - let {name= {typ}; entry; cfg} = func in + let {name= {typ; _}; cfg; _} = func in match typ with - | Pointer {elt= Function {return}} -> + | Pointer {elt= Function {return; _}} -> assert ( not (Vector.contains_dup cfg ~compare:(fun b1 b2 -> String.compare b1.lbl b2.lbl )) ) ; - assert ( - not - (List.contains_dup - (List.concat_map (entry :: Vector.to_list cfg) ~f:(fun blk -> - blk.params )) - ~compare:Var.compare) ) ; assert (Bool.(Option.is_some return = Option.is_some func.freturn)) ; iter_term func ~f:(fun term -> Term.invariant ~parent:func term) | _ -> assert false let find functions name = Map.find functions name - let mk ~(name : Global.t) ~entry ~cfg = + let mk ~(name : Global.t) ~params ~entry ~cfg = let locals = let locals_cmnd locals cmnd = Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals in let locals_block locals block = - Set.add_list block.params (locals_cmnd locals block.cmnd) + locals_cmnd (Term.union_locals block.term locals) block.cmnd in - let init = locals_cmnd Var.Set.empty entry.cmnd in + let init = locals_block Var.Set.empty entry in Vector.fold ~f:locals_block cfg ~init in - let wrt = Set.add_list entry.params locals in + let wrt = Set.add_list params locals in let freturn, wrt = match name.typ with - | Pointer {elt= Function {return= Some _}} -> + | Pointer {elt= Function {return= Some _; _}} -> let freturn, wrt = Var.fresh "freturn" ~wrt in (Some freturn, wrt) | _ -> (None, wrt) in let fthrow, _ = Var.fresh "fthrow" ~wrt in - let func = {name; locals; entry; cfg; freturn; fthrow} in + let func = {name; params; freturn; fthrow; locals; entry; cfg} in let resolve_parent_and_jumps block = block.parent <- func ; let lookup cfg lbl : block = @@ -453,11 +469,11 @@ module Func = struct in let set_dst jmp = jmp.dst <- lookup cfg jmp.dst.lbl in match block.term with - | Switch {tbl; els} -> + | Switch {tbl; els; _} -> Vector.iter tbl ~f:(fun (_, jmp) -> set_dst jmp) ; set_dst els - | Iswitch {tbl} -> Vector.iter tbl ~f:set_dst - | Call {return; throw} -> + | Iswitch {tbl; _} -> Vector.iter tbl ~f:set_dst + | Call {return; throw; _} -> set_dst return ; Option.iter throw ~f:set_dst | Return _ | Throw _ | Unreachable -> () @@ -468,10 +484,10 @@ module Func = struct let mk_undefined ~name ~params = let entry = - Block.mk ~lbl:"" ~params ~cmnd:Vector.empty ~term:Term.unreachable + Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable in let cfg = Vector.empty in - mk ~name ~entry ~cfg + mk ~name ~entry ~params ~cfg end (** Derived meta-data *) @@ -509,8 +525,8 @@ let set_derived_metadata functions = FuncQ.enqueue_back_exn roots func.name.var func ) ; Map.iter functions ~f:(fun func -> Func.fold_term func ~init:() ~f:(fun () -> function - | Call {call= {dst}} -> ( - match Var.of_exp dst with + | Call {callee; _} -> ( + match Var.of_exp callee with | Some callee -> FuncQ.remove roots callee |> (ignore : [> ] -> unit) | None -> () ) @@ -528,18 +544,18 @@ let set_derived_metadata functions = else visit ancestors func jmp.dst in ( match src.term with - | Switch {tbl; els} -> + | Switch {tbl; els; _} -> Vector.iter tbl ~f:(fun (_, jmp) -> jump jmp) ; jump els - | Iswitch {tbl} -> Vector.iter tbl ~f:jump - | Call {call= {dst} as call; return; throw} -> - ( match Var.of_exp dst >>= Func.find functions with + | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump + | Call ({callee; return; throw; _} as call) -> + ( match Var.of_exp callee >>= Func.find functions with | Some func -> - if Set.mem ancestors func.entry then call.retreating <- true + if Set.mem ancestors func.entry then call.recursive <- true else visit ancestors func func.entry | None -> (* conservatively assume all virtual calls are recursive *) - call.retreating <- true ) ; + call.recursive <- true ) ; jump return ; Option.iter ~f:jump throw | Return _ | Throw _ | Unreachable -> () ) ; BlockQ.enqueue_back_exn tips_to_roots src () @@ -555,7 +571,7 @@ let set_derived_metadata functions = index := !index - 1 ) in let sort_cfgs functions = - Map.iter functions ~f:(fun {cfg} -> + Map.iter functions ~f:(fun {cfg; _} -> Array.sort ~compare:(fun x y -> Int.compare x.sort_index y.sort_index) (Vector.to_array cfg) ) diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 715ec4543..1addff835 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -5,28 +5,8 @@ * LICENSE file in the root directory of this source tree. *) -(** Translation units - - LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for - static analysis using a low-level model of memory. Compared to a - compiler IR such as LLVM, an analyzer does not need to perform register - allocation, instruction selection, code generation, etc. or even much - code transformation, so the constraints on the IR are very different. - - LLAIR is a "Functional SSA" form where control transfers pass arguments - instead of using ϕ-nodes. An analyzer will need good support for - parameter passing anyhow, and ϕ-nodes make it hard to express program - properties as predicates on states, since some execution history is - needed to evaluate ϕ instructions. An alternative view is that the scope - of variables [reg] assigned in instructions such as [Load] is the - successor block as well as all blocks the instruction dominates in the - control-flow graph. This language is first-order, and a term structure - for the code constituting the scope of variables is not needed, so SSA - rather than full CPS suffices. - - Additionally, the focus on memory analysis leads to a design where the - arithmetic and logic operations are not "instructions" but instead are - complex expressions (see [Exp]) that refer to registers (see [Var]). *) +(** LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for + static analysis using a low-level model of memory. *) (** Instructions for memory manipulation or other non-control effects. *) type inst = private @@ -61,15 +41,21 @@ type cmnd = inst vector (** A label is a name of a block. *) type label = string -(** A jump with arguments. *) -type 'a control_transfer = - { mutable dst: 'a - ; args: Exp.t list (** Stack of arguments, first-arg-last *) - ; mutable retreating: bool - (** Holds if [dst] is an ancestor in a depth-first traversal. *) } - -(** A jump with arguments to a block. *) -type jump = block control_transfer +(** A jump to a block. *) +type jump = {mutable dst: block; mutable retreating: bool} + +(** A call to a function. *) +and 'a call = + { callee: 'a + ; typ: Typ.t (** Type of the callee. *) + ; args: Exp.t list (** Stack of arguments, first-arg-last. *) + ; areturn: Var.t option (** Register to receive return value. *) + ; return: jump (** Return destination. *) + ; throw: jump option (** Handler destination. *) + ; ignore_result: bool (** Drop return value when invoking return. *) + ; mutable recursive: bool + (** Holds unless [callee] is definitely not recursive. *) + ; loc: Loc.t } (** Block terminators for function call/return or other control transfers. *) and term = private @@ -78,14 +64,8 @@ and term = private [case] which is equal to [key], if any, otherwise invoke [els]. *) | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t} (** Invoke the [jump] in [tbl] whose [dst] is equal to [ptr]. *) - | Call of - { call: Exp.t control_transfer (** A [global] for non-virtual call. *) - ; typ: Typ.t (** Type of the callee. *) - ; return: jump (** Return destination or trampoline. *) - ; throw: jump option (** Handler destination or trampoline. *) - ; ignore_result: bool (** Drop return value when invoking return. *) - ; loc: Loc.t } - (** Call function [call.dst] with arguments [call.args]. *) + | Call of Exp.t call + (** Call function with arguments. A [global] for non-virtual call. *) | Return of {exp: Exp.t option; loc: Loc.t} (** Invoke [return] of the dynamically most recent [Call]. *) | Throw of {exc: Exp.t; loc: Loc.t} @@ -97,7 +77,6 @@ and term = private (** A block is a destination of a jump with arguments, contains code. *) and block = private { lbl: label - ; params: Var.t list (** Formal parameters, first-param-last stack *) ; cmnd: cmnd ; term: term ; mutable parent: func @@ -111,11 +90,12 @@ and cfg parameters are the function parameters. *) and func = private { name: Global.t + ; params: Var.t list (** Formal parameters, first-param-last stack *) + ; freturn: Var.t option + ; fthrow: Var.t ; locals: Var.Set.t (** Local variables *) ; entry: block - ; cfg: cfg - ; freturn: Var.t option - ; fthrow: Var.t } + ; cfg: cfg } type functions @@ -151,8 +131,7 @@ module Jump : sig type t = jump [@@deriving compare, equal, sexp_of] val pp : jump pp - val mk : string -> Exp.t list -> jump - val push_arg : Exp.t -> jump -> jump + val mk : string -> jump end module Term : sig @@ -175,6 +154,7 @@ module Term : sig func:Exp.t -> typ:Typ.t -> args:Exp.t list + -> areturn:Var.t option -> return:jump -> throw:jump option -> ignore_result:bool @@ -193,10 +173,7 @@ module Block : sig include Comparator.S with type t := t val pp : t pp - - include Invariant.S with type t := t - - val mk : lbl:label -> params:Var.t list -> cmnd:cmnd -> term:term -> block + val mk : lbl:label -> cmnd:cmnd -> term:term -> block end module Func : sig @@ -206,7 +183,13 @@ module Func : sig include Invariant.S with type t := t - val mk : name:Global.t -> entry:block -> cfg:block vector -> func + val mk : + name:Global.t + -> params:Var.t list + -> entry:block + -> cfg:block vector + -> func + val mk_undefined : name:Global.t -> params:Var.t list -> t val find : functions -> Var.t -> func option diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 3a5ae8d28..8324f16e0 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -15,10 +15,10 @@ let unknown_call call = call (fun fs (call : Llair.Term.t) -> match call with - | Call {call= {dst}} -> ( - match Var.of_exp dst with + | Call {callee} -> ( + match Var.of_exp callee with | Some var -> Var.pp_demangled fs var - | None -> Exp.pp fs dst ) + | None -> Exp.pp fs callee ) | _ -> () ) call Llair.Term.pp call] diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index a639b3841..dcd25398e 100644 --- a/sledge/src/symbheap/domain.ml +++ b/sledge/src/symbheap/domain.ml @@ -29,17 +29,21 @@ let exec_assume (entry, current) cnd = | Some current -> Some (entry, current) | None -> None +let exec_kill (entry, current) reg = + (entry, State_domain.exec_kill current reg) + +let exec_move (entry, current) formal actual = + (entry, State_domain.exec_move current formal actual) + let exec_inst (entry, current) inst = match State_domain.exec_inst current inst with | Ok current -> Ok (entry, current) | Error e -> Error e -let exec_return (entry, current) formal actual = - (entry, State_domain.exec_return current formal actual) - -let exec_intrinsic ~skip_throw (entry, current) result intrinsic actuals = +let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals = match - State_domain.exec_intrinsic ~skip_throw current result intrinsic actuals + State_domain.exec_intrinsic ~skip_throw current areturn intrinsic + actuals with | None -> None | Some (Ok current) -> Some (Ok (entry, current)) @@ -49,11 +53,8 @@ type from_call = {state_from_call: State_domain.from_call; caller_entry: State_domain.t} [@@deriving sexp_of] -let jump actuals formals ?temps (entry, current) = - let current, _ = State_domain.jump actuals formals ?temps current in - (entry, current) - -let call ~summaries actuals formals locals globals_vec (entry, current) = +let call ~summaries actuals areturn formals locals globals_vec + (entry, current) = let globals = Var.Set.of_vector (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) @@ -67,7 +68,8 @@ let call ~summaries actuals formals locals globals_vec (entry, current) = State_domain.pp current] ; let caller_current, state_from_call = - State_domain.call ~summaries actuals formals locals globals current + State_domain.call ~summaries actuals areturn formals locals globals + current in ((caller_current, caller_current), {state_from_call; caller_entry= entry})) |> @@ -80,10 +82,10 @@ let post locals {caller_entry} (_, current) = |> [%Trace.retn fun {pf} -> pf "@,%a" pp] -let retn formals {caller_entry; state_from_call} (_, current) = +let retn formals freturn {caller_entry; state_from_call} (_, current) = [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current] ; - (caller_entry, State_domain.retn formals state_from_call current) + (caller_entry, State_domain.retn formals freturn state_from_call current) |> [%Trace.retn fun {pf} -> pf "@,%a" pp] diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index 581d3e124..5fc8bd2ef 100644 --- a/sledge/src/symbheap/domain.mli +++ b/sledge/src/symbheap/domain.mli @@ -15,8 +15,9 @@ val init : Global.t vector -> t val join : t -> t -> t val is_false : t -> bool val exec_assume : t -> Exp.t -> t option +val exec_kill : t -> Var.t -> t +val exec_move : t -> Var.t -> Exp.t -> t val exec_inst : t -> Llair.inst -> (t, unit) result -val exec_return : t -> Var.t -> Exp.t -> t val exec_intrinsic : skip_throw:bool @@ -37,11 +38,11 @@ val create_summary : -> State_domain.function_summary * t val apply_summary : t -> State_domain.function_summary -> t option -val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t val call : summaries:bool -> Exp.t list + -> Var.t option -> Var.t list -> Var.Set.t -> Global.t vector @@ -49,7 +50,7 @@ val call : -> t * from_call val post : Var.Set.t -> from_call -> t -> t -val retn : Var.t list -> from_call -> t -> t +val retn : Var.t list -> Var.t option -> from_call -> t -> t val dnf : t -> t list val resolve_callee : diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index a83cca4bf..3b33e3d46 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -52,7 +52,6 @@ let assume pre cnd = if Sh.is_false post then None else Some post let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre -let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre (* { emp } * rs := es @@ -670,10 +669,10 @@ let exec_spec pre {xs; foot; sub; ms; post} = Format.fprintf fs "%a := " Var.Set.pp ms ) ms Sh.pp post ; assert ( - let vs = Set.diff (Set.diff foot.Sh.us xs) pre.Sh.us in + let vs = Set.diff (Set.diff foot.us xs) pre.us in Set.is_empty vs || Trace.fail "unbound foot: {%a}" Var.Set.pp vs ) ; assert ( - let vs = Set.diff (Set.diff post.Sh.us xs) pre.Sh.us in + let vs = Set.diff (Set.diff post.us xs) pre.us in Set.is_empty vs || Trace.fail "unbound post: {%a}" Var.Set.pp vs )] ; let foot = Sh.extend_us xs foot in @@ -698,6 +697,10 @@ let rec exec_specs pre = function exec_specs pre specs >>| fun posts -> Sh.or_ post posts | [] -> Ok (Sh.false_ pre.us) +let move pre reg exp = + exec_spec pre (move_spec pre.us (Vector.of_array [|(reg, exp)|])) + |> function Ok post -> post | _ -> assert false + let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result = fun pre inst -> [%Trace.info @@ -727,18 +730,18 @@ let intrinsic ~skip_throw : -> Var.t -> Exp.t list -> (Sh.t, unit) result option = - fun pre result intrinsic actuals -> + fun pre areturn intrinsic actuals -> [%Trace.info "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]" (Option.pp "%a := " Var.pp) - result Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals) + areturn Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals) Sh.pp pre] ; let us = pre.us in let name = let n = Var.name intrinsic in match String.index n '.' with None -> n | Some i -> String.prefix n i in - match (result, name, actuals) with + match (areturn, name, actuals) with (* * cstdlib - memory management *) diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index 2bedae2a1..c379acc39 100644 --- a/sledge/src/symbheap/exec.mli +++ b/sledge/src/symbheap/exec.mli @@ -8,7 +8,8 @@ (** Symbolic Execution *) val assume : Sh.t -> Exp.t -> Sh.t option -val return : Sh.t -> Var.t -> Exp.t -> Sh.t +val kill : Sh.t -> Var.t -> Sh.t +val move : Sh.t -> Var.t -> Exp.t -> Sh.t val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result val intrinsic : diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index ecfb1db45..68ecaceb3 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -61,7 +61,7 @@ let single_existential_occurrence xs exp = with Multiple_existential_occurrences -> Many let special_cases xs = function - | Exp.(App {op= App {op= Eq; arg= Var _}; arg= Var _}) as e -> + | Exp.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e -> if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e | e -> e diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index f3bbac686..86a32746e 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -27,7 +27,8 @@ let init globals = let join = Sh.or_ let is_false = Sh.is_false let exec_assume = Exec.assume -let exec_return = Exec.return +let exec_kill = Exec.kill +let exec_move = Exec.move let exec_inst = Exec.inst let exec_intrinsic = Exec.intrinsic let dnf = Sh.dnf @@ -66,46 +67,22 @@ let garbage_collect (q : t) ~wrt = |> [%Trace.retn fun {pf} -> pf "%a" pp] -type from_call = {subst: Var.Subst.t; frame: Sh.t} +type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t} [@@deriving compare, equal, sexp] -(** Express formula in terms of formals instead of actuals, and enter scope - of locals: rename formals to fresh vars in formula and actuals, add - equations between each formal and actual, and quantify the temps and - fresh vars. *) -let jump actuals formals ?temps q = - [%Trace.call fun {pf} -> - pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ q: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Sh.pp q] - ; - let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in - let and_eq q formal actual = - let actual' = Exp.rename freshen_locals actual in - Sh.and_ (Exp.eq (Exp.var formal) actual') q - in - let and_eqs formals actuals q = - List.fold2_exn ~f:and_eq formals actuals ~init:q - in - ( Option.fold ~f:(Fn.flip Sh.exists) temps - ~init:(and_eqs formals actuals q') - , {subst= freshen_locals; frame= Sh.emp} ) - |> - [%Trace.retn fun {pf} (q', {subst}) -> - pf "@[subst: %a@ q': %a@]" Var.Subst.pp subst Sh.pp q'] - (** Express formula in terms of formals instead of actuals, and enter scope of locals: rename formals to fresh vars in formula and actuals, add equations between each formal and actual, and quantify fresh vars. *) -let call ~summaries actuals formals locals globals q = +let call ~summaries actuals areturn formals locals globals q = [%Trace.call fun {pf} -> pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]" (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) (List.rev formals) Var.Set.pp locals pp q] ; - let wrt = Set.add_list formals locals in - let q', freshen_locals = Sh.freshen q ~wrt in + let q', freshen_locals = + Sh.freshen q ~wrt:(Set.add_list formals locals) + in let and_eq q formal actual = let actual' = Exp.rename freshen_locals actual in Sh.and_ (Exp.eq (Exp.var formal) actual') q @@ -116,7 +93,7 @@ let call ~summaries actuals formals locals globals q = let q'' = and_eqs formals actuals q' in ( if not summaries then let q'' = Sh.extend_us locals q'' in - (q'', {subst= freshen_locals; frame= Sh.emp}) + (q'', {areturn; subst= freshen_locals; frame= Sh.emp}) else let formals_set = Var.Set.of_list formals in (* Add the formals here to do garbage collection and then get rid of @@ -134,7 +111,7 @@ let call ~summaries actuals formals locals globals q = ~message:"Solver couldn't infer frame of a garbage-collected pre" in let q'' = Sh.extend_us locals (and_eqs formals actuals foot) in - (q'', {subst= freshen_locals; frame}) ) + (q'', {areturn; subst= freshen_locals; frame}) ) |> [%Trace.retn fun {pf} (q', {subst; frame}) -> pf "@[subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp @@ -152,13 +129,19 @@ let post locals q = (** Express in terms of actuals instead of formals: existentially quantify formals, and apply inverse of fresh variables for formals renaming to restore the shadowed variables. *) -let retn formals {subst; frame} q = +let retn formals freturn {areturn; subst; frame} q = [%Trace.call fun {pf} -> pf "@[formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]" (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] ; - let q = Sh.exists (Var.Set.of_list formals) q in + let q = + match (areturn, freturn) with + | Some areturn, Some freturn -> exec_move q areturn (Exp.var freturn) + | Some areturn, None -> exec_kill q areturn + | _ -> q + in + let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in let q = Sh.rename (Var.Subst.invert subst) q in Sh.star frame q |> @@ -175,13 +158,12 @@ let pp_function_summary fs {xs; foot; post} = Format.fprintf fs "@[xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs pp foot pp post -let create_summary ~locals ~formals ~entry ~current = +let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = [%Trace.call fun {pf} -> pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp - current] + post] ; let foot = Sh.exists locals entry in - let post = Sh.exists locals current in let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in let restore_formals q = Set.fold formals ~init:q ~f:(fun q var -> @@ -199,7 +181,7 @@ let create_summary ~locals ~formals ~entry ~current = let xs_and_formals = Set.union xs formals in let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in let post = Sh.exists (Set.diff post.us xs_and_formals) post in - let current = Sh.extend_us xs current in + let current = Sh.extend_us xs post in ({xs; foot; post}, current) |> [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_function_summary fs] diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index fb7e044d5..e9ec91468 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/sledge/src/symbheap/state_domain.mli @@ -14,8 +14,9 @@ val init : Global.t vector -> t val join : t -> t -> t val is_false : t -> bool val exec_assume : t -> Exp.t -> t option +val exec_kill : t -> Var.t -> t +val exec_move : t -> Var.t -> Exp.t -> t val exec_inst : t -> Llair.inst -> (t, unit) result -val exec_return : t -> Var.t -> Exp.t -> t val exec_intrinsic : skip_throw:bool @@ -27,12 +28,10 @@ val exec_intrinsic : type from_call [@@deriving compare, equal, sexp] -val jump : - Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t * from_call - val call : summaries:bool -> Exp.t list + -> Var.t option -> Var.t list -> Var.Set.t -> Var.Set.t @@ -54,7 +53,7 @@ val create_summary : -> function_summary * t val post : Var.Set.t -> t -> t -val retn : Var.t list -> from_call -> t -> t +val retn : Var.t list -> Var.t option -> from_call -> t -> t val dnf : t -> t list val resolve_callee :