Forward Solvers: Split local unknowns by digests by jerhard · Pull Request #1971 · goblint/analyzer

jerhard · 2026-03-30T09:00:01Z

This PR splits the local unknowns by digests for the forward constraint systems. It uses the module P of the analysis specifications that was previously used for pathsensitivity.

Local unknowns now are four-tuples, consisting of the node, the calling context, the calling digest (called original_digest in the implementation) and the current digest.

After the application of a transfer function, when the new abstract state is computed, the new current digest is derived from the abstract state via the function P.of_elt. In case a transfer function should introduce some splitting, it can use man.split, which is the same mechanism as for pathsensitivity.

The pathsensitivity (without splitting of unknowns) is used when solvers.fwd.digests is false, and the digests are used otherwise.

Additionally, there are changes to the XSLT-output, now grouping result entries consisting of context, calling digest, current digest and abstract state together.

This breaks comparing constraint systems for the backward constraint systems (for now).

…, context, original- and current digest.

Handle man.split with the digest system for the foward-propagating constraint system. Handling of procedure calls still needs some work. When defaulting to "bu" as the default solver this commit increases the number of failing sanity tests to 38.

…hin called function.

This introduces makes the domain for function return nodes a mapping from unknowns to abstract values. The unknowns that are used as keys may differ by digest, in particular.

This will allow to have the globals defined by the analyses, globals for returns split by current digest, and globals for returns joined over current digests.

…gests at global return unknowns.

…ction is applicable works.

…ues from dead digests not being pruned

…on call pollute results. Also a problem without digests.

…d_once test.

In fwdConstraints, in case that the callee does not return, introduce a return path with bottom for the longjmpLifter to do its work.

…viely. This implementation using man.split should work when using digests and when using pathsensitivity. The event list passed to man.split is empty, since there is nothing further to do.

…onal path-sensitivity with option solvers.fwd.digests.

…tart node)

sim642 · 2026-03-31T04:49:06Z

I just realized that this isn't merging into master. That's why there's no forward solver in the diff here.

Copilot

Pull request overview

This PR introduces digest-based splitting of local unknowns in the forward constraint system to realize path-sensitivity via analysis-spec P digests (configurable via solvers.fwd.digests). It also adapts result aggregation and the XSLT report output to present results grouped by (context, calling digest, current digest, abstract state).

Changes:

Add digest-aware local variables and forward constraint generation that propagates/updates digests and supports splitting via man.split.
Extend the framework with Spec'/LVarSet support and a new 3-way lifted global lattice (Lift3 / GVar3) to represent spec globals + per-return-node globals + return-node sets.
Update XSLT/XML result output and add new regression tests under tests/regression/90-digests.

Reviewed changes

Copilot reviewed 19 out of 20 changed files in this pull request and generated 9 comments.

Show a summary per file

File	Description
`xslt/node.xsl`	Render node results as grouped `<tuple>` entries with optional digest sections.
`tests/regression/90-digests/01-function-call.c`	New regression test for digest-sensitive behavior across function calls.
`tests/regression/90-digests/02-mutex-lock-split.c`	New regression test for digest-sensitive mutex locking.
`tests/regression/90-digests/03-function-call-split.c`	New regression test for digest changes during a function call.
`tests/regression/90-digests/04-garbage-digest.c`	New regression test for digest “garbage collection” expectations.
`tests/regression/90-digests/05-garbage-call.c`	New regression test involving calls/precision; currently has a C11 declaration-order concern.
`tests/regression/90-digests/06-longjmp-return.c`	New regression test for longjmp/setjmp interactions with the solver.
`src/solver/td_simplified_ref_improved.ml`	Formatting-only adjustments.
`src/lifters/noDigestLifter.ml`	New lifter to expose unit digests when `solvers.fwd.digests` is disabled.
`src/lifters/longjmpLifter.ml`	Adjust setjmp handling to use `man.split` for separating normal vs longjmp return flows.
`src/framework/fwdControl.ml`	Switch forward analysis to `Spec'`, integrate digest-aware result type, and wire in the new comparator.
`src/framework/fwdConstraints.ml`	Core change: digest-aware locals (`VarDigestF`), digest propagation/update, and return handling via return-node sets.
`src/framework/fwdCompareConstraints.ml`	New forward comparator adapted to digest-aware locals and the new forward globals.
`src/framework/control.ml`	Switch to `Spec'` in the (non-forward) control pipeline for shared infrastructure.
`src/framework/compareConstraints.ml`	Refactor comparator to work against `SpecSys` and adjust local-joining logic structure.
`src/framework/analysisResult.ml`	Change XML printing to emit `<tuple>` entries and add a digest-aware result entry type.
`src/framework/analyses.ml`	Introduce `VarDigestF`, `GVarFCNW` return variants, `GVar3`, `Spec'`, and `Spec2Spec'`.
`src/domain/lattice.ml`	Add `Lift3` lattice combinator to support 3-way lifted globals.
`src/config/options.schema.json`	Add new option `solvers.fwd.digests` (default `false`).
`src/common/domains/printable.ml`	Add `Lift3Conf` printable and `Prod4` printable used by new result/global types.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

