Bachelor's Thesis "Synthesizing Ranking Functions for LASW programs with Goblint" #1941

alexandermazur1 · 2026-02-05T13:22:28Z

In this thesis, I'm adding another algorithm for termination proving.
It is based on the synthesis of linear ranking functions suggested by Podelski and Rybalchenko in https://www.cs.cmu.edu/~hzarnani/fm-rg/cmuonly/podelski04complete.pdf.
The implementation uses Apron's convex polyhedra and linear programming.

src/analyses/loopTermination.ml

michael-schwarz · 2026-02-06T06:33:07Z

src/analyses/apron/relationAnalysis.apron.ml

          RD.cil_exp_of_lincons1 lincons1
          |> Option.map e_inv
-          |> Option.filter (InvariantCil.exp_is_suitable ~scope)
+          (*|> Option.filter (InvariantCil.exp_is_suitable ~scope)*)


This will break the framework in unexpected places, I'd recommend getting rid of it soon, so you don't go chasing failures from other analyses that are caused by this. You can, e.g., add a custom query for now that doesn't do this and then get rid of it later.

I'm guessing this is using the witness invariant query internally somewhere. It's not really intended to be used this way:

analyzer/src/cdomain/value/domains/invariant.mli

Lines 9 to 10 in d2d183c

val to_cil: t -> GoblintCil.exp

(** Breaks abstraction, only for use in {!EvalAssert}! *)

I didn't look closely but it seems to me that exp_list_of_constraints is then trying to convert that invariant back into constraints. It's a very roundabout way to get constraints from one analysis to the other, going back and forth via lossy translations that aren't intended for this.

I think the same matter came up a while ago, maybe in relation to #1635 or something similar.

Copilot

Pull request overview

This PR implements a new termination proving algorithm for loops based on linear ranking function synthesis by Podelski and Rybalchenko. The implementation adds a synthesis-based approach using convex polyhedra and linear programming (via ocplib-simplex) as an alternative to the existing loop counter-based termination analysis. The changes span preprocessing logic, Apron domain modifications, sparse matrix operations, and the main termination analysis module, along with 6 new regression tests.

Changes:

Added ocplib-simplex library dependency for linear programming
Implemented linear ranking function synthesis algorithm in loopTermination.ml
Modified preprocessing to collect loop variables and insert old_* shadow variables
Commented out safety checks in Apron domains to allow broader invariant generation
Added sparse vector/matrix addition operations
Added 6 new regression tests demonstrating advantages of synthesis approach

Reviewed changes

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

Show a summary per file

File	Description
src/dune	Adds ocplib-simplex library dependency
src/util/terminationPreprocessing.ml	Replaces loop counter instrumentation with variable collection and old_* variable insertion; contains large commented-out code block
src/cdomains/apron/sharedFunctions.apron.ml	Comments out cast injectivity check and removes type cast for invariant generation
src/analyses/apron/relationAnalysis.apron.ml	Comments out exp_is_suitable scope filter for invariants
src/cdomains/affineEquality/sparseImplementation/sparseVector.ml	Adds vector addition operation
src/cdomains/affineEquality/sparseImplementation/listMatrix.ml	Adds matrix addition operation using vector addition
src/analyses/loopTermination.ml	Implements linear ranking function synthesis using Simplex solver; includes extensive expression parsing and constraint handling
tests/regression/78-termination/52-synthesis-ranking.c	Test case from Podelski paper Example 1
tests/regression/78-termination/53-synthesis-ranking-2.c	Test case with integer division
tests/regression/78-termination/54-synthesis-impossible.c	Test case where no linear ranking function exists
tests/regression/78-termination/55-synthesis-advantage.c	Test showing synthesis advantage with non-monotonic decreasing variable
tests/regression/78-termination/56-synthesis-advantage-2.c	Test with linear ranking function 2x + y
tests/regression/78-termination/57-synthesis-advantage-3.c	Test requiring lexicographic ranking for unbounded numbers

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

Copilot · 2026-02-06T06:34:47Z

src/analyses/loopTermination.ml

+let exp_list_of_constraints (constraints : Invariant.t) =
+  match constraints with
+  | `Top -> []
+  | `Bot -> failwith "Constraints are Bot"


When constraints are Bot (bottom), the code calls failwith which will crash the analysis. However, Bot typically represents an unreachable state, which could legitimately occur in dead code or after certain control flow patterns. Consider handling this case more gracefully, possibly by returning an empty list or reporting a warning instead of crashing.

Suggested change

| `Bot -> failwith "Constraints are Bot"

| `Bot ->

if M.tracing then

M.trace "termination" "Ignoring Bot constraints (unreachable state)";

[]

Copilot · 2026-02-06T06:34:48Z

src/analyses/loopTermination.ml

+      | BinOp (Ge, e1, e2, t) -> (BinOp (Le, e2, e1, t)) :: acc
+      | BinOp (Eq, e1, e2, t) -> (BinOp (Le, e1, e2, t)) :: (BinOp (Le, e2, e1, t)) :: acc
+      | BinOp (Ne, _, _, _) -> acc
+      | _ -> failwith "Found something else, help me" in


The to_leq function uses failwith when encountering constraint types other than Le, Ge, Eq, or Ne. Invariants may contain other binary operations or unary operations that should be handled. This will cause crashes when analyzing loops with more complex conditions.

Suggested change

| _ -> failwith "Found something else, help me" in

| _ ->

(* Ignore expressions that are not simple comparison constraints. *)

acc

in

Copilot · 2026-02-06T06:34:48Z

src/util/terminationPreprocessing.ml

+                b.bstmts <- s1 ::
+                            mkStmt (Instr ((List.map init_old_var vars))) ::
+                            ss @
+                            [mkStmtOneInstr (Call (None, f_bounded, [lval (List.hd vars)], loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)


The code unconditionally passes only the first variable (List.hd vars) to __goblint_bounded, but the TODO comment indicates this needs to be replaced by "something appropriate". This means termination analysis may incorrectly analyze loops based on an arbitrarily selected variable rather than all relevant variables. This could lead to incorrect termination results. The implementation should either use all variables or have a clear strategy for selecting the representative variable.

Suggested change

[mkStmtOneInstr (Call (None, f_bounded, [lval (List.hd vars)], loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)

[mkStmtOneInstr (Call (None, f_bounded, (List.map lval vars), loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)

Copilot · 2026-02-06T06:34:48Z

src/cdomains/apron/sharedFunctions.apron.ml

@@ -316,9 +317,9 @@ struct
    | None ->
      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
      raise Unsupported_Linexpr1
-    | _ ->
+    (*| _ ->
      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
-      raise Unsupported_Linexpr1
+      raise Unsupported_Linexpr1*)


Critical safety check has been commented out. The code previously checked whether a cast from the variable's type to ILongLong was injective (overflow-preserving). Without this check, the analysis may produce incorrect results for variables whose types overflow differently than ILongLong, leading to unsound termination analysis. This change should either be reverted or a clear justification should be provided for why overflow behavior doesn't matter in this context.

Copilot · 2026-02-06T06:34:49Z

src/util/terminationPreprocessing.ml

+        (*let vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "_id" ^ (string_of_int !vcounter) in
+          incr vcounter;
+          let v = Cil.makeLocalVar fd vname counter_typ in (*Not tested for incremental mode*)
+          let lval = Lval (Var v, NoOffset) in
+          let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in
+          let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
+          let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in
+          (*Printf.printf "Before additions\n%s\n\n" (string_of_loop_info b.bstmts);*)
+          b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts;
+          lc := VarToStmt.add (v: varinfo) (s: stmt) !lc;
+          let nb = mkBlock [init_stmt; mkStmt s.skind] in
+          s.skind <- Block nb;*)


Large block of commented-out code (approximately 50 lines) that implements the original loop counter-based termination analysis. Commented code should either be removed or have a clear explanation of why it's being kept. If this is intentionally disabled in favor of the new synthesis-based approach, it should be removed to improve code maintainability.

Suggested change

(*let vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "_id" ^ (string_of_int !vcounter) in

incr vcounter;

let v = Cil.makeLocalVar fd vname counter_typ in (*Not tested for incremental mode*)

let lval = Lval (Var v, NoOffset) in

let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in

let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in

let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in

(*Printf.printf "Before additions\n%s\n\n" (string_of_loop_info b.bstmts);*)

b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts;

lc := VarToStmt.add (v: varinfo) (s: stmt) !lc;

let nb = mkBlock [init_stmt; mkStmt s.skind] in

s.skind <- Block nb;*)

Copilot · 2026-02-06T06:34:51Z

src/analyses/loopTermination.ml

+let const_in_exp e =
+  let rec inner = function
+    | BinOp (PlusA, e1, e2, _) ->
+      (match inner e1, inner e2 with
+       | Some c1, Some c2 -> failwith "This shouldn't happen"
+       | None, None -> None
+       | c, None | None, c -> c)
+    | Const (CInt (c, _, _)) -> if Z.compare c Z.zero = 0 then None else Some (c |> cilint_to_int |> Rat.of_int)
+    | BinOp (Mult, _, _, _) -> None
+    | Lval (Var v, _) -> None
+    | _ -> failwith "found something else"
+  in
+  match e with
+  | BinOp (Le, e1, e2, _) ->
+    (match inner e1, inner e2 with
+     | Some c1, Some c2 -> failwith "This shouldn't happen"
+     | None, None -> Rat.zero
+     | Some c, None -> Rat.neg c
+     | None, Some c -> c)
+  | _ -> failwith "This shouldn't happen"


The const_in_exp function has the same issues as coeff_in_exp: it uses failwith for common expression forms that should be handled. This incomplete implementation will cause crashes on valid C programs.

Copilot · 2026-02-06T06:34:51Z

tests/regression/78-termination/52-synthesis-ranking.c

+    int i, j, nat, pos;
+    __goblint_assume(nat >= 0);
+    __goblint_assume(pos >= 1);
+
+    while (i - j >= 1) {
+        j = j + pos;
+        i = i - nat;
+    }


Variables i, j, nat, and pos are declared but not initialized before being used in the while condition and loop body. While __goblint_assume constraints are provided for nat and pos, i and j are completely uninitialized. This is undefined behavior in C. The test should initialize all variables or at minimum add __goblint_assume constraints for i and j to make the test's assumptions explicit.

Copilot · 2026-02-06T06:34:52Z

tests/regression/78-termination/53-synthesis-ranking-2.c

+    int x1;
+    int x2 = 0;
+
+    while (x1 >= 2) {
+        x1 = x1 / 2;
+        x2++;
+    }


Variables x1 and x2 are used in the loop, but only x2 is initialized. x1 is used uninitialized in the while condition (x1 >= 2) which is undefined behavior in C. The test should initialize x1 or add a __goblint_assume constraint.

Copilot · 2026-02-06T06:34:52Z

tests/regression/78-termination/55-synthesis-advantage.c

+    int x;
+
+    while (x >= 2) {
+        if (x == 42) {
+            x--;
+        } else {
+            x = x / 2;
+        }
+    }


Variable x is declared but not initialized before being used in the while condition (x >= 2). This is undefined behavior in C. The test should initialize x or add a __goblint_assume constraint to specify the expected initial value range.

Copilot · 2026-02-06T06:34:52Z

src/util/terminationPreprocessing.ml

+          | CastE _ -> failwith "Encountered cast"
+          | Question _ -> failwith "Encountered question"


This code uses failwith with generic error messages like "Encountered cast" and "Encountered question". These expressions (CastE and Question) may legitimately appear in programs, and throwing an exception will crash the analysis rather than handling them gracefully. Consider either handling these cases appropriately or using M.warn to report the limitation without crashing.

michael-schwarz · 2026-02-06T06:40:39Z

src/dune

  (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes
  (modules goblint)
-  (libraries goblint.lib goblint_std)
+  (libraries goblint.lib goblint_std ocplib-simplex)


To get the CI working (highly recommended), ocplib-simplex needs to be added to the opam and opam.locked files.

Alexander Mazur added 2 commits February 4, 2026 16:23

Synthesis of ranking functions for simple unnested loops with int vars

702aeb8

Added regression tests

faea985

DrMichaelPetter linked an issue Feb 5, 2026 that may be closed by this pull request

[BA] Synthesizing linear ranking functions for LASW programs #1872

Open

github-advanced-security bot found potential problems Feb 5, 2026

View reviewed changes

DrMichaelPetter assigned DrMichaelPetter and alexandermazur1 and unassigned DrMichaelPetter Feb 5, 2026

DrMichaelPetter added the feature label Feb 5, 2026

sim642 added the student-job label Feb 5, 2026

Replaced print debugging by tracing

211b3e8

michael-schwarz requested a review from Copilot February 6, 2026 06:28

Copilot started reviewing on behalf of michael-schwarz February 6, 2026 06:28 View session

michael-schwarz reviewed Feb 6, 2026

View reviewed changes

Copilot AI reviewed Feb 6, 2026

View reviewed changes

michael-schwarz reviewed Feb 6, 2026

View reviewed changes

	val to_cil: t -> GoblintCil.exp
	(** Breaks abstraction, only for use in {!EvalAssert}! *)

	[mkStmtOneInstr (Call (None, f_bounded, [lval (List.hd vars)], loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)
	[mkStmtOneInstr (Call (None, f_bounded, (List.map lval vars), loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)

		\| CastE _ -> failwith "Encountered cast"
		\| Question _ -> failwith "Encountered question"

Bachelor's Thesis "Synthesizing Ranking Functions for LASW programs with Goblint" #1941

Are you sure you want to change the base?

Bachelor's Thesis "Synthesizing Ranking Functions for LASW programs with Goblint" #1941

Uh oh!

Conversation

alexandermazur1 commented Feb 5, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

michael-schwarz Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

sim642 Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

michael-schwarz Feb 6, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants