From 266da15b5e73076ac82a433892222512e80314a4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Nov 2020 13:15:46 +0200 Subject: [PATCH] Collect thread spawns instead of doing them immediately (issue #148) --- src/analyses/arinc.ml | 2 +- src/analyses/base.ml | 3 +- src/analyses/condVars.ml | 2 +- src/analyses/contain.ml | 2 +- src/analyses/deadlock.ml | 2 +- src/analyses/expRelation.ml | 2 +- src/analyses/extract_arinc.ml | 2 +- src/analyses/extract_osek.ml | 2 +- src/analyses/fileUse.ml | 2 +- src/analyses/flag.ml | 2 +- src/analyses/flagModes.ml | 2 +- src/analyses/mallocWrapperAnalysis.ml | 2 +- src/analyses/malloc_null.ml | 2 +- src/analyses/mayLocks.ml | 2 +- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/octagon.ml | 2 +- src/analyses/osek.ml | 2 +- src/analyses/osektransactionality.ml | 2 +- src/analyses/poly.ml | 2 +- src/analyses/region.ml | 2 +- src/analyses/shapes.ml | 2 +- src/analyses/spec.ml | 2 +- src/analyses/stackTrace.ml | 4 +- src/analyses/symbLocks.ml | 2 +- src/analyses/termination.ml | 2 +- src/analyses/threadAnalysis.ml | 6 +- src/analyses/threadEscape.ml | 15 ++--- src/analyses/threadFlag.ml | 4 +- src/analyses/threadId.ml | 2 +- src/analyses/threadReturn.ml | 2 +- src/analyses/uninit.ml | 2 +- src/analyses/unit.ml | 2 +- src/analyses/varEq.ml | 2 +- src/framework/constraints.ml | 79 +++++++++++++++++---------- src/witness/observerAnalysis.ml | 2 +- src/witness/witnessConstraints.ml | 2 +- 36 files changed, 100 insertions(+), 71 deletions(-) diff --git a/src/analyses/arinc.ml b/src/analyses/arinc.ml index eb73ba563c..f64360792d 100644 --- a/src/analyses/arinc.ml +++ b/src/analyses/arinc.ml @@ -665,7 +665,7 @@ struct let f_d = snd (Tasks.choose tasks_f) in { f_d with pre = d.pre } - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local end let _ = diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c1d4d3b2e7..89e64582f3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2034,7 +2034,7 @@ struct end (* handling thread creations *) | `ThreadCreate _ -> - D.bot () (* actual results joined via threadspawn *) + ctx.local (* actual results joined via threadspawn *) (* handling thread joins... sort of *) | `ThreadJoin (id,ret_var) -> begin match (eval_rv ctx.ask gs st ret_var) with @@ -2184,6 +2184,7 @@ struct ctx.local let threadspawn ctx (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t = + (* D.join ctx.local @@ *) match lval with | Some lval -> begin match ThreadId.get_current fctx.ask with diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 7f45088b59..aeacfe00fc 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -144,7 +144,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () end diff --git a/src/analyses/contain.ml b/src/analyses/contain.ml index 42a93e283a..a4e38ce261 100644 --- a/src/analyses/contain.ml +++ b/src/analyses/contain.ml @@ -806,7 +806,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () end diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index a8cc3b9d9f..9824c5b70d 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -53,7 +53,7 @@ struct (* Some required states *) let startstate _ : D.t = D.empty () let threadenter ctx lval f args : D.t = D.empty () - let threadspawn ctx lval f args fctx = D.empty () + let threadspawn ctx lval f args fctx = ctx.local let exitstate _ : D.t = D.empty () (* ======== Transfer functions ======== *) diff --git a/src/analyses/expRelation.ml b/src/analyses/expRelation.ml index 64681f7529..0e4650e108 100644 --- a/src/analyses/expRelation.ml +++ b/src/analyses/expRelation.ml @@ -113,7 +113,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end diff --git a/src/analyses/extract_arinc.ml b/src/analyses/extract_arinc.ml index cb1bd152d5..e470620d8c 100644 --- a/src/analyses/extract_arinc.ml +++ b/src/analyses/extract_arinc.ml @@ -401,7 +401,7 @@ struct let f_d = snd (Tasks.choose tasks_f) in f_d - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local end let _ = diff --git a/src/analyses/extract_osek.ml b/src/analyses/extract_osek.ml index a6dfc0e7c2..fabdfa8477 100644 --- a/src/analyses/extract_osek.ml +++ b/src/analyses/extract_osek.ml @@ -318,7 +318,7 @@ struct let startstate v = Pid.of_int 0L, Ctx.top (), Pred.of_node (MyCFG.Function (emptyFunction "main").svar) let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () let init () = (* registers which functions to extract and writes out their definitions *) diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml index 2a2828baef..84d9f526fc 100644 --- a/src/analyses/fileUse.ml +++ b/src/analyses/fileUse.ml @@ -297,7 +297,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () end diff --git a/src/analyses/flag.ml b/src/analyses/flag.ml index b7de4b853c..c95926c56e 100644 --- a/src/analyses/flag.ml +++ b/src/analyses/flag.ml @@ -127,7 +127,7 @@ struct let startstate v = D.top () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () let name () = "flag" diff --git a/src/analyses/flagModes.ml b/src/analyses/flagModes.ml index 7c4a62ead6..9c2fb506df 100644 --- a/src/analyses/flagModes.ml +++ b/src/analyses/flagModes.ml @@ -131,7 +131,7 @@ struct let startstate v = D.top () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 8761f941b8..8a133d5de8 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -52,7 +52,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () let heap_hash = Hashtbl.create 113 diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml index 719477435e..ca89ce4da4 100644 --- a/src/analyses/malloc_null.ml +++ b/src/analyses/malloc_null.ml @@ -226,7 +226,7 @@ struct let startstate v = D.empty () let threadenter ctx lval f args = D.empty () - let threadspawn ctx lval f args fctx = D.empty () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.empty () let init () = diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 5adff33223..ed746c9192 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -70,7 +70,7 @@ struct let startstate v = D.empty () let threadenter ctx lval f args = D.empty () - let threadspawn ctx lval f args fctx = D.empty () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index ccbb2abe82..bf02aee69a 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -226,7 +226,7 @@ struct (** We just lift start state, global and dependency functions: *) let startstate v = Lockset.empty () let threadenter ctx lval f args = Lockset.empty () - let threadspawn ctx lval f args fctx = Lockset.empty () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = Lockset.empty () let query ctx (q:Queries.t) : Queries.Result.t = diff --git a/src/analyses/octagon.ml b/src/analyses/octagon.ml index bd10e14196..9921004f45 100644 --- a/src/analyses/octagon.ml +++ b/src/analyses/octagon.ml @@ -371,7 +371,7 @@ struct else `Top | _ -> Queries.Result.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local end diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index 45461e0644..ea092bc2bb 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -714,7 +714,7 @@ struct let exitstate v = D.top () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let activate_task ctx (task_name : string) : unit = let task = Cilfacade.getFun task_name in diff --git a/src/analyses/osektransactionality.ml b/src/analyses/osektransactionality.ml index 142b8e3964..b012ce1aa1 100644 --- a/src/analyses/osektransactionality.ml +++ b/src/analyses/osektransactionality.ml @@ -115,7 +115,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () (** Finalization and other result printing functions: *) diff --git a/src/analyses/poly.ml b/src/analyses/poly.ml index 9c6c7e36b0..c2af61d067 100644 --- a/src/analyses/poly.ml +++ b/src/analyses/poly.ml @@ -20,7 +20,7 @@ struct let context x = if GobConfig.get_bool "exp.full-context" then x else D.bot () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate _ = D.top () let startstate _ = D.top () diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 518e2e58bf..eafb7bdfec 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -176,7 +176,7 @@ struct let threadenter ctx lval f args = `Lifted (RegMap.bot ()) - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = `Lifted (RegMap.bot ()) diff --git a/src/analyses/shapes.ml b/src/analyses/shapes.ml index 273eb3e0cd..9799afe8f4 100644 --- a/src/analyses/shapes.ml +++ b/src/analyses/shapes.ml @@ -71,7 +71,7 @@ struct let threadenter ctx lval f args = let st, re = ctx.local in (LD.singleton (SHMap.top ()), Re.threadenter (re_context ctx re) lval f args) - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let sync_ld ask gl upd st = let f sm (st, ds, rm, part)= diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml index 075c294713..7ed5439051 100644 --- a/src/analyses/spec.ml +++ b/src/analyses/spec.ml @@ -512,7 +512,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () end diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml index c9bf874c6b..3f4a0cac27 100644 --- a/src/analyses/stackTrace.ml +++ b/src/analyses/stackTrace.ml @@ -37,7 +37,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end @@ -79,7 +79,7 @@ struct let threadenter ctx lval f args = D.push !Tracing.current_loc ctx.local - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local end diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 2ad68ba2af..da44b67a34 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -24,7 +24,7 @@ struct let startstate v = D.top () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () let branch ctx exp tv = ctx.local diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml index ae0888b5d6..84b7c839bc 100644 --- a/src/analyses/termination.ml +++ b/src/analyses/termination.ml @@ -230,7 +230,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.bot () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.bot () end diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index abbfe33f40..41cf2b0639 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -15,6 +15,8 @@ struct module C = D module G = ConcDomain.ThreadCreation + let should_join = D.equal + (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = ctx.local let branch ctx (exp:exp) (tv:bool) : D.t = ctx.local @@ -100,7 +102,7 @@ struct | `Bot -> (false, TS.bot (), false) in ctx.sideg tid eff; - D.singleton tid + D.join ctx.local (D.singleton tid) let exitstate v = D.bot () end @@ -131,7 +133,7 @@ struct let location x = let l = !Tracing.current_loc in l.file ^ ":" ^ string_of_int l.line ^ ":" ^ x.vname in D.singleton (location f) - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local end let _ = MCP.register_analysis (module StartLocIDs : MCPSpec) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index be5230d341..f9a3666d11 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -70,13 +70,14 @@ struct | _ -> D.bot () let threadspawn ctx lval f args fctx = - match args with - | [ptc_arg] -> - let escaped = fctx.local in (* reuse reachable computation from threadenter *) - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); - escaped - | _ -> D.bot () + D.join ctx.local @@ + match args with + | [ptc_arg] -> + let escaped = fctx.local in (* reuse reachable computation from threadenter *) + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + escaped + | _ -> D.bot () end let _ = diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index 49256da22b..f4e4762168 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -32,6 +32,8 @@ struct let create_tid v = Flag.get_multi () + let should_join = D.equal + let body ctx f = ctx.local let branch ctx exp tv = ctx.local @@ -84,7 +86,7 @@ struct let threadspawn ctx lval f args fctx = if not (is_multi ctx.ask) then ctx.emit Events.EnterMultiThreaded; - Flag.get_main () + D.join ctx.local (Flag.get_main ()) end let _ = diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 472f6e0e45..22627ef0bc 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -89,7 +89,7 @@ struct create_tid f let threadspawn ctx lval f args fctx = - ThreadLifted.bot () + ctx.local end let _ = diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml index d3c870d8b0..6184b181fc 100644 --- a/src/analyses/threadReturn.ml +++ b/src/analyses/threadReturn.ml @@ -43,7 +43,7 @@ struct let startstate v = true let threadenter ctx lval f args = true - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () let query ctx x = diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml index 7f9a2f0a13..fb36f0051b 100644 --- a/src/analyses/uninit.ml +++ b/src/analyses/uninit.ml @@ -28,7 +28,7 @@ struct let startstate v : D.t = D.empty () let threadenter ctx lval f args : D.t = D.empty () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v : D.t = D.empty () (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain diff --git a/src/analyses/unit.ml b/src/analyses/unit.ml index 46f2a41cd2..e95ed4208a 100644 --- a/src/analyses/unit.ml +++ b/src/analyses/unit.ml @@ -36,7 +36,7 @@ struct let startstate v = D.bot () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index d59006b7a6..f194752097 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -48,7 +48,7 @@ struct let startstate v = D.top () let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () let const_equal c1 c2 = diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 0b63608e87..7706bbebf5 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -537,8 +537,9 @@ struct List.iter (uncurry ctx.sideg) diff; d' - let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, G.t, S.C.t) ctx * D.t list ref = + let common_ctx var edge prev_node pval (getl:lv -> ld) sidel getg sideg : (D.t, G.t, S.C.t) ctx * D.t list ref * (lval option * varinfo * exp list * D.t) list ref = let r = ref [] in + let spawns = ref [] in (* now watch this ... *) let rec ctx = { ask = query @@ -562,37 +563,59 @@ struct (* TODO: adjust ctx node/edge? *) let d = S.threadenter ctx lval f args in let c = S.context d in - let rec fctx = - { ctx with - ask = fquery - ; local = d - } - and fquery x = S.query fctx x - in - r := S.threadspawn ctx lval f args fctx :: !r; + spawns := (lval, f, args, d) :: !spawns; if not full_context then sidel (FunctionEntry f, c) d; ignore (getl (Function f, c)) in (* ... nice, right! *) let pval = sync ctx in - { ctx with local = pval }, r + { ctx with local = pval }, r, spawns let rec bigsqcup = function | [] -> D.bot () | [x] -> x | x::xs -> D.join x (bigsqcup xs) + let thread_spawns ctx d spawns = + if List.is_empty spawns then + d + else + let rec ctx' = + { ctx with + ask = query' + ; local = d + } + and query' x = S.query ctx' x + in + let one_spawn (lval, f, args, fd) = + let rec fctx = + { ctx with + ask = fquery + ; local = fd + } + and fquery x = S.query fctx x + in + S.threadspawn ctx' lval f args fctx + in + bigsqcup (List.map one_spawn spawns) + + let common_join ctx d splits spawns = + (* bigsqcup (d :: splits @ spawns) *) + thread_spawns ctx (bigsqcup (d :: splits)) spawns + + let common_joins ctx ds splits spawns = common_join ctx (bigsqcup ds) splits spawns + let tf_loop var edge prev_node getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.intrpt ctx)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.intrpt ctx) !r !spawns let tf_assign var edge prev_node lv e getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.assign ctx lv e)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.assign ctx lv e) !r !spawns let tf_vdecl var edge prev_node v getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.vdecl ctx v)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.vdecl ctx v) !r !spawns let normal_return r fd ctx sideg = let spawning_return = S.return ctx r fd in @@ -608,7 +631,7 @@ struct nval let tf_ret var edge prev_node ret fd getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in let d = if (fd.svar.vid = MyCFG.dummy_func.svar.vid || List.mem fd.svar.vname (List.map Json.string (get_list "mainfun"))) && @@ -616,15 +639,15 @@ struct then toplevel_kernel_return ret fd ctx sideg else normal_return ret fd ctx sideg in - bigsqcup (d::!r) + common_join ctx d !r !spawns let tf_entry var edge prev_node fd getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.body ctx fd)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.body ctx fd) !r !spawns let tf_test var edge prev_node e tv getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.branch ctx e tv)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.branch ctx e tv) !r !spawns let tf_normal_call ctx lv e f args getl sidel getg sideg = let combine (cd, fc, fd) = @@ -662,7 +685,7 @@ struct let tf_special_call ctx lv f args = S.special ctx lv f args let tf_proc var edge prev_node lv e args getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in let functions = match ctx.ask (Queries.EvalFunvar e) with | `LvalSet ls -> Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls [] @@ -679,15 +702,15 @@ struct d (* because LevelSliceLifter *) else let funs = List.map one_function functions in - bigsqcup (funs @ !r) + common_joins ctx funs !r !spawns let tf_asm var edge prev_node getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.asm ctx)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.asm ctx) !r !spawns let tf_skip var edge prev_node getl sidel getg sideg d = - let ctx, r = common_ctx var edge prev_node d getl sidel getg sideg in - bigsqcup ((S.skip ctx)::!r) + let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in + common_join ctx (S.skip ctx) !r !spawns let tf var getl sidel getg sideg prev_node edge d = begin match edge with diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml index 9baedfdbaf..2a33a6373d 100644 --- a/src/witness/observerAnalysis.ml +++ b/src/witness/observerAnalysis.ml @@ -74,7 +74,7 @@ struct let startstate v = `Lifted Automaton.initial let threadenter ctx lval f args = D.top () - let threadspawn ctx lval f args fctx = D.bot () + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () end diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml index b8e24e7b23..d56507563c 100644 --- a/src/witness/witnessConstraints.ml +++ b/src/witness/witnessConstraints.ml @@ -334,7 +334,7 @@ struct try Dom.add (g (f (conv ctx x))) (step_ctx_edge ctx x) xs with Deadcode -> xs in - let d = Dom.fold h (fst ctx.local) (Dom.empty ()) in + let d = Dom.fold h (fst ctx.local) (Dom.empty ()) |> Dom.reduce in if Dom.is_bot d then raise Deadcode else (d, Sync.bot ()) let assign ctx l e = map ctx Spec.assign (fun h -> h l e )