TUM Practical Course Summer 2023: Termination Analyses

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/src/goblint.c

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

runningGob.sh

@@ -0,0 +1,26 @@
+#!/bin/bash
+make
+make install
+clear
+
+# set options and file for apron execution
+options_apron="--set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --enable warn.debug" #note: preprocessing first needs to be added to apron
+options_signs="--set "ana.activated[+]" signs --enable warn.debug" 
+options_term="--set "ana.activated[+]" termination --enable warn.debug --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra" 
+
+cfile_loops="tests/regression/55-loop-unrolling/01-simple-cases.c"      
+cfile_signs="tests/regression/99-tutorials/01-first.c"
+cfile_goto="tests/incremental/02-cfg-comparison/01-added-return-stmt.c"
+
+# run analysis, write cil output to file and enable visualization via html
+#./goblint $cfile_loops $options_apron --enable justcil > output.txt
+#./goblint $cfile_loops $options_apron --html 
+
+# run analysis, write cil output to file and enable visualization via html
+#./goblint -v $cfile_loops $options_term --enable justcil > output.txt
+./goblint $cfile_loops $options_term --html 
+
+# set up server to see visualizatino
+python3 -m http.server --directory result 8080
+#./goblint --enable dbg.debug tests/regression/55-loop-unrolling/01-simple-cases.c --enable ana.int.interval --set "ana.activated[+]" signs --enable justcil > output.txt
+

scripts/update_suite.rb

@@ -145,29 +145,30 @@ def collect_warnings
         @vars = $1
         @evals = $2
       end
+      if l =~ /\[NonTerminating\]/ then warnings[-1] = "nonterm" end # Get NonTerminating warning
       next unless l =~ /(.*)\(.*?\:(\d+)(?:\:\d+)?(?:-(?:\d+)(?:\:\d+)?)?\)/
       obj,i = $1,$2.to_i
 
