Add P.t as of the local constraint system unknowns.

jerhard · jerhard · commit 436a2eee9573 · 2026-03-09T15:44:50.000+01:00
This breaks comparing constraint systems for the backward constraint systems (for now).
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
@@ -46,6 +46,34 @@ struct
   let is_write_only _ = false
 end
 
+(** Functor for locals with digests. *)
+module VarDigestF (C: Printable.S) (P : Printable.S) =
+struct
+  type t = Node.t * C.t * P.t [@@deriving eq, ord, hash]
+  let relift (n,x,p) = n, C.relift x, P.relift p
+
+  let getLocation (n,d,p) = Node.location n
+
+  let pretty_trace () ((n,c,p) as x) =
+    if get_bool "dbg.trace.context" then (* Print context and digest *)
+      dprintf "(%a, %a, %a) on %a" Node.pretty_trace n C.pretty c P.pretty p CilType.Location.pretty (getLocation x)
+    else
+      dprintf "%a on %a" Node.pretty_trace n CilType.Location.pretty (getLocation x)
+
+  let printXml f (n,c,p) =
+    Var.printXml f n;
+    BatPrintf.fprintf f "<context>\n";
+    C.printXml f c;
+    (* Print digest, for now as part of <context>; not sure how this is parsed. *)
+    P.printXml f p;
+    BatPrintf.fprintf f "</context>\n"
+
+  let var_id (n,_,_) = Var.var_id n
+  let node (n,_,_) = n
+  let is_write_only _ = false
+end
+
+
 module type SpecSysVar =
 sig
   include Printable.S
@@ -497,8 +525,8 @@ end
 module type ComparableSpecSys =
 sig
   module Spec: Spec
-  module EQSys: Goblint_constraint.ConstrSys.BaseGlobConstrSys 
-    with module LVar = VarF (Spec.C)
+  module EQSys: Goblint_constraint.ConstrSys.BaseGlobConstrSys
+    with module LVar = VarDigestF (Spec.C) (Spec.P)
      (* and module GVar = GVarPretty (Spec.V) *)
      and module D = Spec.D
   (* and module G = GVarG (Spec.G) (Spec.C) *)
@@ -509,7 +537,7 @@ end
 module type FwdSpecSys =
 sig
   module Spec: Spec
-  module EQSys: Goblint_constraint.ConstrSys.FwdGlobConstrSys with module LVar = VarF (Spec.C)
+  module EQSys: Goblint_constraint.ConstrSys.FwdGlobConstrSys with module LVar = VarDigestF (Spec.C) (Spec.P)
                                                                and module GVar = GVarFCNW (Spec.V) (Spec.C)
                                                                and module D = Spec.D
                                                                and module G = GVarL (Spec.G) (Spec.D)
diff --git a/src/framework/compareConstraints.ml b/src/framework/compareConstraints.ml
@@ -48,7 +48,7 @@ struct
     Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk
 
   let compare_locals l1 l2 =
-    let one_ctx (node,_) v h =
+    let one_ctx (node,_,_) v h =
       PP.replace h node (try D.join v (PP.find h node) with Not_found -> v);
       h
     in
diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -117,7 +117,7 @@ struct
 
   module Slvr = (GlobSolverFromEqSolver (Goblint_solver.Selector.Make (PostSolverArg))) (EQSys) (LHT) (GHT)
   (* The comparator *)
-  module CompareGlobSys = CompareConstraints.CompareGlobSys (SpecSys)
+  (* module CompareGlobSys = CompareConstraints.CompareGlobSys (SpecSys) *)
 
   (* Triple of the function, context, and the local value. *)
   module RT = AnalysisResult.ResultType2 (Spec)
@@ -552,7 +552,8 @@ struct
                 (Splitter.split_solution vh', vh')
               ) (d1, d2)
             in