src/framework/fwdConstraints.ml

Copilot · 2026-03-31T09:37:47Z

src/framework/fwdConstraints.ml

+            let s = Seq.map return_value return_nodes in
+            if Seq.is_empty s then
+              (* In case the calle does not return, create one bottom return path for LongjmpLifter to do its work *)
+              [S.D.bot ()]
+            else
+              List.of_seq s


Seq.is_empty s consumes the first element of the sequence s, so the subsequent List.of_seq s will miss that element (and may even become empty). This can drop return paths and lead to incorrect call/return semantics. Materialize the sequence once (e.g., convert to a list and test that list), or use Seq.uncons/equivalent to check emptiness without losing elements.

Suggested change

let s = Seq.map return_value return_nodes in

if Seq.is_empty s then

(* In case the calle does not return, create one bottom return path for LongjmpLifter to do its work *)

[S.D.bot ()]

else

List.of_seq s

let return_nodes_list = List.of_seq return_nodes in

if return_nodes_list = [] then

(* In case the calle does not return, create one bottom return path for LongjmpLifter to do its work *)

[S.D.bot ()]

else

List.map return_value return_nodes_list

I don't think this a problem, the sequence should be persistent, or?

src/framework/fwdConstraints.ml

Copilot · 2026-03-31T09:37:48Z

src/lifters/noDigestLifter.ml

+  include S
+  module P = struct
+    include Printable.Unit
+    let of_elt _ = ()


NoDigestLifter uses Printable.Unit for P, which will render digests as "()" in XML/HTML. Since fwdControl always outputs <original_digest>/<current_digest>, this makes the UI show digest sections even when solvers.fwd.digests is disabled. Consider overriding P.printXml/P.show to output an empty value (so the XSLT normalize-space(...) checks hide it), or conditionally omit digest tags in the result XML when digests are disabled.

Suggested change

let of_elt _ = ()

let of_elt _ = ()

let show _ = ""

let printXml _formatter _t = ()

Copilot · 2026-03-31T09:37:48Z

src/framework/analyses.ml

+    if get_bool "dbg.trace.context" then (* Print context and digest *)
+      dprintf "(%a, %a, %a) on %a" Node.pretty_trace x.node C.pretty x.context P.pretty x.original_digest CilType.Location.pretty (getLocation x)


VarDigestF.pretty_trace only prints original_digest, not current_digest. Since the local variable identity includes both digests, traces can become ambiguous once current_digest starts changing. Include both digests (or at least print current_digest when it differs) to make debugging reliable.

Suggested change

if get_bool "dbg.trace.context" then (* Print context and digest *)

dprintf "(%a, %a, %a) on %a" Node.pretty_trace x.node C.pretty x.context P.pretty x.original_digest CilType.Location.pretty (getLocation x)

if get_bool "dbg.trace.context" then (* Print context and digests *)

dprintf "(%a, %a, %a, %a) on %a" Node.pretty_trace x.node C.pretty x.context P.pretty x.original_digest P.pretty x.current_digest CilType.Location.pretty (getLocation x)

Copilot · 2026-03-31T09:37:48Z

src/lifters/longjmpLifter.ml


  module V =
  struct
+    (* TODO: Consider splitting unknowns by digest for constraint system in [FwdConstraints] *)


The TODO comment about "splitting unknowns by digest" looks outdated now that digests are implemented in FwdConstraints. Consider removing or updating it to reflect the current mechanism (e.g., that this lifter uses man.split, which is implemented via digests when solvers.fwd.digests is enabled).

Suggested change

(* TODO: Consider splitting unknowns by digest for constraint system in [FwdConstraints] *)

