|
(* 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."; |
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
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
FromSpecdoes;3. it misses some nontrivial things that would happen during actual solving – e.g.
mainis 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.