diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 2347f9a17..bd6961623 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -391,32 +391,31 @@ module Make (Dom : Domain_sig.Dom) = struct | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) | Call ({callee; args; areturn; return} as call) -> ( - match let lookup name = Option.to_list (Llair.Func.find pgm.functions name) in - Dom.resolve_callee lookup callee state - with - | [] -> exec_skip_func stk state block areturn return - | callees -> - List.fold callees ~init:Work.skip ~f:(fun x callee -> - ( match - Dom.exec_intrinsic ~skip_throw:opts.skip_throw state - areturn callee.name.var args - with - | Some (Error ()) -> - Report.invalid_access_term - (Dom.report_fmt_thunk state) - block.term ; - Work.skip - | Some (Ok state) when Dom.is_false state -> Work.skip - | Some (Ok state) -> exec_jump stk state block return - | None when Llair.Func.is_undefined callee -> - exec_skip_func stk state block areturn return - | None -> - exec_call opts stk state block {call with callee} - pgm.globals ) - |> Work.seq x ) ) + let callees, state = Dom.resolve_callee lookup callee state in + match callees with + | [] -> exec_skip_func stk state block areturn return + | callees -> + List.fold callees ~init:Work.skip ~f:(fun x callee -> + ( match + Dom.exec_intrinsic ~skip_throw:opts.skip_throw state + areturn callee.name.var args + with + | Some (Error ()) -> + Report.invalid_access_term + (Dom.report_fmt_thunk state) + block.term ; + Work.skip + | Some (Ok state) when Dom.is_false state -> Work.skip + | Some (Ok state) -> exec_jump stk state block return + | None when Llair.Func.is_undefined callee -> + exec_skip_func stk state block areturn return + | None -> + 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} -> if opts.skip_throw then Work.skip diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index d4ef69d50..a645dcdde 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -44,7 +44,7 @@ module type Dom = sig val dnf : t -> t list val resolve_callee : - (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list + (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list * t type summary diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 99749cdff..2834c38a4 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -107,8 +107,9 @@ module Make (State_domain : State_domain_sig) = struct let dnf (entry, current) = List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current) - let resolve_callee f e (_, current) = - State_domain.resolve_callee f e current + let resolve_callee f e (entry, current) = + let callees, current = State_domain.resolve_callee f e current in + (callees, (entry, current)) type summary = State_domain.summary diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index 8fa8eca83..660c1fe21 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -27,10 +27,10 @@ let post _ _ () = () let retn _ _ _ _ = () let dnf () = [()] -let resolve_callee lookup ptr _ = +let resolve_callee lookup ptr () = match Var.of_exp ptr with - | Some callee_name -> lookup callee_name - | None -> [] + | Some callee_name -> (lookup callee_name, ()) + | None -> ([], ()) type summary = unit diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index cbd7813d2..68e7f3966 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -33,16 +33,14 @@ let exec_kill st _ = st let exec_move st _ rhs = used_globals ~init:st rhs let exec_inst st inst = - [%Trace.call fun {pf} -> pf "{%a} %a { ? }" pp st Llair.Inst.pp inst] + [%Trace.call fun {pf} -> pf "pre:{%a} %a" pp st Llair.Inst.pp inst] ; Ok (Llair.Inst.fold_exps inst ~init:st ~f:(fun acc e -> used_globals ~init:acc e )) |> - [%Trace.retn fun {pf} res -> - match res with - | Ok uses -> pf "new uses: %a" pp (Set.diff uses st) - | _ -> ()] + [%Trace.retn fun {pf} -> + Result.iter ~f:(fun uses -> pf "post:{%a}" pp uses)] let exec_intrinsic ~skip_throw:_ st _ _ actuals = List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a) @@ -54,10 +52,11 @@ type from_call = t [@@deriving sexp_of] let call ~summaries:_ actuals _ _ _ _ st = (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a)) -let resolve_callee lookup ptr _ = +let resolve_callee lookup ptr st = + let st = used_globals ~init:st ptr in match Var.of_exp ptr with - | Some callee_name -> lookup callee_name - | None -> [] + | Some callee_name -> (lookup callee_name, st) + | None -> ([], st) (* A function summary is the set of global variables accessed by that function and its transitive callees *) diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 17063e307..5024c005a 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -155,10 +155,10 @@ let retn formals freturn {areturn; subst; frame} q = |> [%Trace.retn fun {pf} -> pf "%a" pp] -let resolve_callee lookup ptr _ = +let resolve_callee lookup ptr st = match Var.of_exp ptr with - | Some callee_name -> lookup callee_name - | None -> [] + | Some callee_name -> (lookup callee_name, st) + | None -> ([], st) type summary = {xs: Var.Set.t; foot: t; post: t}