(* This lifter uses [man.split] for splitting unknowns; when [solvers.fwd.digests] is enabled, this is implemented via digests in [FwdConstraints]. *)

Copilot · 2026-03-31T09:37:49Z

src/lifters/longjmpLifter.ml

+        man.split normal_return [];
+        man.split longjmped [];
+        D.bot ()
      )
    | Longjmp {env; value} ->


With the new forward solver semantics, man.split paths are propagated separately (not just joined), and the transfer function return value is also propagated as its own path. Returning D.bot () here therefore introduces an extra bottom path/state in addition to normal_return and longjmped, which can create spurious digest entries and extra solver work. Prefer returning one of the real states (e.g., normal_return) and only man.split the other(s) to avoid propagating a standalone bottom path.

Suggested change

man.split normal_return [];

man.split longjmped [];

D.bot ()

)

| Longjmp {env; value} ->

man.split longjmped [];

normal_return

)

| Longjmp {env; value} ->

| Longjmp {env; value} ->

tests/regression/90-digests/05-garbage-call.c

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

michael-schwarz

Nice! I was wondering if now that you have understood all the details may be a good idea to leave some more comments in these modules. I think if someone comes back to this in a few years, it will all be very hard to understand.

Also: Maybe establishing some kind of terminology for the return variable where occuring digests are accumulated may be helpful?

michael-schwarz · 2026-03-31T09:27:36Z

src/common/domains/printable.ml

+  include Std
+
+  let show (x,y,z,w) =
+    (* TODO: remove ref *)


What is needed to remove the TODO here?

It's a copy-paste leftover from other modules in the file. It should be enough to just inline them.

michael-schwarz · 2026-03-31T09:32:58Z

src/framework/analyses.ml

 end

+(** Functor for locals with digests. *)
+module VarDigestF (C: Printable.S) (P : Printable.S) =


Can one not reuse VarF with an appropriate LD here?

michael-schwarz · 2026-03-31T09:34:17Z

src/framework/analyses.ml

+  (* For return vars given by function, context, original digest *)
+  module ReturnVars = Printable.Prod3 (CilType.Fundec) (C) (P)
+  (* For return vars given by function, context, original digest and current digest *)
+  module SingleReturnVars = VarDigestF (C) (P)


When do we need the first one?

Are these the set constructions? Might be worth commenting on this.

michael-schwarz · 2026-03-31T09:39:11Z

src/framework/fwdConstraints.ml

+      ; control_context = (fun () -> Obj.magic var.context) (** TODO: Just for testing *)
+      ; context = (fun () -> Obj.magic var.context)


Why are these Obj.magic now instead of Obj.obj?

michael-schwarz · 2026-03-31T09:42:45Z

src/framework/fwdConstraints.ml

               M.info ~category:Analyzer "Using special for defined function %s" f.vname;
               tf_special_call man f
             | fd ->
+               (* TODO: Handle this properly by handling splitting also here. *)


What still needs to be done here? Is this about enter or combine splitting?

michael-schwarz · 2026-03-31T09:46:38Z

src/framework/fwdConstraints.ml

+    let return_unknown d =
+      let target_unknown = target_unknown d in
+      (* GVar.single_return *)
+      target_unknown


Also, what is the advantage of this over calling target_unknown x directly?

michael-schwarz · 2026-03-31T09:47:29Z

src/framework/fwdConstraints.ml

+        in
+
+        List.iter sideg_target_unkonwn r;
+        (* TODO: Remove need to also propagate to locals for returns *)


What is this TODO about?

michael-schwarz · 2026-03-31T09:49:51Z

src/framework/fwdConstraints.ml

+        let set = S.LVarSet.bot () in
+        let add_entry set d =
+          let return_unknown = return_unknown d in
+          S.LVarSet.add return_unknown set
+        in
+        let g = GVar.return (fd, x.context, x.original_digest) in
+        let contrib = List.fold add_entry set r |> G.create_return in
+        sideg g contrib


This could use a comment: It creates a set of those digests appearing for the return point and side-effects them to the appropriate helper unknown?

michael-schwarz · 2026-03-31T09:51:17Z

src/framework/fwdConstraints.ml

+    let sidel_target_unknowns ds =
+      List.iter sidel_target_unkonwn ds


Maybe propagate or something like that is the better name here?

michael-schwarz · 2026-03-31T09:53:18Z

src/lifters/longjmpLifter.ml


  module V =
  struct
