-
Notifications
You must be signed in to change notification settings - Fork 87
Move extern inits, global inits and otherfuns spawning into constraint system #178
Copy link
Copy link
Open
Labels
cleanupRefactoring, clean-upRefactoring, clean-up
Description
Currently extern inits, global inits and otherfuns spawning is done by manually simulating transfer function calls with degenerate ctx:
analyzer/src/framework/control.ml
Lines 175 to 349 in 20f3a7d
| (* add extern variables to local state *) | |
| let do_extern_inits ctx (file : file) : Spec.D.t = | |
| let module VS = Set.Make (Basetype.Variables) in | |
| let add_glob s = function | |
| GVar (v,_,_) -> VS.add v s | |
| | _ -> s | |
| in | |
| let vars = foldGlobals file add_glob VS.empty in | |
| let set_bad v st = | |
| Spec.assign {ctx with local = st} (var v) MyCFG.unknown_exp | |
| in | |
| let add_externs s = function | |
| | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) -> set_bad v s | |
| | _ -> s | |
| in | |
| foldGlobals file add_externs (Spec.startstate MyCFG.dummy_func.svar) | |
| in | |
| (* analyze cil's global-inits function to get a starting state *) | |
| let do_global_inits (file: file) : Spec.D.t * fundec list * (varinfo * Spec.G.t) list = | |
| (* Simulate globals before analysis. *) | |
| (* TODO: make extern/global inits part of constraint system so all of this would be unnecessary. *) | |
| let gh = GHT.create 13 in | |
| let getg v = GHT.find_default gh v (Spec.G.bot ()) in | |
| let sideg v d = GHT.replace gh v (Spec.G.join (getg v) d) in | |
| (* Old-style global function for context. | |
| * This indirectly prevents global initializers from depending on each others' global side effects, which would require proper solving. *) | |
| let getg v = Spec.G.bot () in | |
| let ctx = | |
| { ask = (fun _ -> Queries.Result.top ()) | |
| ; node = MyCFG.dummy_node | |
| ; prev_node = MyCFG.dummy_node | |
| ; control_context = Obj.repr (fun () -> ctx_failwith "Global initializers have no context.") | |
| ; context = (fun () -> ctx_failwith "Global initializers have no context.") | |
| ; edge = MyCFG.Skip | |
| ; local = Spec.D.top () | |
| ; global = getg | |
| ; presub = [] | |
| ; postsub = [] | |
| ; spawn = (fun _ -> failwith "Global initializers should never spawn threads. What is going on?") | |
| ; split = (fun _ -> failwith "Global initializers trying to split paths.") | |
| ; sideg = sideg | |
| ; assign = (fun ?name _ -> failwith "Global initializers trying to assign.") | |
| } | |
| in | |
| let edges = MyCFG.getGlobalInits file in | |
| if (get_bool "dbg.verbose") then print_endline ("Executing "^string_of_int (List.length edges)^" assigns."); | |
| let funs = ref [] in | |
| (*let count = ref 0 in*) | |
| let transfer_func (st : Spec.D.t) (edge, loc) : Spec.D.t = | |
| if M.tracing then M.trace "con" "Initializer %a\n" d_loc loc; | |
| (*incr count; | |
| if (get_bool "dbg.verbose")&& (!count mod 1000 = 0) then Printf.printf "%d %!" !count; *) | |
| Tracing.current_loc := loc; | |
| match edge with | |
| | MyCFG.Entry func -> | |
| if M.tracing then M.trace "global_inits" "Entry %a\n" d_lval (var func.svar); | |
| Spec.body {ctx with local = st} func | |
| | MyCFG.Assign (lval,exp) -> | |
| if M.tracing then M.trace "global_inits" "Assign %a = %a\n" d_lval lval d_exp exp; | |
| (match lval, exp with | |
| | (Var v,o), (AddrOf (Var f,NoOffset)) | |
| when v.vstorage <> Static && isFunctionType f.vtype -> | |
| (try funs := Cilfacade.getdec f :: !funs with Not_found -> ()) | |
| | _ -> () | |
| ); | |
| Spec.assign {ctx with local = st} lval exp | |
| | _ -> failwith "Unsupported global initializer edge" | |
| in | |
| let with_externs = do_extern_inits ctx file in | |
| (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges); *) | |
| let result : Spec.D.t = List.fold_left transfer_func with_externs edges in | |
| result, !funs, GHT.to_list gh | |
| in | |
| let print_globals glob = | |
| let out = M.get_out (Spec.name ()) !GU.out in | |
| let print_one v st = | |
| ignore (Pretty.fprintf out "%a -> %a\n" EQSys.GVar.pretty_trace v Spec.G.pretty st) | |
| in | |
| GHT.iter print_one glob | |
| in | |
| (* real beginning of the [analyze] function *) | |
| if get_bool "ana.sv-comp.enabled" then | |
| WResult.init file; (* TODO: move this out of analyze_loop *) | |
| GU.global_initialization := true; | |
| GU.earlyglobs := false; | |
| Spec.init (); | |
| Access.init file; | |
| let test_domain (module D: Lattice.S): unit = | |
| let module DP = DomainProperties.All (D) in | |
| ignore (Pretty.printf "domain testing...: %s\n" (D.name ())); | |
| let errcode = QCheck_base_runner.run_tests DP.tests in | |
| if (errcode <> 0) then | |
| failwith "domain tests failed" | |
| in | |
| let _ = | |
| if (get_bool "dbg.test.domain") then ( | |
| ignore (Pretty.printf "domain testing analysis...: %s\n" (Spec.name ())); | |
| test_domain (module Spec.D); | |
| test_domain (module Spec.G); | |
| ) | |
| in | |
| let startstate, more_funs, entrystates_global = | |
| if (get_bool "dbg.verbose") then print_endline ("Initializing "^string_of_int (MyCFG.numGlobals file)^" globals."); | |
| Stats.time "global_inits" do_global_inits file | |
| in | |
| let otherfuns = if get_bool "kernel" then otherfuns @ more_funs else otherfuns in | |
| let enter_with st fd = | |
| let st = st fd.svar in | |
| let ctx = | |
| { ask = (fun _ -> Queries.Result.top ()) | |
| ; node = MyCFG.dummy_node | |
| ; prev_node = MyCFG.dummy_node | |
| ; control_context = Obj.repr (fun () -> ctx_failwith "enter_func has no context.") | |
| ; context = (fun () -> ctx_failwith "enter_func has no context.") | |
| ; edge = MyCFG.Skip | |
| ; local = st | |
| ; global = (fun _ -> Spec.G.bot ()) | |
| ; presub = [] | |
| ; postsub = [] | |
| ; spawn = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; sideg = (fun _ -> failwith "Bug3: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; assign = (fun ?name _ -> failwith "Bug4: Using enter_func for toplevel functions with 'otherstate'.") | |
| } | |
| in | |
| let args = List.map (fun x -> MyCFG.unknown_exp) fd.sformals in | |
| let ents = Spec.enter ctx None fd.svar args in | |
| List.map (fun (_,s) -> fd.svar, s) ents | |
| in | |
| (try MyCFG.dummy_func.svar.vdecl <- (List.hd otherfuns).svar.vdecl with Failure _ -> ()); | |
| let startvars = | |
| if startfuns = [] | |
| then [[MyCFG.dummy_func.svar, startstate]] | |
| else | |
| let morph f = Spec.morphstate f startstate in | |
| List.map (enter_with morph) startfuns | |
| in | |
| let exitvars = List.map (enter_with Spec.exitstate) exitfuns in | |
| let otherstate st v = | |
| let ctx = | |
| { ask = (fun _ -> Queries.Result.top ()) | |
| ; node = MyCFG.dummy_node | |
| ; prev_node = MyCFG.dummy_node | |
| ; control_context = Obj.repr (fun () -> ctx_failwith "enter_func has no context.") | |
| ; context = (fun () -> ctx_failwith "enter_func has no context.") | |
| ; edge = MyCFG.Skip | |
| ; local = st | |
| ; global = (fun _ -> Spec.G.bot ()) | |
| ; presub = [] | |
| ; postsub = [] | |
| ; spawn = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; split = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; sideg = (fun _ -> failwith "Bug3: Using enter_func for toplevel functions with 'otherstate'.") | |
| ; assign = (fun ?name _ -> failwith "Bug4: Using enter_func for toplevel functions with 'otherstate'.") | |
| } | |
| in | |
| Spec.threadenter ctx None v [] | |
| (* TODO: do threadspawn to mainfuns? *) | |
| in | |
| let prestartstate = Spec.startstate MyCFG.dummy_func.svar in (* like in do_extern_inits *) | |
| let othervars = List.map (enter_with (otherstate prestartstate)) otherfuns in | |
| let startvars = List.concat (startvars @ exitvars @ othervars) in | |
| if startvars = [] then | |
| failwith "BUG: Empty set of start variables; may happen if enter_func of any analysis returns an empty list."; |
In my experience, time and time again, this has been causing issues because:
1.ctxs are degenerate – some outright crash, others have behavior which doesn't match the one available during solving;
2. it somewhat duplicates what FromSpec does;
3. it misses some nontrivial things that would happen during actual solving – e.g. main is unaware of otherfuns having been spawned at all;
4. it's extremely error prone and hard to maintain.
The sensible thing would be to do all these things within the constraint system and let the solver evaluate them.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
cleanupRefactoring, clean-upRefactoring, clean-up