-
+            (* TODO: Fix the implementation of CompareConstraints below *)
+(*
             if get_bool "dbg.compare_runs.globsys" then
               CompareGlobSys.compare (d1, d2) r1 r2;
 
@@ -566,7 +567,7 @@ struct
 
             let module CompareNode = CompareConstraints.CompareNode (Spec.C) (EQSys.D) (LHT) in
             if get_bool "dbg.compare_runs.node" then
-              CompareNode.compare (d1, d2) (fst r1) (fst r2);
+              CompareNode.compare (d1, d2) (fst r1) (fst r2); *)
 
             r1 (* return the result of the first run for further options -- maybe better to exit early since compare_runs is its own mode. Only excluded verify below since it's on by default. *)
           | _ -> failwith "Currently only two runs can be compared!";
@@ -619,19 +620,21 @@ struct
       in
 
       if get_string "comparesolver" <> "" then (
-        let compare_with (module S2 : DemandEqIncrSolver) =
-          let module PostSolverArg2 =
-          struct
+        failwith "Comparison not implemented for backward constraint systems."
+        (** TODO: Fix implementation below *)
+        (* let compare_with (module S2 : DemandEqIncrSolver) =
+           let module PostSolverArg2 =
+           struct
             include PostSolverArg
             let should_warn = false (* we already warn from main solver *)
             let should_save_run = false (* we already save main solver *)
-          end
-          in
-          let module S2' = (GlobSolverFromEqSolver (S2 (PostSolverArg2))) (EQSys) (LHT) (GHT) in
-          let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
-          CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2)
-        in
-        compare_with (Goblint_solver.Selector.choose_solver (get_string "comparesolver"))
+           end
+           in
+           let module S2' = (GlobSolverFromEqSolver (S2 (PostSolverArg2))) (EQSys) (LHT) (GHT) in
+           let (r2, _) = S2'.solve entrystates entrystates_global startvars' None in (* TODO: has incremental data? *)
+           CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (r2)
+           in
+           compare_with (Goblint_solver.Selector.choose_solver (get_string "comparesolver")) *)
       );
 
       (* Most warnings happen before during postsolver, but some happen later (e.g. in finalize), so enable this for the rest (if required by option). *)
diff --git a/src/framework/fwdConstraints.ml b/src/framework/fwdConstraints.ml
@@ -19,18 +19,18 @@ end
 (** The main point of this file---generating a [FwdGlobConstrSys] from a [Spec]. *)
 module FromSpec (S:Spec) (Cfg:CfgForward) (I: Increment)
   : sig
-    include FwdGlobConstrSys with module LVar = VarF (S.C)
+    include FwdGlobConstrSys with module LVar = VarDigestF (S.C) (S.P)
                               and module GVar = GVarFCNW (S.V)(S.C)
                               and module D = S.D
                               and module G = GVarL (S.G) (S.D)
   end
 =
 struct
-  type lv = MyCFG.node * S.C.t
+  type lv = MyCFG.node * S.C.t * S.P.t
   (* type gv = varinfo *)
   type ld = S.D.t
   (* type gd = S.G.t *)
-  module LVar = VarF (S.C)
+  module LVar = VarDigestF (S.C) (S.P)
   module GVar = GVarFCNW (S.V)(S.C)
   module D = S.D
   module G = GVarL (S.G) (S.D)
