Merge branch 'master' into improve-multi-threaded-valid-memcleanup

.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,10 @@ 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!)
+        if: ${{ matrix.apron }}
+        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

@@ -32,6 +32,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; });
     ("__builtin___strncat_chk", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; });
     ("memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
+    ("__builtin_memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
     ("memchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]);
     ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]);
     ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]);
@@ -62,6 +63,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("localeconv", unknown ~attrs:[ThreadUnsafe] []);
     ("localtime", unknown ~attrs:[ThreadUnsafe] [drop "time" [r]]);
     ("strlen", special [__ "s" [r]] @@ fun s -> Strlen s);
+    ("__builtin_strlen", special [__ "s" [r]] @@ fun s -> Strlen s);
     ("strstr", special [__ "haystack" [r]; __ "needle" [r]] @@ fun haystack needle -> Strstr { haystack; needle; });
     ("strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; });
     ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]);
@@ -146,6 +148,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]);
     ("atomic_load", unknown [drop "obj" [r]]);
     ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]);
+    ("_Exit", special [drop "status" []] @@ Abort);
   ]
 
 (** C POSIX library functions.
@@ -335,7 +338,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]);
     ("regfree", unknown [drop "preg" [f_deep]]);
     ("ffs", unknown [drop "i" []]);
-    ("_exit", special [drop "status" []] Abort);
+    ("_exit", special [drop "status" []] @@ Abort);
     ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]);
     ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r])));
     ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]);
@@ -505,6 +508,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_unreachable", special' [] @@ fun () -> if get_bool "sem.builtin_unreachable.dead_code" then Abort else Unknown); (* https://github.com/sosy-lab/sv-benchmarks/issues/1296 *)
     ("__assert_rtn", special [drop "func" [r]; drop "file" [r]; drop "line" []; drop "exp" [r]] @@ Abort); (* MacOS's built-in assert *)
     ("__assert_fail", special [drop "assertion" [r]; drop "file" [r]; drop "line" []; drop "function" [r]] @@ Abort); (* gcc's built-in assert *)
+    ("__assert", special [drop "assertion" [r]; drop "file" [r]; drop "line" []] @@ Abort); (* header says: The following is not at all used here but needed for standard compliance. *)
     ("__builtin_return_address", unknown [drop "level" []]);
     ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r])));
     ("__builtin_add_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]);
@@ -576,6 +580,10 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
+    ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
+    ("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
+    ("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
+    ("__fread_unlocked_chk_warn", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__read_chk", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []; drop "__buflen" []]);
     ("__read_alias", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []]);
     ("__readlink_chk", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []; drop "buflen" []]);
@@ -718,6 +726,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.
@@ -972,6 +981,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic);
     ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
     ("__VERIFIER_nondet_int", unknown []);  (* declare invalidate actions to prevent invalidating globals when extern in regression tests *)
+    ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
   ]
 
 let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[

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)

src/analyses/memLeak.ml

@@ -135,4 +135,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec : MCPSpec)

src/analyses/region.ml

@@ -177,7 +177,15 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
-  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx =
+    match ctx.local with
+    | `Lifted reg ->
+      let old_regpart = ctx.global () in
+      let regpart, reg = List.fold_right Reg.assign_escape args (old_regpart, reg) in
+      if not (RegPart.leq regpart old_regpart) then
+        ctx.sideg () regpart;
+      `Lifted reg
+    | x -> x
 
   let exitstate v = `Lifted (RegMap.bot ())