-      ranking = ["other", "warn", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown"]
-      thiswarn =  case obj
-                    when /\(conf\. \d+\)/            then "race"
-                    when /Deadlock/                  then "deadlock"
-                    when /lock (before|after):/      then "deadlock"
-                    when /Assertion .* will fail/    then "fail"
-                    when /Assertion .* will succeed/ then "success"
-                    when /Assertion .* is unknown/   then "unknown"
-                    when /invariant confirmed/       then "success"
-                    when /invariant unconfirmed/     then "unknown"
-                    when /invariant refuted/         then "fail"
-                    when /^\[Warning\]/              then "warn"
-                    when /^\[Error\]/                then "warn"
-                    when /^\[Info\]/                 then "warn"
-                    when /^\[Success\]/              then "success"
-                    when /\[Debug\]/                 then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
-                    when /^  on line \d+ $/          then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
-                    when /^  on lines \d+..\d+ $/    then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
-                    else "other"
-                  end
+      ranking = ["other", "warn", "term", "nonterm", "race", "norace", "deadlock", "nodeadlock", "success", "fail", "unknown"]
+      thiswarn = case obj
+                 when /\(conf\. \d+\)/            then "race"
+                 when /Deadlock/                  then "deadlock"
+                 when /lock (before|after):/      then "deadlock"
+                 when /Assertion .* will fail/    then "fail"
+                 when /Assertion .* will succeed/ then "success"
+                 when /Assertion .* is unknown/   then "unknown"
+                 when /invariant confirmed/       then "success"
+                 when /invariant unconfirmed/     then "unknown"
+                 when /invariant refuted/         then "fail"
+                 when /^\[Warning\]/              then "warn"
+                 when /^\[Error\]/                then "warn"
+                 when /^\[Info\]/                 then "warn"
+                 when /^\[Success\]/              then "success"
+                 when /\[Debug\]/                 then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
+                 when /^  on line \d+ $/          then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
+                 when /^  on lines \d+..\d+ $/    then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
+                 else "other"
+                 end
       oldwarn = warnings[i]
       if oldwarn.nil? then
         warnings[i] = thiswarn
@@ -183,19 +184,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"
         check.call warnings[idx] == type
-      when "nowarn"
+      when "nonterm"
+        check.call warnings[idx] == type
+      when "nowarn", "term"
         check.call warnings[idx].nil?
       when "assert", "success"
         check.call warnings[idx] == "success"
@@ -306,6 +321,21 @@ def parse_tests (lines)
         end
       end
     end
+    case lines[0]
+    when /TODO|SKIP/
+      case lines[0]
+      when /NONTERM/
+        tests[-1] = "nonterm"
+        todo << -1
+      when /TERM/
+        tests[-1] = "term"
+        todo << -1
+      end
+    when /NONTERM/
+      tests[-1] = "nonterm"
+    when /TERM/
+      tests[-1] = "term"
+    end
     Tests.new(self, tests, tests_line, todo)
   end
 

src/analyses/apron/apronAnalysis.apron.ml

@@ -4,6 +4,7 @@ open Analyses
 
 include RelationAnalysis
 
+
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module Man = (val ApronDomain.get_manager ()) in
@@ -34,7 +35,8 @@ let get_spec (): (module MCPSpec) =
 let after_config () =
   let module Spec = (val get_spec ()) in
   MCP.register_analysis (module Spec : MCPSpec);
-  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+  GobConfig.set_string "ana.path_sens[+]" (Spec.name ())
+
 
 let _ =
   AfterConfig.register after_config

src/analyses/libraryFunctions.ml

@@ -302,6 +302,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 -> Assert { exp; check = true; refine = false });
   ]
 
 (** zstd functions.

src/analyses/loop_termination.ml

@@ -0,0 +1,116 @@
+(** Work in progress *)
+
+open Analyses
+open GoblintCil
+open TerminationPreprocessing
+
+exception PreProcessing of string
+
+(*
+let loop_heads () =
+  let module FileCfg =
+  struct
+    let file = !Cilfacade.current_file
+    module Cfg = (val !MyCFG.current_cfg)
+  end in
+  let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in
+  WitnessInvariant.loop_heads (* TODO: Unused *)
+*)
+
+(** Contains all loop counter variables (varinfo) and maps them to their corresponding loop statement. *)
+let loop_counters : stmt VarToStmt.t ref = ref VarToStmt.empty
+
+(** Contains the locations of the upjumping gotos *)
+let upjumping_gotos : location list ref = ref []
+
+(** Indicates the place in the code, right after a loop is exited. *)
+let loop_exit : varinfo ref = ref (makeVarinfo false "-error" Cil.intType)
+
+let is_loop_counter_var (x : varinfo) =
+  VarToStmt.mem x !loop_counters
+
+let is_loop_exit_indicator (x : varinfo) =
+  x = !loop_exit
+
+let no_upjumping_gotos () =
+  upjumping_gotos.contents = []
+
+(** 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 -> raise (PreProcessing "Loop variable is Bot")
+
+module UnitV =
+struct
+  include Printable.Unit
+  include StdV
+end
+
+(** 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) (* TODO: Use Basetype.CilStmt instead? *)
+
+(** The termination analysis considering loops and gotos *)
+module Spec : Analyses.MCPSpec =
+struct
+
+  (** Provides some default implementations *)
+  include Analyses.IdentitySpec
+
+  let name () = "termination"
+
+  module D = Lattice.Unit
+  module C = D
+  module V = UnitV
+  module G = MapDomain.MapBot (Statements) (BoolDomain.MustBool)
+
+  let startstate _ = D.bot ()
+  let exitstate = startstate
+
+  let assign ctx (lval : lval) (rval : exp) =
+    (* Detect assignment to loop counter variable *)
+    match lval, rval with
+      (Var y, NoOffset), Lval (Var x, NoOffset) when is_loop_exit_indicator y ->
+      (* Loop exit: Check whether loop counter variable is bounded *)
+      (* TODO: Move to special *)
+      let is_bounded = check_bounded ctx x in
+      let loop_statement = VarToStmt.find x !loop_counters in
+      let () = ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.global ())) in
+      ctx.local
+    | _ -> ctx.local
+
+  let special ctx (lval : lval option) (f : varinfo) (arglist : exp list) =
+    (* TODO: Implement check for our special loop exit indicator function *)
+    ctx.local
+
+  (** Checks whether a new thread was spawned some time. We want to discard
+   * any knowledge about termination then (see query function) *)
+  let must_be_single_threaded_since_start ctx =
+    ctx.ask (Queries.MustBeSingleThreaded {since_start = true})
+
+  (** Provides information to Goblint *)
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.MustTermLoop loop_statement ->
+      (match G.find_opt (`Lifted loop_statement) (ctx.global ()) with
+         Some b -> b
+       | None -> false)
+      && must_be_single_threaded_since_start ctx
+    | Queries.MustTermProg ->
+      G.for_all (fun _ term_info -> term_info) (ctx.global ())
+      && no_upjumping_gotos ()
+      && must_be_single_threaded_since_start ctx
+    | _ -> Queries.Result.top q
+
+end
+
+let () =
+  (* Register the preprocessing *)
+  Cilfacade.register_preprocess_cil (Spec.name ()) (new loopCounterVisitor loop_counters upjumping_gotos loop_exit);
+  (* Register this analysis within the master control program *)
+  MCP.register_analysis (module Spec : MCPSpec)