@@ -45,17 +45,17 @@ struct
       S.sync man (`JoinCall f)
     | _ -> S.sync man `Join
 
-  let common_man' var edge target_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
+  let common_man' (var: node * Obj.t * Obj.t) edge target_node pval (getl:lv -> ld) sidel getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
     let r = ref [] in
     let spawns = ref [] in
     (* now watch this ... *)
     let rec man =
       { ask     = (fun (type a) (q: a Queries.t) -> S.query man q)
       ; emit    = (fun _ -> failwith "emit outside MCP")
       ; node    = target_node
-      ; prev_node = fst var
-      ; control_context = (fun () -> snd var |> Obj.obj)
-      ; context = (fun () -> snd var |> Obj.obj)
+      ; prev_node = Tuple3.first var
+      ; control_context = (fun () -> Tuple3.second var |> Obj.obj)
+      ; context = (fun () -> Tuple3.second var |> Obj.obj)
       ; edge    = edge
       ; local   = pval
       ; global  = (fun g -> G.spec (getg (GVar.spec g)))
@@ -72,7 +72,9 @@ struct
           match Cilfacade.find_varinfo_fundec f with
           | fd ->
             let c = S.context man fd d in
-            sidel (FunctionEntry fd, c) d
+            (* Derive digest from abstract state *)
+            let p = S.P.of_elt d in
+            sidel (FunctionEntry fd, c, p) d
           | exception Not_found ->
             (* unknown function *)
             M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
@@ -167,7 +169,7 @@ struct
     let d = S.branch man e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf_normal_call man lv e (f:fundec) args getl sidel getg sideg =
+  let tf_normal_call man lv e (f:fundec) args getl (sidel : lv -> ld -> unit) getg sideg =
     let combine (cd, fc, fd) =
       if M.tracing then M.traceli "combine" "local: %a" S.D.pretty cd;
       if M.tracing then M.trace "combine" "function: %a" S.D.pretty fd;
@@ -222,7 +224,13 @@ struct
     in
     let paths = S.enter man lv f args in
     let paths = List.map (fun (c,v) -> (c, S.context man f v, v)) paths in
-    List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) paths;
+    let sidel_entries (c,fc,v) =
+      if not (S.D.is_bot v) then begin
+        let p = S.P.of_elt v in
+        sidel (FunctionEntry f, fc, p) v
+      end
+    in
+    List.iter sidel_entries paths;
     let paths = List.map (fun (c,fc,v) ->
         let endvar = (GVar.return (f,fc)) in
         (c, fc, if S.D.is_bot v then v else G.return @@ getg endvar)) paths in
@@ -323,33 +331,33 @@ struct
     let d = S.skip man in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
     common_join man d !r !spawns
 
-  let tf ((n,c) as var) getl sidel getg sideg target_node edge d =
+  let tf ((n,c,p) as var) getl sidel getg sideg target_node edge d =
     begin match edge with
       | Assign (lv,rv) ->
         let r = tf_assign var edge target_node lv rv getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | VDecl (v)      ->
         let r = tf_vdecl var edge target_node v getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | Proc (r,f,ars) ->
         let r = tf_proc var edge target_node r f ars getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | Entry f        ->
         let r = tf_entry var edge target_node f getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | Ret (r,fd)     ->
         let r = tf_ret var edge target_node r fd getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r;
+        sidel (target_node, Obj.obj c, Obj.obj p) r;
         sideg (GVar.return (fd,Obj.obj c)) (G.create_return r)
-      | Test (p,b)     ->
-        let r = tf_test var edge target_node p b getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+      | Test (e,b)     ->
+        let r = tf_test var edge target_node e b getl sidel getg sideg d in
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | ASM (_, _, _)  ->
         let r = tf_asm var edge target_node getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
       | Skip           ->
         let r = tf_skip var edge target_node getl sidel getg sideg d in
-        sidel (target_node, Obj.obj c) r
+        sidel (target_node, Obj.obj c, Obj.obj p) r
     end
 
   type Goblint_backtrace.mark += TfLocation of location
@@ -372,13 +380,13 @@ struct
         tf var getl sidel getg sideg target_node edge d
       )
 
-  let tf_fwd value (v,c) (edges, u) getl sidel getg sideg:unit =
+  let tf_fwd value (v,c,p) (edges, u) getl sidel getg sideg:unit =
     let pval = value in
     let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in
-    let es = List.map (tf (v,Obj.repr c) getl sidel getg sideg u) edges in
+    let es = List.map (tf (v,Obj.repr c, Obj.repr p) getl sidel getg sideg u) edges in
     List.iter2 (fun e l -> e pval l) es locs
 
-  let tf value (v,c) (e,u) getl sidel getg sideg =
+  let tf value (v,c,p) (e,u) getl sidel getg sideg =
     let old_node = !current_node in
     let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
     let new_fd = Node.find_fundec v in
@@ -393,12 +401,12 @@ struct
         if not (CilType.Fundec.equal old_fd new_fd) then
           Timing.Program.exit new_fd.svar.vname
       ) (fun () ->
-        tf_fwd value (v,c) (e,u) getl sidel getg sideg
+        tf_fwd value (v,c,p) (e,u) getl sidel getg sideg
       )
 
-  let system (v,c) =
+  let system (v,c,p) =
     let tf value getl sidel getg sideg =