+    (* TODO: Consider splitting unknowns by digest for constraint system in [FwdConstraints] *)


Does this mean that here we still have the set construction? Which is fine, I'm just worried whether this will work together nicely.

michael-schwarz · 2026-03-31T10:02:00Z

@arkocal Can you have a look if the test failures as you would expect them to be?

jerhard added 20 commits March 17, 2026 10:41

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

a95cf6f

This breaks comparing constraint systems for the backward constraint systems (for now).

Change type of lvars of forward constraint system to record with node…

e9e643e

…, context, original- and current digest.

Add test case for "transparent calls", i.e. where digests changes wit…

9e1bbfd

…hin called function.

Digests: handle digest changing in callee.

a2ba743

This introduces makes the domain for function return nodes a mapping from unknowns to abstract values. The unknowns that are used as keys may differ by digest, in particular.

Remove obsolete todo to use common_split instead of common_join.

c82157d

Add module GVar3 that allows for three different types of globals.

dc10ee5

This will allow to have the globals defined by the analyses, globals for returns split by current digest, and globals for returns joined over current digests.

FwdConstraints: Collect sets of return unknowns with their current di…

60290a4

…gests at global return unknowns.

FwdConstraints: move List.flatten down, so that check whether any fun…

650ee6c

…ction is applicable works.

Digests: Add test case showing precision loss due to old abstract val…

8b23b7b

…ues from dead digests not being pruned

Add test case where garbage results from a spuriously analyzed functi…

3c4bff0

…on call pollute results. Also a problem without digests.

Add missing return statements to test cases.

26363e9

FwdConstraints: join pthread_once results earlier, fixey 87/01 pthrea…

3a9b0d8

…d_once test.

FwdConstraints: Set currently unknown __goblint_check to TODO.

7b1b9f9

Digests + LongjmpLifter: Fix handling of returns by longjmp.

42f5dc1

In fwdConstraints, in case that the callee does not return, introduce a return path with bottom for the longjmpLifter to do its work.

Digests: Handle return from setjmps with separate digets / pathsensit…

0a5ebf2

…viely. This implementation using man.split should work when using digests and when using pathsensitivity. The event list passed to man.split is empty, since there is nothing further to do.

FwdConstraints: Make it configurable whether to use digest or traditi…

9dc79d7

…onal path-sensitivity with option solvers.fwd.digests.

Fwd constraint system/XSLT view: Display path again.

44a5b58

XSLT view: Also display original digest (the digest at the function s…

c98e770

…tart node)

Adapt result output for backward constraint system to work again.

4654d80

jerhard requested a review from michael-schwarz March 30, 2026 13:08

Make compare constraints work for backward constraints again.

26c3acf

sim642 added the feature label Mar 31, 2026

sim642 requested review from sim642 and removed request for sim642 March 31, 2026 04:47

michael-schwarz requested a review from Copilot March 31, 2026 09:25

Copilot started reviewing on behalf of michael-schwarz March 31, 2026 09:25 View session

Copilot AI reviewed Mar 31, 2026

View reviewed changes

Fix typo in comment

1e86c64

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

michael-schwarz reviewed Mar 31, 2026

View reviewed changes

jerhard added 2 commits March 31, 2026 12:00

Move definition of identity before first call of it.

17d6d76

Fix typo in name of helper function sideg_target_unknown

8548001

jerhard added 2 commits March 31, 2026 12:14

Use List instead of Seq where is_empty is checked.

ce037a5

For forward constraint systems, use digests by default.

810b9f1

		if get_bool "dbg.trace.context" then (* Print context and digest *)
		dprintf "(%a, %a, %a) on %a" Node.pretty_trace x.node C.pretty x.context P.pretty x.original_digest CilType.Location.pretty (getLocation x)

	(* TODO: Consider splitting unknowns by digest for constraint system in [FwdConstraints] *)
	(* This lifter uses [man.split] for splitting unknowns; when [solvers.fwd.digests] is enabled, this is implemented via digests in [FwdConstraints]. *)

		; control_context = (fun () -> Obj.magic var.context) (** TODO: Just for testing *)
		; context = (fun () -> Obj.magic var.context)

		let sidel_target_unknowns ds =
		List.iter sidel_target_unkonwn ds

Conversation

jerhard commented Mar 30, 2026

Uh oh!

sim642 commented Mar 31, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

michael-schwarz left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

michael-schwarz commented Mar 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants