TUM Practical Course Summer 2023: Termination Analyses

.github/workflows/coverage.yml

@@ -65,6 +65,9 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 

.github/workflows/locked.yml

@@ -64,6 +64,9 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 

.github/workflows/unlocked.yml

@@ -92,6 +92,9 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test apron termination regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group termination -s
+
       - name: Test regression cram
         run: opam exec -- dune runtest tests/regression
 

conf/svcomp.json

@@ -71,7 +71,9 @@
         "octagon",
         "wideningThresholds",
         "loopUnrollHeuristic",
-        "memsafetySpecification"
+        "memsafetySpecification",
+        "termination",
+        "specification"
       ]
     }
   },

docs/developer-guide/firstanalysis.md

@@ -67,7 +67,7 @@ The key part now is to define transfer functions for assignment. We only handle
 There is no need to implement the transfer functions for branching for this example; it only relies on lattice join operations to correctly take both paths into account.
 
 The assignment relies on the function `eval`, which is almost there. It just needs you to fix the evaluation of constants! Unless you jumped straight to this line, it should not be too complicated to fix this.
-With this in place, we should have sufficient information to tell Goblint that the assertion does hold.
+With this in place, we should have sufficient information to tell Goblint that the assertion does hold (run `make` to compile the updated analysis in Goblint).
 
 For more information on the signature of the individual transfer functions, please check out `module type Spec` documentation in [`src/framework/analyses.ml`](https://github.com/goblint/analyzer/blob/master/src/framework/analyses.ml).
 

lib/goblint/runtime/include/goblint.h

@@ -6,3 +6,5 @@ void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to av
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);
+
+void __goblint_bounded(unsigned long long exp);

lib/goblint/runtime/src/goblint.c

@@ -27,4 +27,8 @@ void __goblint_split_begin(int exp) {
 
 void __goblint_split_end(int exp) {
 
+}
+
+void __goblint_bounded(unsigned long long exp) {
+
 }

scripts/update_suite.rb

@@ -145,10 +145,11 @@ def collect_warnings
         @vars = $1
         @evals = $2
       end
+      if l =~ /\[Termination\]/ then warnings[-1] = "nonterm" end # Get Termination warning
       next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?(?:-(?:\d+)(?:\:\d+)?)?\)/
       obj,i = $1,$2.to_i
 
-      ranking = ["other", "warn", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown"]
+      ranking = ["other", "warn", "goto", "fundec", "loop", "term", "nonterm", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown"]
       thiswarn =  case obj
                     when /\(conf\. \d+\)/            then "race"
                     when /Deadlock/                  then "deadlock"
@@ -159,6 +160,9 @@ def collect_warnings
                     when /invariant confirmed/       then "success"
                     when /invariant unconfirmed/     then "unknown"
                     when /invariant refuted/         then "fail"
+                    when /(Upjumping Goto)/          then "goto"
+                    when /(Fundec \w+ is contained in a call graph cycle)/ then "fundec"
+                    when /(Loop analysis)/           then "loop"
                     when /^\[Warning\]/              then "warn"
                     when /^\[Error\]/                then "warn"
                     when /^\[Info\]/                 then "warn"
@@ -183,19 +187,33 @@ def compare_warnings
         if cond then
           @correct += 1
           # full p.path is too long and p.name does not allow click to open in terminal
-          if todo.include? idx then puts "Excellent: ignored check on #{relpath(p.path).to_s.cyan}:#{idx.to_s.blue} is now passing!" end
+          if todo.include? idx
+            if idx < 0
+              puts "Excellent: ignored check on #{relpath(p.path).to_s.cyan} for #{type.yellow} is now passing!"
+            else
+              puts "Excellent: ignored check on #{relpath(p.path).to_s.cyan}:#{idx.to_s.blue} is now passing!"
+            end
+          end
         else
-          if todo.include? idx then @ignored += 1 else
-            puts "Expected #{type.yellow}, but registered #{(warnings[idx] or "nothing").yellow} on #{p.name.cyan}:#{idx.to_s.blue}"
-            puts tests_line[idx].rstrip.gray
-            ferr = idx if ferr.nil? or idx < ferr
+          if todo.include? idx
+            @ignored += 1
+          else
+            if idx < 0 # When non line specific keywords were used don't print a line
+              puts "Expected #{type.yellow}, but registered #{(warnings[idx] or "nothing").yellow} on #{p.name.cyan}"
+            else
+              puts "Expected #{type.yellow}, but registered #{(warnings[idx] or "nothing").yellow} on #{p.name.cyan}:#{idx.to_s.blue}"
+              puts tests_line[idx].rstrip.gray
+              ferr = idx if ferr.nil? or idx < ferr
+            end
           end
         end
       }
       case type
-      when "deadlock", "race", "fail", "unknown", "warn"
+      when "goto", "fundec", "loop", "deadlock", "race", "fail", "unknown", "warn"
+        check.call warnings[idx] == type
+      when "nonterm"
         check.call warnings[idx] == type
-      when "nowarn"
+      when "nowarn", "term"
         check.call warnings[idx].nil?
       when "assert", "success"
         check.call warnings[idx] == "success"
@@ -294,6 +312,12 @@ def parse_tests (lines)
         tests[i] = "success"
       elsif obj =~ /FAIL/ then
         tests[i] = "fail"
+      elsif obj =~ /NONTERMLOOP/ then
+        tests[i] = "loop"
+      elsif obj =~ /NONTERMGOTO/ then
+        tests[i] = "goto"
+      elsif obj =~ /NONTERMFUNDEC/ then
+        tests[i] = "fundec"
       elsif obj =~ /UNKNOWN/ then
         tests[i] = "unknown"
       elsif obj =~ /(assert|__goblint_check).*\(/ then
@@ -306,6 +330,15 @@ def parse_tests (lines)
         end
       end
     end
+    case lines[0]
+    when /NONTERM/
+      tests[-1] = "nonterm"
+    when /TERM/
+      tests[-1] = "term"
+    end
+    if lines[0] =~ /TODO/ then
+      todo << -1
+    end
     Tests.new(self, tests, tests_line, todo)
   end
 

src/analyses/apron/relationAnalysis.apron.ml

@@ -196,15 +196,14 @@ struct
   let assert_type_bounds ask rel x =
     assert (RD.Tracked.varinfo_tracked x);
     match Cilfacade.get_ikind x.vtype with
-    | ik when not (IntDomain.should_ignore_overflow ik) -> (* don't add type bounds for signed when assume_none *)
+    | ik ->
       let (type_min, type_max) = IntDomain.Size.range ik in
       (* TODO: don't go through CIL exp? *)
       let e1 = BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik type_max), intType) in
       let e2 = BinOp (Ge, Lval (Cil.var x), (Cil.kintegerCilint ik type_min), intType) in
       let rel = RD.assert_inv rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *)
       let rel = RD.assert_inv rel e2 false (no_overflow ask e2) in
       rel
-    | _
     | exception Invalid_argument _ ->
       rel
 

src/analyses/libraryDesc.ml

@@ -78,6 +78,7 @@ type special =
   | Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
   | Setjmp of { env: Cil.exp; }
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
+  | Bounded of { exp: Cil.exp}  (** Used to check for bounds for termination analysis. *)
   | Rand
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 

src/analyses/libraryFunctions.ml

@@ -718,6 +718,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);
+    ("__goblint_bounded", special [__ "exp"[]] @@ fun exp -> Bounded { exp });
   ]
 
 (** zstd functions.

src/analyses/loopTermination.ml

@@ -0,0 +1,87 @@
+(** Termination analysis for loops and [goto] statements ([termination]). *)
+
+open Analyses
+open GoblintCil
+open TerminationPreprocessing
+
+(** Contains all loop counter variables (varinfo) and maps them to their corresponding loop statement. *)
+let loop_counters : stmt VarToStmt.t ref = ref VarToStmt.empty
+
+(** Checks whether a variable can be bounded. *)
+let check_bounded ctx varinfo =
+  let open IntDomain.IntDomTuple in
+  let exp = Lval (Var varinfo, NoOffset) in
+  match ctx.ask (EvalInt exp) with
+  | `Top -> false
+  | `Lifted v -> not (is_top_of (ikind v) v)
+  | `Bot -> failwith "Loop counter variable is Bot."
+
+(** We want to record termination information of loops and use the loop
+ * statements for that. We use this lifting because we need to have a
+ * lattice. *)
+module Statements = Lattice.Flat (CilType.Stmt) (Printable.DefaultNames)
+
+(** The termination analysis considering loops and gotos *)
+module Spec : Analyses.MCPSpec =
+struct
+
+  include Analyses.IdentitySpec
+
+  let name () = "termination"
+
+  module D = Lattice.Unit
+  module C = D
+  module V = struct
+    include UnitV
+    let is_write_only _ = true
+  end
+  module G = MapDomain.MapBot (Statements) (BoolDomain.MustBool)
+
+  let startstate _ = ()
+  let exitstate = startstate
+
+  let find_loop ~loop_counter =
+    VarToStmt.find loop_counter !loop_counters
+
+  (** Recognizes a call of [__goblint_bounded] to check the EvalInt of the
+   * respective loop counter variable at that position. *)
+  let special ctx (lval : lval option) (f : varinfo) (arglist : exp list) =
+    if !AnalysisState.postsolving then
+      match f.vname, arglist with
+        "__goblint_bounded", [Lval (Var loop_counter, NoOffset)] ->
+        (try
+           let loop_statement = find_loop ~loop_counter in
+           let is_bounded = check_bounded ctx loop_counter in
+           ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.global ()));
+           (* In case the loop is not bounded, a warning is created. *)
+           if not (is_bounded) then (
+             M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:Termination "The program might not terminate! (Loop analysis)"
+           );
+           ()
+         with Not_found ->
+           failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable.")
+      | _ -> ()
+    else ()
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.MustTermLoop loop_statement ->
+      let multithreaded = ctx.ask Queries.IsEverMultiThreaded in
+      (not multithreaded)
+      && (match G.find_opt (`Lifted loop_statement) (ctx.global ()) with
+            Some b -> b
+          | None -> false)
+    | Queries.MustTermAllLoops ->
+      let multithreaded = ctx.ask Queries.IsEverMultiThreaded in
+      if multithreaded then (
+        M.warn ~category:Termination "The program might not terminate! (Multithreaded)\n";
+        false)
+      else
+        G.for_all (fun _ term_info -> term_info) (ctx.global ())
+    | _ -> Queries.Result.top q
+
+end
+
+let () =
+  Cilfacade.register_preprocess (Spec.name ()) (new loopCounterVisitor loop_counters);
+  MCP.register_analysis (module Spec : MCPSpec)