-      let tf' eu = tf value (v,c) eu getl sidel getg sideg in
+      let tf' eu = tf value (v,c,p) eu getl sidel getg sideg in
       let xs = Cfg.next v in
       List.iter (fun eu -> tf' eu) xs
     in
diff --git a/src/framework/fwdControl.ml b/src/framework/fwdControl.ml
@@ -225,7 +225,8 @@ struct
     let res = Result.create 113 in
 
     (* Adding the state at each system variable to the final result *)
-    let add_local_var (n,es) state =
+    (* TODO: Consider digest in result? *)
+    let add_local_var (n,es,_) state =
       (* Not using Node.location here to have updated locations in incremental analysis.
           See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *)
       let loc = UpdateCil.getLoc n in
@@ -445,8 +446,8 @@ struct
     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
+    let startfuns = List.concat (startvars @ exitvars @ othervars) in
+    if startfuns = [] then
       failwith "BUG: Empty set of start variables; may happen if enter_func of any analysis returns an empty list.";
 
     AnalysisState.global_initialization := false;
@@ -466,9 +467,21 @@ struct
       ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
       }
     in
-    let startvars' = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (man e) n e)) startvars in
+    let startvars' =
+      let to_startvar (n,e) =
+        let context = Spec.context (man e) n e in
+        let digest = Spec.P.of_elt e in
+        (MyCFG.FunctionEntry n, context, digest)
+      in
+      List.map to_startvar startfuns in
 
-    let entrystates = List.map (fun (n,e) -> (MyCFG.FunctionEntry n, Spec.context (man e) n e), e) startvars in
+    let entrystates =
+      let to_entrystate (n,e) =
+        let context = Spec.context (man e) n e in
+        let digest = Spec.P.of_elt e in
+        ((MyCFG.FunctionEntry n, context, digest), e)
+      in
+      List.map to_entrystate startfuns in
     let entrystates_global = GHT.to_list gh in
 
     let uncalled_dead = ref 0 in
@@ -481,9 +494,9 @@ struct
       let gobview = get_bool "gobview" in
       let save_run_str = let o = get_string "save_run" in if o = "" then (if gobview then "run" else "") else o in
       let solve = if (get_string "solver" = "bu") then BuSolver.solve else
-        if (get_string "solver" = "wbu") then WBuSolver.solve else FwdSolver.solve in 
-      let check = if (get_string "solver" = "bu") then BuSolver.check else 
-        if (get_string "solver" = "wbu") then WBuSolver.check else FwdSolver.check in 
+        if (get_string "solver" = "wbu") then WBuSolver.solve else FwdSolver.solve in
+      let check = if (get_string "solver" = "bu") then BuSolver.check else
+        if (get_string "solver" = "wbu") then WBuSolver.check else FwdSolver.check in
       let _ = solve entrystates entrystates_global startvars' in
 
       AnalysisState.should_warn := true; (* reset for postsolver *)
@@ -496,7 +509,7 @@ struct
       (* Most warnings happen before during postsolver, but some happen later (e.g. in finalize), so enable this for the rest (if required by option). *)
       AnalysisState.should_warn := PostSolverArg.should_warn;
       let insrt k _ s = match k with
-        | (MyCFG.FunctionEntry fn,_) -> Set.Int.add fn.svar.vid s
+        | (MyCFG.FunctionEntry fn,_,_) -> Set.Int.add fn.svar.vid s
         | _ -> s
       in
       (* set of ids of called functions *)
@@ -541,10 +554,10 @@ struct
           let lh2, gh2 = LHT.of_seq rho, GHT.of_seq tau in
           CompareGlobSys.compare (get_string "solver", get_string "comparesolver") (lh,gh) (lh2, gh2)
         in
-        let solve = if (get_string "comparesolver" = "bu") then BuSolver.solve else 
+        let solve = if (get_string "comparesolver" = "bu") then BuSolver.solve else
             (if (get_string "comparesolver" = "fwd") then FwdSolver.solve else WBuSolver.solve) in
 
-        let check = if (get_string "comparesolver" = "bu") then BuSolver.check else 
+        let check = if (get_string "comparesolver" = "bu") then BuSolver.check else
             (if (get_string "comparesolver" = "fwd") then FwdSolver.check else WBuSolver.check) in
         compare_with solve check;
       );

Original file line number	Diff line number	Diff line change
`@@ -48,7 +48,7 @@ struct`
`48`	`48`	`Logs.info "globals:\tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk`
`49`	`49`
`50`	`50`	`let compare_locals l1 l2 =`
`51`		`- let one_ctx (node,_) v h =`
	`51`	`+ let one_ctx (node,_,_) v h =`
`52`	`52`	`PP.replace h node (try D.join v (PP.find h node) with Not_found -> v);`
`53`	`53`	`h`
`54`	`54`	`in`