diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 5635ebbeea..0208af7c7a 100644 --- a/.github/workflows/coverage.yml +++ b/.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 diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 65dfbe7bac..8604e7f52c 100644 --- a/.github/workflows/locked.yml +++ b/.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 diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 6c23c7cdd4..990b7cfb49 100644 --- a/.github/workflows/unlocked.yml +++ b/.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 diff --git a/conf/svcomp.json b/conf/svcomp.json index 73f99500b9..cc6d1e303a 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -71,7 +71,9 @@ "octagon", "wideningThresholds", "loopUnrollHeuristic", - "memsafetySpecification" + "memsafetySpecification", + "termination", + "specification" ] } }, diff --git a/docs/developer-guide/firstanalysis.md b/docs/developer-guide/firstanalysis.md index 0923e792cd..4eb35e7f5d 100644 --- a/docs/developer-guide/firstanalysis.md +++ b/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). diff --git a/lib/goblint/runtime/include/goblint.h b/lib/goblint/runtime/include/goblint.h index b0af41616e..af87035d33 100644 --- a/lib/goblint/runtime/include/goblint.h +++ b/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); \ No newline at end of file diff --git a/lib/goblint/runtime/src/goblint.c b/lib/goblint/runtime/src/goblint.c index bc176f93a6..cbcb7cf505 100644 --- a/lib/goblint/runtime/src/goblint.c +++ b/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) { + } \ No newline at end of file diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index ca408a513a..2722b3ddb5 100755 --- a/scripts/update_suite.rb +++ b/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 diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 13f549fc44..8b128eb271 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -196,7 +196,7 @@ 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 @@ -204,7 +204,6 @@ struct 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 diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 72a4261cb5..55da9f6635 100644 --- a/src/analyses/libraryDesc.ml +++ b/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? *) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f84fe1d4e3..0a9c03a32e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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.[ diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml new file mode 100644 index 0000000000..10e0f5c5f4 --- /dev/null +++ b/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) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 336943d407..b1b57b6694 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -135,4 +135,4 @@ struct end let _ = - MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 652526543c..5b10586aba 100644 --- a/src/analyses/region.ml +++ b/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 ()) diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml deleted file mode 100644 index 0563730fb2..0000000000 --- a/src/analyses/termination.ml +++ /dev/null @@ -1,239 +0,0 @@ -(** Termination analysis of loops using counter variables ([term]). *) - -open Batteries -open GoblintCil -open Analyses - -module M = Messages -let (||?) a b = match a,b with Some x,_ | _, Some x -> Some x | _ -> None - -module TermDomain = struct - include SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All Variables" end) -end - -(* some kind of location string suitable for variable names? *) -let show_location_id l = - string_of_int l.line ^ "_" ^ string_of_int l.column - -class loopCounterVisitor (fd : fundec) = object(self) - inherit nopCilVisitor - method! vstmt s = - let action s = match s.skind with - | Loop (b, loc, eloc, _, _) -> - (* insert loop counter variable *) - let name = "term"^show_location_id loc in - let typ = intType in (* TODO the type should be the same as the one of the original loop counter *) - let v = Cilfacade.create_var (makeLocalVar fd name ~init:(SingleInit zero) typ) in - (* make an init stmt since the init above is apparently ignored *) - let init_stmt = mkStmtOneInstr @@ Set (var v, zero, loc, eloc) in - (* increment it every iteration *) - let inc_stmt = mkStmtOneInstr @@ Set (var v, increm (Lval (var v)) 1, loc, eloc) in - b.bstmts <- inc_stmt :: b.bstmts; - let nb = mkBlock [init_stmt; mkStmt s.skind] in - s.skind <- Block nb; - s - | _ -> s - in ChangeDoChildrenPost (s, action) -end - -let loopBreaks : (int, location) Hashtbl.t = Hashtbl.create 13 (* break stmt sid -> corresponding loop *) -class loopBreaksVisitor (fd : fundec) = object(self) - inherit nopCilVisitor - method! vstmt s = - (match s.skind with - | Loop (b, loc, eloc, Some continue, Some break) -> Hashtbl.add loopBreaks break.sid loc (* TODO: use eloc? *) - | Loop _ -> failwith "Termination.preprocess: every loop should have a break and continue stmt after prepareCFG" - | _ -> ()); - DoChildren -end - -(* if the given block contains a goto while_break.* we have the termination condition for a loop *) -let exits = function - | { bstmts = [{ skind = Goto (stmt, loc); _ }]; _ } -> Hashtbl.find_option loopBreaks !stmt.sid - | _ -> None (* TODO handle return (need to find out what loop we are in) *) - -let lvals_of_expr = - let rec f a = function - | Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ | AddrOfLabel _ -> a - | Lval l | AddrOf l | StartOf l -> l :: a - | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,e) | Imag e | Real e -> f a e - | BinOp (_,e1,e2,_) -> f a e1 @ f a e2 - | Question (c,t,e,_) -> f a c @ f a t @ f a e - in f [] - -let loopVars : (location, lval) Hashtbl.t = Hashtbl.create 13 (* loop location -> lval used for exit *) -class loopVarsVisitor (fd : fundec) = object - inherit nopCilVisitor - method! vstmt s = - let add_exit_cond e loc = - match lvals_of_expr e with - | [lval] when Cilfacade.typeOf e |> isArithmeticType -> Hashtbl.add loopVars loc lval - | _ -> () - in - (match s.skind with - | If (e, tb, fb, loc, eloc) -> Option.map_default (add_exit_cond e) () (exits tb ||? exits fb) - | _ -> ()); - DoChildren -end - -let stripCastsDeep e = - let v = object - inherit nopCilVisitor - method! vexpr e = ChangeTo (stripCasts e) - end - in visitCilExpr v e - -(* keep the enclosing loop for statements *) -let cur_loop = ref None (* current loop *) -let cur_loop' = ref None (* for nested loops *) -let makeVar fd loc name = - let id = name ^ "__" ^ show_location_id loc in - try List.find (fun v -> v.vname = id) fd.slocals - with Not_found -> - let typ = intType in (* TODO the type should be the same as the one of the original loop counter *) - Cilfacade.create_var (makeLocalVar fd id ~init:(SingleInit zero) typ) -let f_assume = Lval (var (emptyFunction "__goblint_assume").svar) -let f_check = Lval (var (emptyFunction "__goblint_check").svar) -class loopInstrVisitor (fd : fundec) = object(self) - inherit nopCilVisitor - method! vstmt s = - (* TODO: use Loop eloc? *) - (match s.skind with - | Loop (_, loc, eloc, _, _) -> - cur_loop' := !cur_loop; - cur_loop := Some loc - | _ -> ()); - let action s = - (* first, restore old cur_loop *) - (match s.skind with - | Loop (_, loc, eloc, _, _) -> - cur_loop := !cur_loop'; - | _ -> ()); - let in_loop () = Option.is_some !cur_loop && Hashtbl.mem loopVars (Option.get !cur_loop) in - match s.skind with - | Loop (b, loc, eloc, Some continue, Some break) when Hashtbl.mem loopVars loc -> - (* find loop var for current loop *) - let x = Hashtbl.find loopVars loc in - (* insert loop counter and diff to loop var *) - let t = var @@ makeVar fd loc "t" in - let d1 = var @@ makeVar fd loc "d1" in - let d2 = var @@ makeVar fd loc "d2" in - (* make init stmts *) - let t_init = mkStmtOneInstr @@ Set (t, zero, loc, eloc) in - let d1_init = mkStmtOneInstr @@ Set (d1, Lval x, loc, eloc) in - let d2_init = mkStmtOneInstr @@ Set (d2, Lval x, loc, eloc) in - (* increment/decrement in every iteration *) - let t_inc = mkStmtOneInstr @@ Set (t, increm (Lval t) 1, loc, eloc) in - let d1_inc = mkStmtOneInstr @@ Set (d1, increm (Lval d1) (-1), loc, eloc) in - let d2_inc = mkStmtOneInstr @@ Set (d2, increm (Lval d2) 1 , loc, eloc) in - let typ = intType in - let e1 = BinOp (Eq, Lval t, BinOp (MinusA, Lval x, Lval d1, typ), typ) in - let e2 = BinOp (Eq, Lval t, BinOp (MinusA, Lval d2, Lval x, typ), typ) in - let inv1 = mkStmtOneInstr @@ Call (None, f_assume, [e1], loc, eloc) in - let inv2 = mkStmtOneInstr @@ Call (None, f_assume, [e2], loc, eloc) in - (match b.bstmts with - | cont :: cond :: ss -> - (* changing succs/preds directly doesn't work -> need to replace whole stmts *) - b.bstmts <- cont :: cond :: inv1 :: inv2 :: d1_inc :: d2_inc :: t_inc :: ss; - let nb = mkBlock [t_init; d1_init; d2_init; mkStmt s.skind] in - s.skind <- Block nb; - | _ -> ()); - s - | Loop (b, loc, eloc, Some continue, Some break) -> - print_endline @@ "WARN: Could not determine loop variable for loop at " ^ CilType.Location.show loc; - s - | _ when Hashtbl.mem loopBreaks s.sid -> (* after a loop, we check that t is bounded/positive (no overflow happened) *) - let loc = Hashtbl.find loopBreaks s.sid in - let t = var @@ makeVar fd loc "t" in - let e3 = BinOp (Ge, Lval t, zero, intType) in - let inv3 = mkStmtOneInstr @@ Call (None, f_check, [e3], loc, locUnknown) in - let nb = mkBlock [mkStmt s.skind; inv3] in - s.skind <- Block nb; - s - | Instr [Set (lval, e, loc, eloc)] when in_loop () -> - (* find loop var for current loop *) - let cur_loop = Option.get !cur_loop in - let x = Hashtbl.find loopVars cur_loop in - if x <> lval then - s - else (* we only care about the loop var *) - let d1 = makeVar fd cur_loop "d1" in - let d2 = makeVar fd cur_loop "d2" in - (match stripCastsDeep e with - | BinOp (op, Lval x', e2, typ) when (op = PlusA || op = MinusA) && x' = x && isArithmeticType typ -> (* TODO x = 1 + x, MinusA! *) - (* increase diff by same expr *) - let d1_inc = mkStmtOneInstr @@ Set (var d1, BinOp (PlusA, Lval (var d1), e2, typ), loc, eloc) in - let d2_inc = mkStmtOneInstr @@ Set (var d2, BinOp (PlusA, Lval (var d2), e2, typ), loc, eloc) in - let nb = mkBlock [d1_inc; d2_inc; mkStmt s.skind] in - s.skind <- Block nb; - s - | _ -> - (* otherwise diff is e - counter *) - let t = makeVar fd cur_loop "t" in - let te = Cilfacade.typeOf e in - let dt1 = mkStmtOneInstr @@ Set (var d1, BinOp (MinusA, Lval x, Lval (var t), te), loc, eloc) in - let dt2 = mkStmtOneInstr @@ Set (var d2, BinOp (MinusA, Lval x, Lval (var t), te), loc, eloc) in - let nb = mkBlock [mkStmt s.skind; dt1; dt2] in - s.skind <- Block nb; - s - ) - | _ -> s - in - ChangeDoChildrenPost (s, action) -end - - -module Spec = -struct - include Analyses.IdentitySpec - - let name () = "term" - module D = TermDomain - module C = TermDomain - - (* queries *) - (*let query ctx (q:Queries.t) : Queries.Result.t =*) - (*match q with*) - (*| Queries.MustTerm loc -> `Bool (D.mem v ctx.local)*) - (*| _ -> Queries.Result.top ()*) - - (* transfer functions *) - - let branch ctx (exp:exp) (tv:bool) : D.t = - ctx.local - (* if the then-block contains a goto while_break.* we have the termination condition for a loop *) - (* match !MyCFG.current_node with *) - (* | Some (MyCFG.Statement({ skind = If (e, tb, fb, loc) })) -> *) - (* let str_exit b = match exits b with Some loc -> string_of_int loc.line | None -> "None" in *) - (* M.debug @@ *) - (* "\nCil-exp: " ^ sprint d_exp e *) - (* (*^ "; Goblint-exp: " ^ sprint d_exp exp*) *) - (* ^ "; Goblint: " ^ sprint Queries.Result.pretty (ctx.ask (Queries.EvalInt exp)) *) - (* ^ "\nCurrent block: " ^ (if tv then "Then" else "Else") *) - (* ^ "\nThen block (exits " ^ str_exit tb ^ "): " ^ sprint d_block tb *) - (* ^ "\nElse block (exits " ^ str_exit fb ^ "): " ^ sprint d_block fb *) - (* ; *) - (* ctx.local *) - (* | _ -> ctx.local *) - - let startstate v = D.bot () - let threadenter ctx ~multiple lval f args = [D.bot ()] - let exitstate v = D.bot () -end - -class recomputeVisitor (fd : fundec) = object(self) - inherit nopCilVisitor - method! vfunc fd = - computeCFGInfo fd true; - SkipChildren -end - -let _ = - (* Cilfacade.register_preprocess Spec.name (new loopCounterVisitor); *) - Cilfacade.register_preprocess (Spec.name ()) (new loopBreaksVisitor); - Cilfacade.register_preprocess (Spec.name ()) (new loopVarsVisitor); - Cilfacade.register_preprocess (Spec.name ()) (new loopInstrVisitor); - Cilfacade.register_preprocess (Spec.name ()) (new recomputeVisitor); - Hashtbl.clear loopBreaks; (* because the sids are now different *) - Cilfacade.register_preprocess (Spec.name ()) (new loopBreaksVisitor); - MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index 6bd466caef..a751ae074a 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -21,6 +21,8 @@ struct module D = Flag module C = Flag module P = IdentityP (D) + module V = UnitV + module G = BoolDomain.MayBool let name () = "threadflag" @@ -44,6 +46,7 @@ struct match x with | Queries.MustBeSingleThreaded _ -> not (Flag.is_multi ctx.local) (* If this analysis can tell, it is the case since the start *) | Queries.MustBeUniqueThread -> not (Flag.is_not_main ctx.local) + | Queries.IsEverMultiThreaded -> (ctx.global () : bool) (* requires annotation to compile *) (* This used to be in base but also commented out. *) (* | Queries.MayBePublic _ -> Flag.is_multi ctx.local *) | _ -> Queries.Result.top x @@ -64,6 +67,7 @@ struct [create_tid f] let threadspawn ctx ~multiple lval f args fctx = + ctx.sideg () true; if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then ctx.emit Events.EnterMultiThreaded; D.join ctx.local (Flag.get_main ()) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 43707acd1e..5895f242c9 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -200,6 +200,46 @@ struct M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv in + let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = + + let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = + let loc = loc_of_location location_invariant.location in + let inv = location_invariant.value in + let msgLoc: M.Location.t = CilLocation loc in + + match Locator.find_opt locator loc with + | Some nodes -> + unassume_nodes_invariant ~loc ~nodes inv + | None -> + M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv + in + + let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) = + let loc = loc_of_location loop_invariant.location in + let inv = loop_invariant.value in + let msgLoc: M.Location.t = CilLocation loc in + + match Locator.find_opt loop_locator loc with + | Some nodes -> + unassume_nodes_invariant ~loc ~nodes inv + | None -> + M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv + in + + let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) = + let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in + match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with + | true, LocationInvariant x -> + unassume_location_invariant x + | true, LoopInvariant x -> + unassume_loop_invariant x + | false, (LocationInvariant _ | LoopInvariant _) -> + M.info_noloc ~category:Witness "disabled invariant of type %s" target_type + in + + List.iter validate_invariant invariant_set.content + in + match YamlWitness.entry_type_enabled target_type, entry.entry_type with | true, LocationInvariant x -> unassume_location_invariant x @@ -207,7 +247,9 @@ struct unassume_loop_invariant x | true, PreconditionLoopInvariant x -> unassume_precondition_loop_invariant x - | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) -> + | true, InvariantSet x -> + unassume_invariant_set x + | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> M.info_noloc ~category:Witness "disabled entry of type %s" target_type | _ -> M.info_noloc ~category:Witness "cannot unassume entry of type %s" target_type diff --git a/src/autoTune.ml b/src/autoTune.ml index 06347f3190..5e0034e6eb 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -180,7 +180,7 @@ let enableAnalyses anas = List.iter (GobConfig.set_auto "ana.activated[+]") anas (*If only one thread is used in the program, we can disable most thread analyses*) -(*The exceptions are analyses that are depended on by others: base -> mutex -> mutexEvents, access*) +(*The exceptions are analyses that are depended on by others: base -> mutex -> mutexEvents, access; termination -> threadflag *) (*escape is also still enabled, because otherwise we get a warning*) (*does not consider dynamic calls!*) @@ -227,8 +227,8 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = | ValidMemcleanup -> (* Enable the memLeak analysis *) let memLeakAna = ["memLeak"] in if (get_int "ana.malloc.unique_address_count") < 1 then ( - print_endline "Setting \"ana.malloc.unique_address_count\" to 1"; - set_int "ana.malloc.unique_address_count" 1; + print_endline "Setting \"ana.malloc.unique_address_count\" to 5"; + set_int "ana.malloc.unique_address_count" 5; ); print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\""; enableAnalyses memLeakAna @@ -243,6 +243,14 @@ let focusOnSpecification (spec: Svcomp.Specification.t) = | NoDataRace -> (*enable all thread analyses*) print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\""; enableAnalyses notNeccessaryThreadAnalyses; + | Termination -> + let terminationAnas = ["termination"; "threadflag"; "apron"] in + print_endline @@ "Specification: Termination -> enabling termination analyses \"" ^ (String.concat ", " terminationAnas) ^ "\""; + enableAnalyses terminationAnas; + set_string "sem.int.signed_overflow" "assume_none"; + set_bool "ana.int.interval" true; + set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *) + () | NoOverflow -> (*We focus on integer analysis*) set_bool "ana.int.def_exc" true; set_bool "ana.int.interval" true @@ -458,7 +466,6 @@ let wideningOption factors file = print_endline "Enabled widening thresholds"; } - let estimateComplexity factors file = let pathsEstimate = factors.loops + factors.controlFlowStatements / 90 in let operationEstimate = factors.instructions + (factors.expressions / 60) in @@ -487,6 +494,11 @@ let chooseFromOptions costTarget options = let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_list "ana.autotune.activated" +let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ()) + +let specificationIsActivated () = + isActivated "specification" && get_string "ana.specification" <> "" + let chooseConfig file = let factors = collectFactors visitCilFileSameGlobals file in let fileCompplexity = estimateComplexity factors file in @@ -506,8 +518,8 @@ let chooseConfig file = if isActivated "mallocWrappers" then findMallocWrappers (); - if isActivated "specification" && get_string "ana.specification" <> "" then - focusOnSpecification (); + (* if specificationIsActivated () then + focusOnSpecification (); *) if isActivated "enums" && hasEnums file then set_bool "ana.int.enums" true; @@ -520,10 +532,10 @@ let chooseConfig file = let options = [] in let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in - let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in + (* Termination analysis uses apron in a different configuration. *) + let options = if isActivated "octagon" && not (isTerminationTask ()) then (apronOctagonOption factors file)::options else options in let options = if isActivated "wideningThresholds" then (wideningOption factors file)::options else options in List.iter (fun o -> o.activate ()) @@ chooseFromOptions (totalTarget - fileCompplexity) options - let reset_lazy () = ResettableLazy.reset functionCallMaps diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml index b577e3499f..681eb79007 100644 --- a/src/cdomains/regionDomain.ml +++ b/src/cdomains/regionDomain.ml @@ -157,13 +157,13 @@ struct (* This is the main logic for dealing with the bullet and finding it an * owner... *) - let add_set (s:set) llist (p,m:t): t = + let add_set ?(escape=false) (s:set) llist (p,m:t): t = if RS.has_bullet s then let f key value (ys, x) = if RS.has_bullet value then key::ys, RS.join value x else ys,x in let ys,x = RegMap.fold f m (llist, RS.remove_bullet s) in let x = RS.remove_bullet x in - if RS.is_empty x then + if not escape && RS.is_empty x then p, RegMap.add_list_set llist RS.single_bullet m else RegPart.add x p, RegMap.add_list_set ys x m @@ -215,6 +215,25 @@ struct | Some (_,x,_) -> p, RegMap.add x RS.single_bullet m | _ -> p,m + (* Copied & modified from assign. *) + let assign_escape (rval: exp) (st: t): t = + (* let _ = printf "%a = %a\n" (printLval plainCilPrinter) lval (printExp plainCilPrinter) rval in *) + let t = Cilfacade.typeOf rval in + if isPointerType t then begin (* TODO: this currently allows function pointers, e.g. in iowarrior, but should it? *) + match eval_exp rval with + (* TODO: should offs_x matter? *) + | Some (deref_y,y,offs_y) -> + let (p,m) = st in begin + match is_global y with + | true -> + add_set ~escape:true (RS.single_vf y) [] st + | false -> + add_set ~escape:true (RegMap.find y m) [y] st + end + | _ -> st + end else + st + let related_globals (deref_vfd: eval_t) (p,m: t): elt list = let add_o o2 (v,o) = (v, F.add_offset o o2) in match deref_vfd with diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml index 05a93741f8..fd76e1bb67 100644 --- a/src/common/framework/analysisState.ml +++ b/src/common/framework/analysisState.ml @@ -7,6 +7,8 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false +(** Whether the termination analysis detects the program as non-terminating *) +let svcomp_may_not_terminate = ref false (** Whether an invalid free happened *) let svcomp_may_invalid_free = ref false diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index ba57074e5a..26a2f082a4 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -74,19 +74,18 @@ let print (fileAST: file) = let rmTemps fileAST = RmUnused.removeUnused fileAST - let visitors = ref [] let register_preprocess name visitor_fun = visitors := !visitors @ [name, visitor_fun] let do_preprocess ast = - let f fd (name, visitor_fun) = - (* this has to be done here, since the settings aren't available when register_preprocess is called *) - if List.mem name (get_string_list "ana.activated") then - ignore @@ visitCilFunction (visitor_fun fd) fd - in - iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) !visitors | _ -> ()) - + (* this has to be done here, since the settings aren't available when register_preprocess is called *) + let active_visitors = List.filter_map (fun (name, visitor_fun) -> if List.mem name (get_string_list "ana.activated") then Some visitor_fun else None) !visitors in + let f fd visitor_fun = ignore @@ visitCilFunction (visitor_fun fd) fd in + if active_visitors <> [] then + iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) active_visitors | _ -> ()) + else + () (** @raise GoblintCil.FrontC.ParseError @raise GoblintCil.Errormsg.Error *) @@ -667,9 +666,16 @@ let find_stmt_sid sid = try IntH.find pseudo_return_stmt_sids sid with Not_found -> IntH.find (ResettableLazy.force stmt_sids) sid +module FunLocH = Hashtbl.Make(CilType.Fundec) +module LocSet = Hashtbl.Make(CilType.Location) + +(** Contains the locations of the upjumping gotos and the respective functions + * they are being called in. *) +let funs_with_upjumping_gotos: unit LocSet.t FunLocH.t = FunLocH.create 13 -let reset_lazy () = +let reset_lazy ?(keepupjumpinggotos=false) () = StmtH.clear pseudo_return_to_fun; + if not keepupjumpinggotos then FunLocH.clear funs_with_upjumping_gotos; ResettableLazy.reset stmt_fundecs; ResettableLazy.reset varinfo_fundecs; ResettableLazy.reset name_fundecs; @@ -700,4 +706,4 @@ let add_function_declarations (file: Cil.file): unit = in let fun_decls = List.filter_map declaration_from_GFun functions in let globals = upto_last_type @ fun_decls @ non_types @ functions in - file.globals <- globals + file.globals <- globals \ No newline at end of file diff --git a/src/common/util/messageCategory.ml b/src/common/util/messageCategory.ml index c70b8faf5f..41c9bc08e1 100644 --- a/src/common/util/messageCategory.ml +++ b/src/common/util/messageCategory.ml @@ -46,6 +46,7 @@ type category = | Imprecise | Witness | Program + | Termination [@@deriving eq, ord, hash] type t = category [@@deriving eq, ord, hash] @@ -204,6 +205,7 @@ let should_warn e = | Imprecise -> "imprecise" | Witness -> "witness" | Program -> "program" + | Termination -> "termination" (* Don't forget to add option to schema! *) in get_bool ("warn." ^ (to_string e)) @@ -224,6 +226,7 @@ let path_show e = | Imprecise -> ["Imprecise"] | Witness -> ["Witness"] | Program -> ["Program"] + | Termination -> ["Termination"] let show x = String.concat " > " (path_show x) @@ -263,6 +266,7 @@ let categoryName = function | Overflow -> "Overflow"; | DivByZero -> "DivByZero") | Float -> "Float" + | Termination -> "Termination" let from_string_list (s: string list) = @@ -283,6 +287,7 @@ let from_string_list (s: string list) = | "imprecise" -> Imprecise | "witness" -> Witness | "program" -> Program + | "termination" -> Termination | _ -> Unknown let to_yojson x = `List (List.map (fun x -> `String x) (path_show x)) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 40669ff729..9a6a66ee6b 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -352,7 +352,7 @@ "description": "List of path-sensitive analyses", "type": "array", "items": { "type": "string" }, - "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp" ] + "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak" ] }, "ctx_insens": { "title": "ana.ctx_insens", @@ -2105,6 +2105,12 @@ "type": "boolean", "default": true }, + "termination": { + "title": "warn.termination", + "description": "Non-Termination warning", + "type": "boolean", + "default": true + }, "unknown": { "title": "warn.unknown", "description": "Unknown (of string) warnings", @@ -2418,6 +2424,16 @@ "type": "boolean", "default": false }, + "format-version": { + "title": "witness.yaml.format-version", + "description": "YAML witness format version", + "type": "string", + "enum": [ + "0.1", + "2.0" + ], + "default": "0.1" + }, "entry-types": { "title": "witness.yaml.entry-types", "description": "YAML witness entry types to output/input.", @@ -2430,7 +2446,8 @@ "flow_insensitive_invariant", "precondition_loop_invariant", "loop_invariant_certificate", - "precondition_loop_invariant_certificate" + "precondition_loop_invariant_certificate", + "invariant_set" ] }, "default": [ @@ -2438,7 +2455,24 @@ "loop_invariant", "flow_insensitive_invariant", "loop_invariant_certificate", - "precondition_loop_invariant_certificate" + "precondition_loop_invariant_certificate", + "invariant_set" + ] + }, + "invariant-types": { + "title": "witness.yaml.invariant-types", + "description": "YAML witness invariant types to output/input.", + "type": "array", + "items": { + "type": "string", + "enum": [ + "location_invariant", + "loop_invariant" + ] + }, + "default": [ + "location_invariant", + "loop_invariant" ] }, "path": { diff --git a/src/domains/queries.ml b/src/domains/queries.ml index c706339bf2..52038fcf77 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -127,6 +127,9 @@ type _ t = | MayAccessed: AccessDomain.EventSet.t t | MayBeTainted: AD.t t | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t + | MustTermLoop: stmt -> MustBool.t t + | MustTermAllLoops: MustBool.t t + | IsEverMultiThreaded: MayBool.t t | TmpSpecial: Mval.Exp.t -> ML.t t type 'a result = 'a @@ -193,6 +196,9 @@ struct | MayAccessed -> (module AccessDomain.EventSet) | MayBeTainted -> (module AD) | MayBeModifiedSinceSetjmp _ -> (module VS) + | MustTermLoop _ -> (module MustBool) + | MustTermAllLoops -> (module MustBool) + | IsEverMultiThreaded -> (module MayBool) | TmpSpecial _ -> (module ML) (** Get bottom result for query. *) @@ -258,6 +264,9 @@ struct | MayAccessed -> AccessDomain.EventSet.top () | MayBeTainted -> AD.top () | MayBeModifiedSinceSetjmp _ -> VS.top () + | MustTermLoop _ -> MustBool.top () + | MustTermAllLoops -> MustBool.top () + | IsEverMultiThreaded -> MayBool.top () | TmpSpecial _ -> ML.top () end @@ -319,6 +328,9 @@ struct | Any (EvalMutexAttr _ ) -> 50 | Any ThreadCreateIndexedNode -> 51 | Any ThreadsJoinedCleanly -> 52 + | Any (MustTermLoop _) -> 53 + | Any MustTermAllLoops -> 54 + | Any IsEverMultiThreaded -> 55 | Any (TmpSpecial _) -> 53 | Any (IsAllocVar _) -> 54 @@ -362,6 +374,7 @@ struct | Any (IsHeapVar v1), Any (IsHeapVar v2) -> CilType.Varinfo.compare v1 v2 | Any (IsAllocVar v1), Any (IsAllocVar v2) -> CilType.Varinfo.compare v1 v2 | Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2 + | Any (MustTermLoop s1), Any (MustTermLoop s2) -> CilType.Stmt.compare s1 s2 | Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2 | Any (EvalJumpBuf e1), Any (EvalJumpBuf e2) -> CilType.Exp.compare e1 e2 | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) @@ -401,6 +414,7 @@ struct | Any (IterVars i) -> 0 | Any (PathQuery (i, q)) -> 31 * i + hash (Any q) | Any (IsHeapVar v) -> CilType.Varinfo.hash v + | Any (MustTermLoop s) -> CilType.Stmt.hash s | Any (IsAllocVar v) -> CilType.Varinfo.hash v | Any (IsMultiple v) -> CilType.Varinfo.hash v | Any (EvalThread e) -> CilType.Exp.hash e @@ -471,6 +485,9 @@ struct | Any MayBeTainted -> Pretty.dprintf "MayBeTainted" | Any DYojson -> Pretty.dprintf "DYojson" | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf + | Any (MustTermLoop s) -> Pretty.dprintf "MustTermLoop %a" CilType.Stmt.pretty s + | Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops" + | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv end diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index eec811afc4..a37a3043c2 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -88,6 +88,22 @@ struct | `Right _ -> true end +module GVarFC (V:SpecSysVar) (C:Printable.S) = +struct + include Printable.Either (V) (Printable.Prod (CilType.Fundec) (C)) + let name () = "FromSpec" + let spec x = `Left x + let call (x, c) = `Right (x, c) + + (* from Basetype.Variables *) + let var_id = show + let node _ = MyCFG.Function Cil.dummyFunDec + let pretty_trace = pretty + let is_write_only = function + | `Left x -> V.is_write_only x + | `Right _ -> true +end + module GVarG (G: Lattice.S) (C: Printable.S) = struct module CSet = @@ -596,6 +612,12 @@ struct let is_write_only _ = false end +module UnitV = +struct + include Printable.Unit + include StdV +end + module VarinfoV = struct include CilType.Varinfo (* TODO: or Basetype.Variables? *) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index cc54c91a5a..b1bbc73660 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1687,6 +1687,10 @@ struct ) in List.iter handle_path (S.paths_as_set conv_ctx); + if !AnalysisState.should_warn && List.mem "termination" @@ get_string_list "ana.activated" then ( + AnalysisState.svcomp_may_not_terminate := true; + M.warn ~category:Termination "The program might not terminate! (Longjmp)" + ); S.D.bot () | _ -> S.special conv_ctx lv f args let threadenter ctx = S.threadenter (conv ctx) @@ -1697,6 +1701,149 @@ struct let event ctx e octx = S.event (conv ctx) e (conv octx) end + +(** Add cycle detection in the context-sensitive dynamic function call graph to an analysis *) +module RecursionTermLifter (S: Spec) + : Spec with module D = S.D + and module C = S.C += +(* two global invariants: + - S.V -> S.G + Needed to store the previously built global invariants + - fundec * S.C -> (Set (fundec * S.C)) + The second global invariant maps from the callee fundec and context to a set of caller fundecs and contexts. + This structure therefore stores the context-sensitive call graph. + For example: + let the function f in context c call function g in context c'. + In the global invariant structure it would be stored like this: (g,c') -> {(f, c)} +*) + +struct + include S + + (* contains all the callee fundecs and contexts *) + module V = GVarFC(S.V)(S.C) + + (* Tuple containing the fundec and context of a caller *) + module Call = Printable.Prod (CilType.Fundec) (S.C) + + (* Set containing multiple caller tuples *) + module CallerSet = SetDomain.Make (Call) + + module G = + struct + include Lattice.Lift2 (G) (CallerSet) (Printable.DefaultNames) + + let spec = function + | `Bot -> G.bot () + | `Lifted1 x -> x + | _ -> failwith "RecursionTermLifter.spec" + + let callers = function + | `Bot -> CallerSet.bot () + | `Lifted2 x -> x + | _ -> failwith "RecursionTermLifter.callGraph" + + let create_spec spec = `Lifted1 spec + let create_singleton_caller caller = `Lifted2 (CallerSet.singleton caller) + + let printXml f = function + | `Lifted1 x -> G.printXml f x + | `Lifted2 x -> BatPrintf.fprintf f "%a" CallerSet.printXml x + | x -> BatPrintf.fprintf f "%a" printXml x + + end + + let name () = "RecursionTermLifter (" ^ S.name () ^ ")" + + let conv (ctx: (_, G.t, _, V.t) ctx): (_, S.G.t, _, S.V.t) ctx = + { ctx with + global = (fun v -> G.spec (ctx.global (V.spec v))); + sideg = (fun v g -> ctx.sideg (V.spec v) (G.create_spec g)); + } + + let cycleDetection ctx call = + let module LH = Hashtbl.Make (Printable.Prod (CilType.Fundec) (S.C)) in + let module LS = Set.Make (Printable.Prod (CilType.Fundec) (S.C)) in + (* find all cycles/SCCs *) + let global_visited_calls = LH.create 100 in + + (* DFS *) + let rec iter_call (path_visited_calls: LS.t) ((fundec, _) as call) = + if LS.mem call path_visited_calls then ( + AnalysisState.svcomp_may_not_terminate := true; (*set the indicator for a non-terminating program for the sv comp*) + (*Cycle found*) + let loc = M.Location.CilLocation fundec.svar.vdecl in + M.warn ~loc ~category:Termination "The program might not terminate! (Fundec %a is contained in a call graph cycle)" CilType.Fundec.pretty fundec) (* output a warning for non-termination*) + else if not (LH.mem global_visited_calls call) then begin + LH.replace global_visited_calls call (); + let new_path_visited_calls = LS.add call path_visited_calls in + let gvar = V.call call in + let callers = G.callers (ctx.global gvar) in + CallerSet.iter (fun to_call -> + iter_call new_path_visited_calls to_call + ) callers; + end + in + iter_call LS.empty call + + let query ctx (type a) (q: a Queries.t): a Queries.result = + match q with + | WarnGlobal v -> + (* check result of loop analysis *) + if not (ctx.ask Queries.MustTermAllLoops) then + AnalysisState.svcomp_may_not_terminate := true; + let v: V.t = Obj.obj v in + begin match v with + | `Left v' -> + S.query (conv ctx) (WarnGlobal (Obj.repr v')) + | `Right call -> cycleDetection ctx call (* Note: to make it more efficient, one could only execute the cycle detection in case the loop analysis returns true, because otherwise the program will probably not terminate anyway*) + end + | InvariantGlobal v -> + let v: V.t = Obj.obj v in + begin match v with + | `Left v -> + S.query (conv ctx) (InvariantGlobal (Obj.repr v)) + | `Right v -> + Queries.Result.top q + end + | _ -> S.query (conv ctx) q + + let branch ctx = S.branch (conv ctx) + let assign ctx = S.assign (conv ctx) + let vdecl ctx = S.vdecl (conv ctx) + + + let record_call sideg callee caller = + sideg (V.call callee) (G.create_singleton_caller caller) + + let enter ctx = S.enter (conv ctx) + let paths_as_set ctx = S.paths_as_set (conv ctx) + let body ctx = S.body (conv ctx) + let return ctx = S.return (conv ctx) + let combine_env ctx r fe f args fc es f_ask = + if !AnalysisState.postsolving then ( + let c_r: S.C.t = ctx.context () in (* Caller context *) + let nodeF = ctx.node in + let fd_r : fundec = Node.find_fundec nodeF in (* Caller fundec *) + let caller: (fundec * S.C.t) = (fd_r, c_r) in + let c_e: S.C.t = Option.get fc in (* Callee context *) + let fd_e : fundec = f in (* Callee fundec *) + let callee = (fd_e, c_e) in + record_call ctx.sideg callee caller + ); + S.combine_env (conv ctx) r fe f args fc es f_ask + + let combine_assign ctx = S.combine_assign (conv ctx) + let special ctx = S.special (conv ctx) + let threadenter ctx = S.threadenter (conv ctx) + let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx) + let sync ctx = S.sync (conv ctx) + let skip ctx = S.skip (conv ctx) + let asm ctx = S.asm (conv ctx) + let event ctx e octx = S.event (conv ctx) e (conv octx) +end + module CompareGlobSys (SpecSys: SpecSys) = struct open SpecSys diff --git a/src/framework/control.ml b/src/framework/control.ml index 5c938cfd08..0c9b61739b 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -15,6 +15,7 @@ module type S2S = functor (X : Spec) -> Spec let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg" in + let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*) let open Batteries in (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in @@ -36,6 +37,7 @@ let spec_module: (module Spec) Lazy.t = lazy ( Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *) |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter) |> lift true (module LongjmpLifter) + |> lift termination_enabled (module RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*) ) in GobConfig.building_spec := false; ControlSpecC.control_spec_c := (module S1.C); @@ -103,6 +105,8 @@ struct let module StringMap = BatMap.Make (String) in let live_lines = ref StringMap.empty in let dead_lines = ref StringMap.empty in + let module FunSet = Hashtbl.Make (CilType.Fundec) in + let live_funs: unit FunSet.t = FunSet.create 13 in let add_one n v = match n with | Statement s when Cilfacade.(StmtH.mem pseudo_return_to_fun s) -> @@ -113,6 +117,7 @@ struct See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) let l = UpdateCil.getLoc n in let f = Node.find_fundec n in + FunSet.replace live_funs f (); let add_fun = BatISet.add l.line in let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in @@ -134,6 +139,21 @@ struct try StringMap.find fn (StringMap.find file !live_lines) with Not_found -> BatISet.empty in + if List.mem "termination" @@ get_string_list "ana.activated" then ( + (* check if we have upjumping gotos *) + let open Cilfacade in + let warn_for_upjumps fundec gotos = + if FunSet.mem live_funs fundec then ( + (* set nortermiantion flag *) + AnalysisState.svcomp_may_not_terminate := true; + (* iterate through locations to produce warnings *) + LocSet.iter (fun l _ -> + M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)" + ) gotos + ) + in + FunLocH.iter warn_for_upjumps funs_with_upjumping_gotos + ); dead_lines := StringMap.mapi (fun fi -> StringMap.mapi (fun fu ded -> BatISet.diff ded (live fi fu))) !dead_lines; dead_lines := StringMap.map (StringMap.filter (fun _ x -> not (BatISet.is_empty x))) !dead_lines; dead_lines := StringMap.filter (fun _ x -> not (StringMap.is_empty x)) !dead_lines; diff --git a/src/goblint.ml b/src/goblint.ml index 4ea3a3d242..6c5a2df33d 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -38,6 +38,8 @@ let main () = print_endline (GobUnix.localtime ()); print_endline GobSys.command_line; ); + (* When analyzing a termination specification, activate the termination analysis before pre-processing. *) + if get_bool "ana.autotune.enabled" && AutoTune.specificationIsActivated () then AutoTune.focusOnSpecification (); let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in if get_bool "server.enabled" then ( let file = diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index a71a0c9684..cb18ad0dd7 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -148,8 +148,8 @@ module UnitAnalysis = UnitAnalysis module Assert = Assert module FileUse = FileUse +module LoopTermination = LoopTermination module Uninit = Uninit -module Termination = Termination module Expsplit = Expsplit module StackTrace = StackTrace module Spec = Spec @@ -339,6 +339,7 @@ module Tracing = Tracing module Preprocessor = Preprocessor module CompilationDatabase = CompilationDatabase module MakefileUtil = MakefileUtil +module TerminationPreprocessing = TerminationPreprocessing (** {2 Witnesses} diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 1512e63b47..82a19aa4ae 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -161,6 +161,12 @@ let check_arguments () = ); if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint"; if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'"; + if List.mem "termination" @@ get_string_list "ana.activated" then ( + if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then fail "termination analysis is not compatible with incremental analysis"; + set_list "ana.activated" (GobConfig.get_list "ana.activated" @ [`String ("threadflag")]); + set_string "sem.int.signed_overflow" "assume_none"; + warn "termination analysis implicitly activates threadflag analysis and set sem.int.signed_overflow to assume_none"; + ); if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)" (** Initialize some globals in other modules. *) @@ -487,7 +493,7 @@ let merge_parsed parsed = Cilfacade.current_file := merged_AST; (* Set before createCFG, so Cilfacade maps can be computed for loop unrolling. *) CilCfg.createCFG merged_AST; (* Create CIL CFG from CIL AST. *) - Cilfacade.reset_lazy (); (* Reset Cilfacade maps, which need to be recomputer after loop unrolling. *) + Cilfacade.reset_lazy ~keepupjumpinggotos:true (); (* Reset Cilfacade maps, which need to be recomputer after loop unrolling but keep gotos. *) merged_AST let preprocess_parse_merge () = diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index 2c8ec646c3..923cf7600b 100644 --- a/src/util/cilCfg.ml +++ b/src/util/cilCfg.ml @@ -42,6 +42,7 @@ let loopCount file = let createCFG (fileAST: file) = + Cilfacade.do_preprocess fileAST; (* The analyzer keeps values only for blocks. So if you want a value for every program point, each instruction *) (* needs to be in its own block. end_basic_blocks does that. *) (* After adding support for VLAs, there are new VarDecl instructions at the point where a variable was declared and *) @@ -49,6 +50,7 @@ let createCFG (fileAST: file) = (* BB causes the output CIL file to no longer compile. *) (* Since we want the output of justcil to compile, we do not run allBB visitor if justcil is enable, regardless of *) (* exp.basic-blocks. This does not matter, as we will not run any analysis anyway, when justcil is enabled. *) + (* the preprocessing must be done here, to add the changes of CIL to the CFG*) if not (get_bool "exp.basic-blocks") && not (get_bool "justcil") then end_basic_blocks fileAST; (* We used to renumber vids but CIL already generates them fresh, so no need. @@ -66,6 +68,4 @@ let createCFG (fileAST: file) = computeCFGInfo fd true | _ -> () ); - if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST); - - Cilfacade.do_preprocess fileAST + if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST); \ No newline at end of file diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 4ce8fc06b4..e1a8ad542b 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -320,6 +320,7 @@ class loopUnrollingCallVisitor = object | Unlock _ | ThreadCreate _ | Assert _ + | Bounded _ | ThreadJoin _ -> raise Found; | _ -> diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml new file mode 100644 index 0000000000..9023a68f8a --- /dev/null +++ b/src/util/terminationPreprocessing.ml @@ -0,0 +1,76 @@ +open GoblintCil +(* module Z = Big_int_Z *) + +module VarToStmt = Map.Make(CilType.Varinfo) (* maps varinfos (= loop counter variable) to the statement of the corresponding loop*) + +let counter_ikind = IULongLong +let counter_typ = TInt (counter_ikind, []) +let min_int_exp = + (* Currently only tested for IInt type, which is signed *) + if Cil.isSigned counter_ikind then + Const(CInt(Z.shift_left Cilint.mone_cilint ((bytesSizeOfInt counter_ikind)*8-1), IInt, None)) + else + Const(CInt(Z.zero, counter_ikind, None)) + +class loopCounterVisitor lc (fd : fundec) = object(self) + inherit nopCilVisitor + + (* Counter of variables inserted for termination *) + val mutable vcounter = ref 0 + + method! vfunc _ = + vcounter := 0; + DoChildren + + method! vstmt s = + + let specialFunction name = + { svar = makeGlobalVar name (TFun(voidType, Some [("exp", counter_typ, [])], false,[])); + smaxid = 0; + slocals = []; + sformals = []; + sbody = mkBlock []; + smaxstmtid = None; + sallstmts = []; + } in + + let f_bounded = Lval (var (specialFunction "__goblint_bounded").svar) in + + (* Yields increment expression e + 1 where the added "1" that has the same type as the expression [e]. + Using Cil.increm instead does not work for non-[IInt] ikinds. *) + let increment_expression e = + let et = typeOf e in + let bop = PlusA in + let one = Const (CInt (Cilint.one_cilint, counter_ikind, None)) in + constFold false (BinOp(bop, e, one, et)) in + + let action s = match s.skind with + | Loop (b, loc, eloc, _, _) -> + 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 + 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; + s + | Goto (sref, l) -> + let goto_jmp_stmt = sref.contents.skind in + let loc_stmt = Cil.get_stmtLoc goto_jmp_stmt in + if CilType.Location.compare l loc_stmt >= 0 then ( + (* is pos if first loc is greater -> below the second loc *) + (* problem: the program might not terminate! *) + let open Cilfacade in + let current = FunLocH.find_opt funs_with_upjumping_gotos fd in + let current = BatOption.default (LocSet.create 13) current in + LocSet.replace current l (); + FunLocH.replace funs_with_upjumping_gotos fd current; + ); + s + | _ -> s + in ChangeDoChildrenPost (s, action); +end diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 89487ea8d4..6d22a51166 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -17,7 +17,6 @@ let task: (module Task) option ref = ref None let is_error_function' f spec = - let module Task = (val (Option.get !task)) in List.exists (function | Specification.UnreachCall f_spec -> f.vname = f_spec | _ -> false @@ -53,6 +52,7 @@ struct | UnreachCall _ -> "unreach-call" | NoOverflow -> "no-overflow" | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *) + | Termination -> "termination" | ValidFree -> "valid-free" | ValidDeref -> "valid-deref" | ValidMemtrack -> "valid-memtrack" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 66b3b83ac8..c7601ef637 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -6,6 +6,7 @@ type t = | UnreachCall of string | NoDataRace | NoOverflow + | Termination | ValidFree | ValidDeref | ValidMemtrack @@ -17,6 +18,7 @@ let of_string s = let s = String.strip s in let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in + let regexp_finally = Str.regexp "CHECK( init(main()), LTL(F \\(.*\\)) )" in if Str.string_match regexp_negated s 0 then let global_not = Str.matched_group 1 s in if global_not = "data-race" then @@ -42,6 +44,12 @@ let of_string s = ValidMemcleanup else failwith "Svcomp.Specification.of_string: unknown global expression" + else if Str.string_match regexp_finally s 0 then + let finally = Str.matched_group 1 s in + if finally = "end" then + Termination + else + failwith "Svcomp.Specification.of_string: unknown finally expression" else failwith "Svcomp.Specification.of_string: unknown expression" @@ -66,22 +74,32 @@ let of_option () = of_string s let to_string spec = - let print_output spec_str is_neg = + let module Prop = struct + type prop = F | G + let string_of_prop = function + | F -> "F" + | G -> "G" + end + in + let open Prop in + let print_output prop spec_str is_neg = + let prop = string_of_prop prop in if is_neg then - Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str + Printf.sprintf "CHECK( init(main()), LTL(%s ! %s) )" prop spec_str else - Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str + Printf.sprintf "CHECK( init(main()), LTL(%s %s) )" prop spec_str in - let spec_str, is_neg = match spec with - | UnreachCall f -> "call(" ^ f ^ "())", true - | NoDataRace -> "data-race", true - | NoOverflow -> "overflow", true - | ValidFree -> "valid-free", false - | ValidDeref -> "valid-deref", false - | ValidMemtrack -> "valid-memtrack", false - | ValidMemcleanup -> "valid-memcleanup", false + let prop, spec_str, is_neg = match spec with + | UnreachCall f -> G, "call(" ^ f ^ "())", true + | NoDataRace -> G, "data-race", true + | NoOverflow -> G, "overflow", true + | ValidFree -> G, "valid-free", false + | ValidDeref -> G, "valid-deref", false + | ValidMemtrack -> G, "valid-memtrack", false + | ValidMemcleanup -> G, "valid-memcleanup", false + | Termination -> F, "end", false in - print_output spec_str is_neg + print_output prop spec_str is_neg let to_string spec = String.concat "\n" (List.map to_string spec) diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 235461c348..52b1131821 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -475,6 +475,36 @@ struct in (module TaskResult:WitnessTaskResult) ) + | Termination -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_not_terminate then + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.True + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + else ( + let module TaskResult = + struct + module Arg = TrivialArg + let result = Result.Unknown + let invariant _ = Invariant.none + let is_violation _ = false + let is_sink _ = false + end + in + (module TaskResult:WitnessTaskResult) + ) | NoOverflow -> let module TrivialArg = struct diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 9e8ebeff51..f8532a1551 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -25,7 +25,7 @@ struct let uuid = Uuidm.v4_gen uuid_random_state () in let creation_time = TimeUtil.iso8601_now () in { - format_version = "0.1"; + format_version = GobConfig.get_string "witness.yaml.format-version"; uuid = Uuidm.to_string uuid; creation_time; producer; @@ -91,6 +91,29 @@ struct metadata = metadata ~task (); } + let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = { + invariant_type = LocationInvariant { + location; + value = invariant; + format = "c_expression"; + }; + } + + let loop_invariant' ~location ~(invariant): InvariantSet.Invariant.t = { + invariant_type = LoopInvariant { + location; + value = invariant; + format = "c_expression"; + }; + } + + let invariant_set ~task ~(invariants): Entry.t = { + entry_type = InvariantSet { + content = invariants; + }; + metadata = metadata ~task (); + } + let target ~uuid ~type_ ~(file_name): Target.t = { uuid; type_; @@ -120,12 +143,12 @@ struct } end -let yaml_entries_to_file yaml_entries file = +let yaml_entries_to_file ?(invariants=0) yaml_entries file = let yaml = `A yaml_entries in (* Yaml_unix.to_file_exn file yaml *) (* to_file/to_string uses a fixed-size buffer... *) (* estimate how big it should be + extra in case empty *) - let text = match Yaml.to_string ~len:(List.length yaml_entries * 4096 + 2048) yaml with + let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 4096 + 2048) yaml with | Ok text -> text | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) in @@ -134,6 +157,9 @@ let yaml_entries_to_file yaml_entries file = let entry_type_enabled entry_type = List.mem entry_type (GobConfig.get_string_list "witness.yaml.entry-types") +let invariant_type_enabled invariant_type = + List.mem invariant_type (GobConfig.get_string_list "witness.yaml.invariant-types") + module Make (R: ResultQuery.SpecSysSol2) = struct open R @@ -385,13 +411,81 @@ struct entries in + (* Generate invariant set *) + let (entries, invariants) = + if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then ( + let invariants = [] in + + (* Generate location invariants *) + let invariants = + if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( + NH.fold (fun n local acc -> + let loc = Node.location n in + if is_invariant_node n then ( + let lvals = local_lvals n local in + match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Node.find_fundec n).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.location_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else + acc + ) (Lazy.force nh) invariants + ) + else + invariants + in + + (* Generate loop invariants *) + let invariants = + if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( + NH.fold (fun n local acc -> + let loc = Node.location n in + if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( + match R.ask_local_node n ~local (Invariant Invariant.default_context) with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Node.find_fundec n).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.loop_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else + acc + ) (Lazy.force nh) invariants + ) + else + invariants + in + + let invariants = List.rev invariants in + let entry = Entry.invariant_set ~task ~invariants in + (entry :: entries, List.length invariants) + ) + else + (entries, 0) + in + let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *) M.msg_group Info ~category:Witness "witness generation summary" [ (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None); ]; - yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) + yaml_entries_to_file ~invariants yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) let write () = Timing.wrap "yaml witness" write () @@ -639,6 +733,48 @@ struct None in + let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = + + let validate_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = + let loc = loc_of_location location_invariant.location in + let inv = location_invariant.value in + + match Locator.find_opt locator loc with + | Some lvars -> + ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv) + | None -> + incr cnt_error; + M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv; + in + + let validate_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) = + let loc = loc_of_location loop_invariant.location in + let inv = loop_invariant.value in + + match Locator.find_opt loop_locator loc with + | Some lvars -> + ignore (validate_lvars_invariant ~entry_certificate:None ~loc ~lvars inv) + | None -> + incr cnt_error; + M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv; + in + + let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) = + let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in + match invariant_type_enabled target_type, invariant.invariant_type with + | true, LocationInvariant x -> + validate_location_invariant x + | true, LoopInvariant x -> + validate_loop_invariant x + | false, (LocationInvariant _ | LoopInvariant _) -> + incr cnt_disabled; + M.info_noloc ~category:Witness "disabled invariant of type %s" target_type; + in + + List.iter validate_invariant invariant_set.content; + None + in + match entry_type_enabled target_type, entry.entry_type with | true, LocationInvariant x -> validate_location_invariant x @@ -646,7 +782,9 @@ struct validate_loop_invariant x | true, PreconditionLoopInvariant x -> validate_precondition_loop_invariant x - | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _) -> + | true, InvariantSet x -> + validate_invariant_set x + | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> incr cnt_disabled; M.info_noloc ~category:Witness "disabled entry of type %s" target_type; None diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 3390c1e3ab..f9bcf3235f 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -242,6 +242,100 @@ struct {location; loop_invariant; precondition} end +module InvariantSet = +struct + module LoopInvariant = + struct + type t = { + location: Location.t; + value: string; + format: string; + } + + let invariant_type = "loop_invariant" + + let to_yaml' {location; value; format} = + [ + ("location", Location.to_yaml location); + ("value", `String value); + ("format", `String format); + ] + + let of_yaml y = + let open GobYaml in + let+ location = y |> find "location" >>= Location.of_yaml + and+ value = y |> find "value" >>= to_string + and+ format = y |> find "format" >>= to_string in + {location; value; format} + end + + module LocationInvariant = + struct + include LoopInvariant + + let invariant_type = "location_invariant" + end + + (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *) + module InvariantType = + struct + type t = + | LocationInvariant of LocationInvariant.t + | LoopInvariant of LoopInvariant.t + + let invariant_type = function + | LocationInvariant _ -> LocationInvariant.invariant_type + | LoopInvariant _ -> LoopInvariant.invariant_type + + let to_yaml' = function + | LocationInvariant x -> LocationInvariant.to_yaml' x + | LoopInvariant x -> LoopInvariant.to_yaml' x + + let of_yaml y = + let open GobYaml in + let* invariant_type = y |> find "type" >>= to_string in + if invariant_type = LocationInvariant.invariant_type then + let+ x = y |> LocationInvariant.of_yaml in + LocationInvariant x + else if invariant_type = LoopInvariant.invariant_type then + let+ x = y |> LoopInvariant.of_yaml in + LoopInvariant x + else + Error (`Msg "type") + end + + module Invariant = + struct + type t = { + invariant_type: InvariantType.t; + } + + let to_yaml {invariant_type} = + `O ([ + ("type", `String (InvariantType.invariant_type invariant_type)); + ] @ InvariantType.to_yaml' invariant_type) + + let of_yaml y = + let open GobYaml in + let+ invariant_type = y |> InvariantType.of_yaml in + {invariant_type} + end + + type t = { + content: Invariant.t list; + } + + let entry_type = "invariant_set" + + let to_yaml' {content} = + [("content", `A (List.map Invariant.to_yaml content))] + + let of_yaml y = + let open GobYaml in + let+ content = y |> find "content" >>= list >>= list_map Invariant.of_yaml in + {content} +end + module Target = struct type t = { @@ -326,6 +420,7 @@ struct | PreconditionLoopInvariant of PreconditionLoopInvariant.t | LoopInvariantCertificate of LoopInvariantCertificate.t | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t + | InvariantSet of InvariantSet.t let entry_type = function | LocationInvariant _ -> LocationInvariant.entry_type @@ -334,6 +429,7 @@ struct | PreconditionLoopInvariant _ -> PreconditionLoopInvariant.entry_type | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type + | InvariantSet _ -> InvariantSet.entry_type let to_yaml' = function | LocationInvariant x -> LocationInvariant.to_yaml' x @@ -342,6 +438,7 @@ struct | PreconditionLoopInvariant x -> PreconditionLoopInvariant.to_yaml' x | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x + | InvariantSet x -> InvariantSet.to_yaml' x let of_yaml y = let open GobYaml in @@ -364,6 +461,9 @@ struct else if entry_type = PreconditionLoopInvariantCertificate.entry_type then let+ x = y |> PreconditionLoopInvariantCertificate.of_yaml in PreconditionLoopInvariantCertificate x + else if entry_type = InvariantSet.entry_type then + let+ x = y |> InvariantSet.of_yaml in + InvariantSet x else Error (`Msg "entry_type") end diff --git a/tests/regression/09-regions/38-escape_malloc.c b/tests/regression/09-regions/38-escape_malloc.c index 9f5b44531e..c849d5bbe3 100644 --- a/tests/regression/09-regions/38-escape_malloc.c +++ b/tests/regression/09-regions/38-escape_malloc.c @@ -9,7 +9,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; void *t_fun(void *arg) { int *p = (int *) arg; pthread_mutex_lock(&mutex1); - (*p)++; // TODO RACE! + (*p)++; // RACE! pthread_mutex_unlock(&mutex1); return NULL; } @@ -20,7 +20,7 @@ int main(void) { // TODO: q escapes as region owner pthread_create(&id, NULL, t_fun, (void *) q); pthread_mutex_lock(&mutex2); - (*q)++; // TODO RACE! + (*q)++; // RACE! pthread_mutex_unlock(&mutex2); pthread_join (id, NULL); return 0; diff --git a/tests/regression/09-regions/41-per-thread-array-init-race.c b/tests/regression/09-regions/41-per-thread-array-init-race.c new file mode 100644 index 0000000000..f6d267495e --- /dev/null +++ b/tests/regression/09-regions/41-per-thread-array-init-race.c @@ -0,0 +1,40 @@ +// PARAM: --set ana.activated[+] region --enable ana.sv-comp.functions +// Per-thread array pointers passed via argument but initialized before thread create. +// Extracted from silver searcher. +#include +#include +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} +extern int __VERIFIER_nondet_int(); + +void *thread(void *arg) { + int *p = arg; + int i = *p; // RACE! + return NULL; +} + +int main() { + int threads_total = __VERIFIER_nondet_int(); + assume_abort_if_not(threads_total >= 0); + + pthread_t *tids = malloc(threads_total * sizeof(pthread_t)); + int *is = calloc(threads_total, sizeof(int)); + + // create threads + for (int i = 0; i < threads_total; i++) { + pthread_create(&tids[i], NULL, &thread, &is[i]); // may fail but doesn't matter + is[i] = i; // RACE! + } + + // join threads + for (int i = 0; i < threads_total; i++) { + pthread_join(tids[i], NULL); + } + + free(tids); + free(is); + + return 0; +} diff --git a/tests/regression/78-termination/01-simple-loop-terminating.c b/tests/regression/78-termination/01-simple-loop-terminating.c new file mode 100644 index 0000000000..8ca4610057 --- /dev/null +++ b/tests/regression/78-termination/01-simple-loop-terminating.c @@ -0,0 +1,15 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 1; + + while (i <= 10) + { + printf("%d\n", i); + i++; + } + + return 0; +} diff --git a/tests/regression/78-termination/02-simple-loop-nonterminating.c b/tests/regression/78-termination/02-simple-loop-nonterminating.c new file mode 100644 index 0000000000..d8847e2b74 --- /dev/null +++ b/tests/regression/78-termination/02-simple-loop-nonterminating.c @@ -0,0 +1,12 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + while (1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + continue; + } + + return 0; +} diff --git a/tests/regression/78-termination/03-nested-loop-terminating.c b/tests/regression/78-termination/03-nested-loop-terminating.c new file mode 100644 index 0000000000..6b31204567 --- /dev/null +++ b/tests/regression/78-termination/03-nested-loop-terminating.c @@ -0,0 +1,27 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int rows = 3; + int columns = 4; + int i = 1; + + // Outer while loop for rows + while (i <= rows) + { + int j = 1; + + // Inner while loop for columns + while (j <= columns) + { + printf("(%d, %d) ", i, j); + j++; + } + + printf("\n"); + i++; + } + + return 0; +} diff --git a/tests/regression/78-termination/04-nested-loop-nonterminating.c b/tests/regression/78-termination/04-nested-loop-nonterminating.c new file mode 100644 index 0000000000..21b6014509 --- /dev/null +++ b/tests/regression/78-termination/04-nested-loop-nonterminating.c @@ -0,0 +1,23 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int outerCount = 1; + + while (outerCount <= 3) + { + int innerCount = 1; + + while (1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + printf("(%d, %d) ", outerCount, innerCount); + innerCount++; + } + + printf("\n"); + outerCount++; + } + + return 0; +} diff --git a/tests/regression/78-termination/05-for-loop-terminating.c b/tests/regression/78-termination/05-for-loop-terminating.c new file mode 100644 index 0000000000..7a2b789496 --- /dev/null +++ b/tests/regression/78-termination/05-for-loop-terminating.c @@ -0,0 +1,14 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i; + + for (i = 1; i <= 10; i++) + { + printf("%d\n", i); + } + + return 0; +} diff --git a/tests/regression/78-termination/06-for-loop-nonterminating.c b/tests/regression/78-termination/06-for-loop-nonterminating.c new file mode 100644 index 0000000000..6c6123251c --- /dev/null +++ b/tests/regression/78-termination/06-for-loop-nonterminating.c @@ -0,0 +1,12 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + for (;;) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop + { + printf("This loop does not terminate.\n"); + } + + return 0; +} diff --git a/tests/regression/78-termination/07-nested-for-loop-terminating.c b/tests/regression/78-termination/07-nested-for-loop-terminating.c new file mode 100644 index 0000000000..3293a1fa2c --- /dev/null +++ b/tests/regression/78-termination/07-nested-for-loop-terminating.c @@ -0,0 +1,20 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int rows = 3; + int columns = 4; + + // Nested loop to iterate over rows and columns + for (int i = 1; i <= rows; i++) + { + for (int j = 1; j <= columns; j++) + { + printf("(%d, %d) ", i, j); + } + printf("\n"); + } + + return 0; +} diff --git a/tests/regression/78-termination/08-nested-for-loop-nonterminating.c b/tests/regression/78-termination/08-nested-for-loop-nonterminating.c new file mode 100644 index 0000000000..cb65a0d267 --- /dev/null +++ b/tests/regression/78-termination/08-nested-for-loop-nonterminating.c @@ -0,0 +1,19 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int outerCount, innerCount; + + for (outerCount = 1; outerCount <= 3; outerCount++) + { + for (innerCount = 1;; innerCount++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop + { + printf("(%d, %d) ", outerCount, innerCount); + } + + printf("\n"); + } + + return 0; +} diff --git a/tests/regression/78-termination/09-complex-for-loop-terminating.c b/tests/regression/78-termination/09-complex-for-loop-terminating.c new file mode 100644 index 0000000000..74ee41eae8 --- /dev/null +++ b/tests/regression/78-termination/09-complex-for-loop-terminating.c @@ -0,0 +1,98 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none +// Apron is not precise enough for some nested loops +#include + +int loops0(){ + int i, j, k; + + // Outer loop + for (i = 1; i <= 5; i++) + { + // Inner loop 1 + for (j = 1; j <= i; j++) + { + printf("%d ", j); + } + printf("\n"); + + // Inner loop 2 + for (k = i; k >= 1; k--) + { + printf("%d ", k); + } + printf("\n"); + } + + // Additional loop + for (i = 5; i >= 1; i--) + { + for (j = i; j >= 1; j--) + { + printf("%d ", j); + } + printf("\n"); + } + return 0; +} + +int loops1(){ + int i, j, k; + + // Loop with conditions + for (i = 1; i <= 10; i++) + { + if (i % 2 == 0) + { + printf("%d is even\n", i); + } + else + { + printf("%d is odd\n", i); + } + } + + // Loop with nested conditions + for (i = 1; i <= 10; i++) + { + printf("Number: %d - ", i); + if (i < 5) + { + printf("Less than 5\n"); + } + else if (i > 5) + { + printf("Greater than 5\n"); + } + else + { + printf("Equal to 5\n"); + } + } + + // Loop with a break statement + for (i = 1; i <= 10; i++) + { + printf("%d ", i); + if (i == 5) + { + break; + } + } + printf("\n"); + + // Loop with multiple variables + int a, b, c; + for (a = 1, b = 2, c = 3; a <= 10; a++, b += 2, c += 3) + { + printf("%d %d %d\n", a, b, c); + } + return 0; +} + +int main() +{ + loops0(); + loops1(); + + return 0; +} diff --git a/tests/regression/78-termination/10-complex-loop-terminating.c b/tests/regression/78-termination/10-complex-loop-terminating.c new file mode 100644 index 0000000000..96253c445f --- /dev/null +++ b/tests/regression/78-termination/10-complex-loop-terminating.c @@ -0,0 +1,218 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none +// Apron is not precise enough for some nested loops +#include + +int loops0(){ + int i = 1; + int j = 1; + int k = 5; + + // Outer while loop + while (i <= 5) + { + // Inner while loop 1 + while (j <= i) + { + printf("%d ", j); + j++; + } + printf("\n"); + j = 1; + + // Inner while loop 2 + while (k >= 1) + { + printf("%d ", k); + k--; + } + printf("\n"); + k = 5; + + i++; + } + + // Additional while loop + i = 5; + while (i >= 1) + { + j = i; + while (j >= 1) + { + printf("%d ", j); + j--; + } + printf("\n"); + i--; + } + + // Loop with conditions + i = 1; + while (i <= 10) + { + if (i % 2 == 0) + { + printf("%d is even\n", i); + } + else + { + printf("%d is odd\n", i); + } + i++; + } + + // Loop with nested conditions + i = 1; + while (i <= 10) + { + printf("Number: %d - ", i); + if (i < 5) + { + printf("Less than 5\n"); + } + else if (i > 5) + { + printf("Greater than 5\n"); + } + else + { + printf("Equal to 5\n"); + } + i++; + } + return 0; +} + +int loops1() +{ + int i = 1; + int j = 1; + int k = 5; + + // Outer while loop + while (i <= 5) + { + // Inner while loop 1 + while (j <= i) + { + printf("%d ", j); + j++; + } + printf("\n"); + j = 1; + + // Inner while loop 2 + while (k >= 1) + { + printf("%d ", k); + k--; + } + printf("\n"); + k = 5; + + i++; + } + + // Additional while loop + i = 5; + while (i >= 1) + { + j = i; + while (j >= 1) + { + printf("%d ", j); + j--; + } + printf("\n"); + i--; + } + + // Loop with conditions + i = 1; + while (i <= 10) + { + if (i % 2 == 0) + { + printf("%d is even\n", i); + } + else + { + printf("%d is odd\n", i); + } + i++; + } + + return 0; +} + +int loops2(){ + int i = 1; + int j = 1; + int k = 5; + + // Loop with nested conditions + i = 1; + while (i <= 10) + { + printf("Number: %d - ", i); + if (i < 5) + { + printf("Less than 5\n"); + } + else if (i > 5) + { + printf("Greater than 5\n"); + } + else + { + printf("Equal to 5\n"); + } + i++; + } + + // Loop with a break statement + i = 1; + while (i <= 10) + { + printf("%d ", i); + if (i == 5) + { + break; + } + i++; + } + printf("\n"); + + // Loop with a continue statement + i = 1; + while (i <= 10) + { + if (i % 2 == 0) + { + i++; + continue; + } + printf("%d ", i); + i++; + } + printf("\n"); + + // Loop with multiple variables + int a = 1; + int b = 2; + int c = 3; + while (a <= 10) + { + printf("%d %d %d\n", a, b, c); + a++; + b += 2; + c += 3; + } + return 0; +} + +int main(){ + loops0(); + loops1(); + loops2(); + return 0; +} \ No newline at end of file diff --git a/tests/regression/78-termination/11-loopless-termination.c b/tests/regression/78-termination/11-loopless-termination.c new file mode 100644 index 0000000000..9f1a7e0f13 --- /dev/null +++ b/tests/regression/78-termination/11-loopless-termination.c @@ -0,0 +1,8 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + printf("Terminating code without a loop\n"); + return 0; +} diff --git a/tests/regression/78-termination/12-do-while-instant-terminating.c b/tests/regression/78-termination/12-do-while-instant-terminating.c new file mode 100644 index 0000000000..5bc18902b3 --- /dev/null +++ b/tests/regression/78-termination/12-do-while-instant-terminating.c @@ -0,0 +1,15 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 0; + + do + { + printf("Inside the do-while loop\n"); + } while (i > 0); + + printf("Exited the loop\n"); + return 0; +} diff --git a/tests/regression/78-termination/13-do-while-terminating.c b/tests/regression/78-termination/13-do-while-terminating.c new file mode 100644 index 0000000000..6ac6946495 --- /dev/null +++ b/tests/regression/78-termination/13-do-while-terminating.c @@ -0,0 +1,16 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 1; + + do + { + printf("Inside the do-while loop\n"); + i++; + } while (i <= 5); + + printf("Exited the loop\n"); + return 0; +} diff --git a/tests/regression/78-termination/14-do-while-nonterminating.c b/tests/regression/78-termination/14-do-while-nonterminating.c new file mode 100644 index 0000000000..0a9df3421f --- /dev/null +++ b/tests/regression/78-termination/14-do-while-nonterminating.c @@ -0,0 +1,16 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 1; + + do + { + printf("Inside the do-while loop\n"); + i++; + } while (i >= 2); // NONTERMLOOP termination analysis shall mark while as non-terminating loop + + printf("Exited the loop\n"); + return 0; +} diff --git a/tests/regression/78-termination/15-complex-loop-combination-terminating.c b/tests/regression/78-termination/15-complex-loop-combination-terminating.c new file mode 100644 index 0000000000..4912bbb1f2 --- /dev/null +++ b/tests/regression/78-termination/15-complex-loop-combination-terminating.c @@ -0,0 +1,126 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none +// Apron is not precise enough for some nested loops +#include + +int non_nested_loops(){ + // Non-nested loops + int i; + + // for loop + for (i = 1; i <= 10; i++) + { + printf("For loop iteration: %d\n", i); + } + + // while loop + int j = 1; + while (j <= 10) + { + printf("While loop iteration: %d\n", j); + j++; + } + + // do-while loop + int k = 1; + do + { + printf("Do-While loop iteration: %d\n", k); + k++; + } while (k <= 10); + return 0; +} + +int nested_loops(){ + // Nested loops + int a, b; + + // Nested for and while loop + for (a = 1; a <= 5; a++) + { + int c = 1; + while (c <= a) + { + printf("Nested For-While loop: %d\n", c); + c++; + } + } + + // Nested while and do-while loop + int x = 1; + while (x <= 5) + { + int y = 1; + do + { + printf("Nested While-Do-While loop: %d\n", y); + y++; + } while (y <= x); + x++; + } + + // Nested do-while and for loop + int p = 1; + do + { + for (int q = 1; q <= p; q++) + { + printf("Nested Do-While-For loop: %d\n", q); + } + p++; + } while (p <= 5); + return 0; +} + +int nested_while_loop_with_break(){ + int m; + + // Nested while loop with a break statement + int n = 1; + while (n <= 5) + { + printf("Outer While loop iteration: %d\n", n); + m = 1; + while (1) + { + printf("Inner While loop iteration: %d\n", m); + m++; + if (m == 4) + { + break; + } + } + n++; + } + return 0; +} + +int nested_loop_with_conditions(){ + // Loop with nested conditions + for (int v = 1; v <= 10; v++) + { + printf("Loop with Nested Conditions: %d - ", v); + if (v < 5) + { + printf("Less than 5\n"); + } + else if (v > 5) + { + printf("Greater than 5\n"); + } + else + { + printf("Equal to 5\n"); + } + } +} + +int main() +{ + non_nested_loops(); + nested_loops(); + // Additional nested loops + nested_while_loop_with_break(); + nested_loop_with_conditions(); + + return 0; +} diff --git a/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c b/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c new file mode 100644 index 0000000000..267a2d2fd8 --- /dev/null +++ b/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c @@ -0,0 +1,23 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int outerCount = 1; + + while (outerCount <= 3) + { + int innerCount = 1; + + while (outerCount < 3 || innerCount > 0) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + printf("(%d, %d) ", outerCount, innerCount); + innerCount++; + } + + printf("\n"); + outerCount++; + } + + return 0; +} diff --git a/tests/regression/78-termination/17-goto-terminating.c b/tests/regression/78-termination/17-goto-terminating.c new file mode 100644 index 0000000000..2f678d294b --- /dev/null +++ b/tests/regression/78-termination/17-goto-terminating.c @@ -0,0 +1,21 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +// The program terminates but the analysis is currently only meant to detect up-jumping gotos as potentially NonTerminating, therefore we expect an NonTerm +#include + +int main() +{ + int num = 1; + +loop: + printf("Current number: %d\n", num); + num++; + + if (num <= 10) + { + goto loop; // NONTERMGOTO termination analysis shall mark goto statement up-jumping goto + // We are not able to detect up-jumping gotos as terminating, we + // just warn about them might being nonterminating. + } + + return 0; +} diff --git a/tests/regression/78-termination/18-goto-nonterminating.c b/tests/regression/78-termination/18-goto-nonterminating.c new file mode 100644 index 0000000000..6de80effd7 --- /dev/null +++ b/tests/regression/78-termination/18-goto-nonterminating.c @@ -0,0 +1,15 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int num = 1; + +loop: + printf("Current number: %d\n", num); + num++; + + goto loop; // NONTERMGOTO termination analysis shall mark goto statement up-jumping goto + + return 0; +} diff --git a/tests/regression/78-termination/19-rand-terminating.c b/tests/regression/78-termination/19-rand-terminating.c new file mode 100644 index 0000000000..a5b6c22941 --- /dev/null +++ b/tests/regression/78-termination/19-rand-terminating.c @@ -0,0 +1,31 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include +#include +#include + +int main() +{ + // Seed the random number generator + srand(time(NULL)); + + if (rand()) + { + // Loop inside the if part + for (int i = 1; i <= 5; i++) + { + printf("Loop inside if part: %d\n", i); + } + } + else + { + // Loop inside the else part + int j = 1; + while (j <= 5) + { + printf("Loop inside else part: %d\n", j); + j++; + } + } + + return 0; +} diff --git a/tests/regression/78-termination/20-rand-nonterminating.c b/tests/regression/78-termination/20-rand-nonterminating.c new file mode 100644 index 0000000000..21b25ed9dd --- /dev/null +++ b/tests/regression/78-termination/20-rand-nonterminating.c @@ -0,0 +1,30 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include +#include +#include + +int main() +{ + // Seed the random number generator + srand(time(NULL)); + + if (rand()) + { + // Loop inside the if part + for (int i = 1; i >= 0; i++) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + printf("Loop inside if part: %d\n", i); + } + } + else + { + // Loop inside the else part + int j = 1; + while (j > 0) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + printf("Loop inside else part: %d\n", j); + } + } + + return 0; +} diff --git a/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c b/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c new file mode 100644 index 0000000000..5f82d91079 --- /dev/null +++ b/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c @@ -0,0 +1,20 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int forever, i = 0; + + // This loop is not provable, therefore it should throw a warning + while (i < 4 || forever == 1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + i++; + if (i == 4) + { + if (rand()) + { + forever = 1; + } + } + } +} \ No newline at end of file diff --git a/tests/regression/78-termination/22-exit-on-rand-unproofable.c b/tests/regression/78-termination/22-exit-on-rand-unproofable.c new file mode 100644 index 0000000000..33838ca83d --- /dev/null +++ b/tests/regression/78-termination/22-exit-on-rand-unproofable.c @@ -0,0 +1,16 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int forever = 1; + + // This loop is not provable, therefore it should throw a warning + while (forever == 1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + { + if (rand()) // May exit, may not + { + forever = 0; + } + } +} \ No newline at end of file diff --git a/tests/regression/78-termination/23-exit-on-rand-terminating.c b/tests/regression/78-termination/23-exit-on-rand-terminating.c new file mode 100644 index 0000000000..e65c064c40 --- /dev/null +++ b/tests/regression/78-termination/23-exit-on-rand-terminating.c @@ -0,0 +1,17 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include +#include + +int main() +{ + int short_run, i = 0; + // Currently not able to detect this as terminating due to multiple conditions + while (i < 90 && short_run != 1) + { + i++; + if (rand()) + { + short_run = 1; + } + } +} \ No newline at end of file diff --git a/tests/regression/78-termination/24-upjumping-goto-loopless-terminating.c b/tests/regression/78-termination/24-upjumping-goto-loopless-terminating.c new file mode 100644 index 0000000000..ce257d11ef --- /dev/null +++ b/tests/regression/78-termination/24-upjumping-goto-loopless-terminating.c @@ -0,0 +1,21 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +// The program terminates but the analysis is currently only meant to detect up-jumping gotos as potentially NonTerminating, therefore we expect an NonTerm +#include + +int main() +{ // Currently not able to detect up-jumping loop free gotos + goto mark2; + +mark1: + printf("This is mark1\n"); + goto mark3; + +mark2: + printf("This is mark2\n"); + goto mark1; // NONTERMGOTO termination analysis shall mark goto statement up-jumping goto + +mark3: + printf("This is mark3\n"); + + return 0; +} diff --git a/tests/regression/78-termination/25-leave-loop-goto-terminating.c b/tests/regression/78-termination/25-leave-loop-goto-terminating.c new file mode 100644 index 0000000000..b882759bff --- /dev/null +++ b/tests/regression/78-termination/25-leave-loop-goto-terminating.c @@ -0,0 +1,28 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int counter = 0; + + while (1) + { + counter++; + + // Dummy code + printf("Iteration %d\n", counter); + int result = counter * 2; + printf("Result: %d\n", result); + + // Condition to terminate the loop + if (result >= 10) + { // Apron is not able to detect this + goto end; + } + } + +end: + printf("Loop exited. Result is greater than or equal to 10.\n"); + + return 0; +} diff --git a/tests/regression/78-termination/26-enter-loop-goto-terminating.c b/tests/regression/78-termination/26-enter-loop-goto-terminating.c new file mode 100644 index 0000000000..aa85f22b3e --- /dev/null +++ b/tests/regression/78-termination/26-enter-loop-goto-terminating.c @@ -0,0 +1,31 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int counter = 0; + + goto jump_point; + + while (1) + { + counter++; + + // Dummy code + printf("Iteration %d\n", counter); + int result = counter * 2; + jump_point: + printf("Result: %d\n", result); + + // Condition to terminate the loop + if (result >= 10) + { // Apron is not able to detect this + goto end; + } + } + +end: + printf("Loop exited. Result is greater than or equal to 10.\n"); + + return 0; +} diff --git a/tests/regression/78-termination/27-upjumping-goto-nonterminating.c b/tests/regression/78-termination/27-upjumping-goto-nonterminating.c new file mode 100644 index 0000000000..e0eb633b11 --- /dev/null +++ b/tests/regression/78-termination/27-upjumping-goto-nonterminating.c @@ -0,0 +1,21 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + goto mark2; + +mark1: + printf("This is mark1\n"); + goto mark3; + +mark2: + printf("This is mark2\n"); + goto mark1; // NONTERMGOTO termination analysis shall mark goto statement up-jumping goto + +mark3: + printf("This is mark3\n"); + goto mark1; // NONTERMGOTO termination analysis shall mark goto statement up-jumping goto + + return 0; +} diff --git a/tests/regression/78-termination/28-do-while-continue-terminating.c b/tests/regression/78-termination/28-do-while-continue-terminating.c new file mode 100644 index 0000000000..a61174d295 --- /dev/null +++ b/tests/regression/78-termination/28-do-while-continue-terminating.c @@ -0,0 +1,99 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 1; + + do + { + i++; + printf("Inside the do-while loop\n"); + if (i % 2 == 0) + { + + printf("Skipping %i is even\n", i); + continue; // This is handled as an goto to line 8 and therefore an up-jumping goto + } + } while (i <= 5); + + printf("Exited the loop\n"); + return 0; +} + +/* +NOTE: +Test 28: does not terminate but should terminate (test case +"28-do-while-continue-terminating.c") Reason: upjumping goto + +If one has a look at the generated CIL output (attached at the bottom of this +file), one can see that the "continue" is translated in a "goto" with a +corresponding label "__Cont". This label points to the loop-exit condition. +Since the condition is part of the loop, its location is evaluated to 8-17. The +location of the goto "goto __Cont" is located in line 15. To provide soundness +for the analysis, the preprocessing detects upjumping gotos with the help of its +location. In case such a goto is detected, the program is classified as +non-terminating. Due to this inserted goto (which is a result of the +"continue"), an upjumping goto is located, which makes this program +non-terminating. + +It should be noted that this issue happens when "do while"-loops and "continues" +are combined. If one combines "while"-loops and "continues", the analysis can +still classify the loop as terminating. The reason for that can be seen in the +second CIL output, where the "do while"-loop is replaced by a "while"-loop. +Instead of creating a new label, the "while-continue" label of the loop is +reused. Also, this goto statement is not specified as a goto, but as a Continue +statement. Hence, it is not analyzed for the upjumping gotos, which does not +lead to the problem as with the "do while". + + +------- SHORTENED CIL output for Test 28 (DO WHILE): ------- +int main(void) +{{{{ + #line 8 + while (1) { + while_continue: ; + #line 12 + if (i % 2 == 0) { + #line 15 + goto __Cont; + } + __Cont: + #line 8 + if (! (i <= 5)) { + #line 8 + goto while_break; + } + } + + while_break: + }} + #line 20 + return (0); +}} + + +------- SHORTENED CIL output for Test 28 (WHILE): ------- +Test 28: replacing DO WHILE with WHILE: int main(void) +{{{{ + #line 8 + while (1) { + while_continue: ; + #line 8 + if (! (i <= 5)) { + #line 8 + goto while_break; + } + #line 12 + if (i % 2 == 0) { + #line 15 + goto while_continue; + } + } + while_break: ; + }} + #line 20 + return (0); +}} + +*/ diff --git a/tests/regression/78-termination/29-do-while-continue-nonterminating.c b/tests/regression/78-termination/29-do-while-continue-nonterminating.c new file mode 100644 index 0000000000..dd931c012f --- /dev/null +++ b/tests/regression/78-termination/29-do-while-continue-nonterminating.c @@ -0,0 +1,22 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i = 1; + + do + { + printf("Inside the do-while loop\n"); + i++; + + if (i % 2) + { + printf("Continue as %i is odd\n", i); + continue; + } + } while (i >= 2); // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop + + printf("Exited the loop\n"); + return 0; +} diff --git a/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c b/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c new file mode 100644 index 0000000000..c07b558d07 --- /dev/null +++ b/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c @@ -0,0 +1,36 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int rows = 5; + int columns = 5; + + // Outer loop for rows + for (int i = 1; i <= rows; i++) + { + // Inner loop for columns + for (int j = 1; j <= columns; j++) + { + if (j == 3) + { + goto outer_loop; // Jump to the label "outer_loop" + } + printf("(%d, %d) ", i, j); + } + printf("Not Skipped?\n"); + outer_loop:; // Label for the outer loop + printf("Skipped!\n"); + } + + return 0; +} + +/* +NOTE: In case we do NOT assume no-overflow: +Test 30: terminates (test case "30-goto-out-of-inner-loop-terminating.c") +Test 35: does not terminate (test case +"35-goto-out-of-inner-loop-with-print-terminating.c") + +The reason is explained in "35-goto-out-of-inner-loop-with-print-terminating.c" +*/ diff --git a/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c b/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c new file mode 100644 index 0000000000..f9b9275620 --- /dev/null +++ b/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c @@ -0,0 +1,27 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int rows = 5; + int columns = 5; + + // Outer loop for rows + for (int i = 1; 1; i++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop + { + // Inner loop for columns + for (int j = 1; j <= columns; j++) + { + if (j == 3) + { + printf("Goto as continue for outer loop\n"); + goto outer_loop; + } + printf("(%d, %d) ", i, j); + } + printf("\n"); + outer_loop:; // Label for the outer loop + } + + return 0; +} diff --git a/tests/regression/78-termination/32-multithread-terminating.c b/tests/regression/78-termination/32-multithread-terminating.c new file mode 100644 index 0000000000..eb8b796a47 --- /dev/null +++ b/tests/regression/78-termination/32-multithread-terminating.c @@ -0,0 +1,30 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +// The program terminates but as the termination analysis is meant to not handle multithreaded programs we expect NonTerm here +#include +#include +#include + +// Thread function +void *printPID(void *arg) +{ + pid_t pid = getpid(); + pthread_t tid = pthread_self(); + printf("Thread ID: %lu, Process ID: %d\n", (unsigned long)tid, pid); + return NULL; +} + +int main() +{ + // Create three threads + pthread_t thread1, thread2, thread3; + pthread_create(&thread1, NULL, printPID, NULL); + pthread_create(&thread2, NULL, printPID, NULL); + pthread_create(&thread3, NULL, printPID, NULL); + + // Wait for all threads to finish + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + pthread_join(thread3, NULL); + + return 0; +} diff --git a/tests/regression/78-termination/33-multithread-nonterminating.c b/tests/regression/78-termination/33-multithread-nonterminating.c new file mode 100644 index 0000000000..8a6274c7ab --- /dev/null +++ b/tests/regression/78-termination/33-multithread-nonterminating.c @@ -0,0 +1,40 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include +#include +#include +#include +#include + +// Thread function +void *printPID(void *arg) +{ + pid_t pid = getpid(); + pthread_t tid = pthread_self(); + while (1) + { + printf("Thread ID: %lu, Process ID: %d\n", (unsigned long)tid, pid); + struct timespec sleepTime; + sleepTime.tv_sec = 1; // Seconds + sleepTime.tv_nsec = + 100000000 + (rand() % 200000000); // Nanoseconds (0.1 seconds + rand) + printf("Sleep for %ld nsec\n", sleepTime.tv_nsec); + nanosleep(&sleepTime, NULL); + } + return NULL; +} + +int main() +{ + // Create three threads + pthread_t thread1, thread2, thread3; + pthread_create(&thread1, NULL, printPID, NULL); + pthread_create(&thread2, NULL, printPID, NULL); + pthread_create(&thread3, NULL, printPID, NULL); + + // Wait for all threads to finish + pthread_join(thread1, NULL); + pthread_join(thread2, NULL); + pthread_join(thread3, NULL); + + return 0; +} diff --git a/tests/regression/78-termination/34-nested-for-loop-nonterminating.c b/tests/regression/78-termination/34-nested-for-loop-nonterminating.c new file mode 100644 index 0000000000..2f21f9e996 --- /dev/null +++ b/tests/regression/78-termination/34-nested-for-loop-nonterminating.c @@ -0,0 +1,19 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int outerCount, innerCount; + + for (outerCount = 1; outerCount <= 3; outerCount++) + { + for (innerCount = 1; innerCount > 0; innerCount++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop + { + printf("(%d, %d) ", outerCount, innerCount); + } + + printf("\n"); + } + + return 0; +} diff --git a/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c b/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c new file mode 100644 index 0000000000..4c738e1173 --- /dev/null +++ b/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c @@ -0,0 +1,42 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set "ana.activated[+]" apron --enable ana.int.interval --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none +#include + +int main() +{ + int rows = 5; + int columns = 5; + + // Outer loop for rows + for (int i = 1; i <= rows; i++) + { + // Inner loop for columns + for (int j = 1; j <= columns; j++) + { + if (j == 3) + { + goto outer_loop; // Jump to the label "outer_loop" + } + printf("(%d, %d) ", i, j); + } + outer_loop: // Label for the outer loop + printf("\n"); + } + + return 0; +} + +/* +NOTE: In case we do NOT assume no-overflow: +Test 30: terminates (test case "30-goto-out-of-inner-loop-terminating.c") +Test 35: does not terminate (test case +"35-goto-out-of-inner-loop-with-print-terminating.c") + +The only difference between Test 30 and Test 35 is line 17. Test 30 has an +additional statement, and Test 35 continues already with the label. This +difference in Test 35 leads to an overflow in line 11, and hence to the +non-termination. This overflow is created by a WPoint Issue. By enabling the +no-overflow option this issue can be fixed and, both test cases are correctly +detected as terminating. + +(The overflow also happens without the termination analysis enabled.) +*/ diff --git a/tests/regression/78-termination/36-recursion-terminating.c b/tests/regression/78-termination/36-recursion-terminating.c new file mode 100644 index 0000000000..179efabeea --- /dev/null +++ b/tests/regression/78-termination/36-recursion-terminating.c @@ -0,0 +1,25 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void recursiveFunction(int n) +{ + // Base case: When n reaches 0, stop recursion + if (n == 0) + { + printf("Terminating recursion\n"); + return; + } + + printf("Recursive call with n = %d\n", n); + + // Recursive call: Decrement n and call the function again + recursiveFunction(n - 1); +} + +int main() +{ + // Call the recursive function with an initial value + recursiveFunction(5); + + return 0; +} diff --git a/tests/regression/78-termination/37-recursion-nonterminating.c b/tests/regression/78-termination/37-recursion-nonterminating.c new file mode 100644 index 0000000000..c47fbcdd49 --- /dev/null +++ b/tests/regression/78-termination/37-recursion-nonterminating.c @@ -0,0 +1,25 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --enable ana.context.widen +#include + +void recursiveFunction(int n) // NONTERMFUNDEC termination analysis shall mark fundec of non-terminating function +{ + // Base case: When n reaches 0, stop recursion + if (n == 30) + { + printf("Terminating recursion\n"); + return; + } + + printf("Recursive call with n = %d\n", n); + + // Recursive call: Decrement n and call the function again + recursiveFunction(n - 1); +} + +int main() +{ + // Call the recursive function with an initial value + recursiveFunction(5); + + return 0; +} diff --git a/tests/regression/78-termination/38-recursion-nested-terminating.c b/tests/regression/78-termination/38-recursion-nested-terminating.c new file mode 100644 index 0000000000..a471cfc386 --- /dev/null +++ b/tests/regression/78-termination/38-recursion-nested-terminating.c @@ -0,0 +1,41 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void innerRecursiveFunction(int n) +{ + if (n == 0) + { + printf("Terminating inner recursion\n"); + return; + } + + printf("Inner recursive call with n = %d\n", n); + + // Recursive call to the innerRecursiveFunction + innerRecursiveFunction(n - 1); +} + +void outerRecursiveFunction(int n) +{ + if (n == 0) + { + printf("Terminating outer recursion\n"); + return; + } + + printf("Outer recursive call with n = %d\n", n); + + // Recursive call to the outerRecursiveFunction + outerRecursiveFunction(n - 1); + + // Call to the innerRecursiveFunction + innerRecursiveFunction(n); +} + +int main() +{ + // Call the outerRecursiveFunction with an initial value + outerRecursiveFunction(3); + + return 0; +} diff --git a/tests/regression/78-termination/39-recursion-nested-nonterminating.c b/tests/regression/78-termination/39-recursion-nested-nonterminating.c new file mode 100644 index 0000000000..a8d7107442 --- /dev/null +++ b/tests/regression/78-termination/39-recursion-nested-nonterminating.c @@ -0,0 +1,29 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void innerRecursiveFunction() // TODO NONTERMFUNDEC termination analysis shall mark fundec of non-terminating function but can not as dead code is not analysed +{ + printf("Nested recursive call\n"); + + // Recursive call to the innerRecursiveFunction + innerRecursiveFunction(); +} + +void outerRecursiveFunction() // NONTERMFUNDEC termination analysis shall mark fundec of non-terminating function +{ + printf("Outer recursive call\n"); + + // Recursive call to the outerRecursiveFunction + outerRecursiveFunction(); + + // Call to the innerRecursiveFunction + innerRecursiveFunction(); +} + +int main() +{ + // Call the outerRecursiveFunction + outerRecursiveFunction(); + + return 0; +} diff --git a/tests/regression/78-termination/40-multi-expression-conditions-terminating.c b/tests/regression/78-termination/40-multi-expression-conditions-terminating.c new file mode 100644 index 0000000000..80f8c5a1e8 --- /dev/null +++ b/tests/regression/78-termination/40-multi-expression-conditions-terminating.c @@ -0,0 +1,44 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + int i; + + // Loop with complex conditions + for (i = 1; i <= 10; i++) + { + if (i > 5 && i % 2 == 0) // CIL defines new jump labels to default location (-1) + { + printf("%d ", i); + } + } + printf("\n"); + + // Loop with complex conditions + i = 1; + while (i <= 10) + { + if (i > 5 && i % 2 == 0) // CIL defines new jump labels to default location (-1) + { + printf("%d ", i); + } + i++; + } + printf("\n"); + + // Loop with multiple conditions + int s = 1; + while (s <= 10 && s % 2 == 0) // CIL defines new jump labels to default location (-1) + { + printf("Loop with Multiple Conditions: %d\n", s); + s++; + } + + // Loop with multiple variables + int t, u; + for (t = 1, u = 10; t <= 5 && u >= 5; t++, u--) // CIL defines new jump labels to default location (-1) + { + printf("Loop with Multiple Variables: %d %d\n", t, u); + } +} \ No newline at end of file diff --git a/tests/regression/78-termination/41-for-continue-terminating.c b/tests/regression/78-termination/41-for-continue-terminating.c new file mode 100644 index 0000000000..d87a705868 --- /dev/null +++ b/tests/regression/78-termination/41-for-continue-terminating.c @@ -0,0 +1,27 @@ +// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() +{ + // Loop with a continue statement + for (int i = 1; i <= 10; i++) + { + if (i % 2 == 0) + { + continue; // Converted to an goto to "for" in line 7 + } + printf("%d ", i); + } + printf("\n"); + + + // Loop with a continue statement + for (int r = 1; r <= 10; r++) + { + if (r % 3 == 0) + { + continue; // Converted to an goto to "for" in line 19 + } + printf("Loop with Continue: %d\n", r); + } +} \ No newline at end of file diff --git a/tests/regression/78-termination/42-downjumping-goto-loopless-terminating.c b/tests/regression/78-termination/42-downjumping-goto-loopless-terminating.c new file mode 100644 index 0000000000..48864883f7 --- /dev/null +++ b/tests/regression/78-termination/42-downjumping-goto-loopless-terminating.c @@ -0,0 +1,19 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() { // Currently not able to detect up-jumping loop free gotos + goto mark2; + +mark1: + printf("This is mark1\n"); + goto mark3; + +mark2: + printf("This is mark2\n"); + goto mark3; + +mark3: + printf("This is mark3\n"); + + return 0; +} diff --git a/tests/regression/78-termination/43-return-from-endless-loop-terminating.c b/tests/regression/78-termination/43-return-from-endless-loop-terminating.c new file mode 100644 index 0000000000..fb48e1cdbe --- /dev/null +++ b/tests/regression/78-termination/43-return-from-endless-loop-terminating.c @@ -0,0 +1,14 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +int main() { + int i = 1; + + while (i != 0) { + printf("%d\n", i); + i++; + if (i>10) { + return 0; + } + } +} diff --git a/tests/regression/78-termination/44-recursion-multiple-functions-terminating.c b/tests/regression/78-termination/44-recursion-multiple-functions-terminating.c new file mode 100644 index 0000000000..7f9b63527e --- /dev/null +++ b/tests/regression/78-termination/44-recursion-multiple-functions-terminating.c @@ -0,0 +1,40 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void functionB(int n); +void functionC(int n); +void functionD(int n); + +void functionA(int n) { + if (n > 0) { + printf("Function A: %d\n", n); + functionB(n - 1); + } +} + +void functionB(int n) { + if (n > 0) { + printf("Function B: %d\n", n); + functionC(n - 1); + } +} + +void functionC(int n) { + if (n > 0) { + printf("Function C: %d\n", n); + functionD(n - 1); + } +} + +void functionD(int n) { + if (n > 0) { + printf("Function D: %d\n", n); + functionA(n - 1); + } +} + +int main() { + int n = 15; + functionA(n); + return 0; +} diff --git a/tests/regression/78-termination/45-recursion-multiple-functions-nonterminating.c b/tests/regression/78-termination/45-recursion-multiple-functions-nonterminating.c new file mode 100644 index 0000000000..be47fde704 --- /dev/null +++ b/tests/regression/78-termination/45-recursion-multiple-functions-nonterminating.c @@ -0,0 +1,40 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void functionB(int n); +void functionC(int n); +void functionD(int n); + +void functionA(int n) { + if (n > 0) { + printf("Function A: %d\n", n); + functionB(n - 1); + } +} + +void functionB(int n) { + if (n > 0) { + printf("Function B: %d\n", n); + functionC(n - 1); + } +} + +void functionC(int n) { + if (n > 0) { + printf("Function C: %d\n", n); + functionD(n + 1); + } +} + +void functionD(int n) { + if (n > 0) { + printf("Function D: %d\n", n); + functionA(n + 1); + } +} + +int main() { + int n = 15; + functionA(n); + return 0; +} diff --git a/tests/regression/78-termination/46-recursion-different-context-terminating.c b/tests/regression/78-termination/46-recursion-different-context-terminating.c new file mode 100644 index 0000000000..2fa42f58fc --- /dev/null +++ b/tests/regression/78-termination/46-recursion-different-context-terminating.c @@ -0,0 +1,32 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void functionC(int n); + +void functionA(int n) { + if (n > 0) { + printf("Function A: %d\n", n); + functionC(n - 1); + } +} + +void functionB(int n) { + if (n > 0) { + printf("Function B: %d\n", n); + functionC(n - 1); + } +} + +void functionC(int n) { + if (n > 0) { + printf("Function C: %d\n", n); + functionC(n - 1); + } +} + +int main() { + int n = 5; + functionA(n + 1); + functionB(n + 7); + return 0; +} diff --git a/tests/regression/78-termination/47-recursion-different-context-nonterminating.c b/tests/regression/78-termination/47-recursion-different-context-nonterminating.c new file mode 100644 index 0000000000..b0e44bce92 --- /dev/null +++ b/tests/regression/78-termination/47-recursion-different-context-nonterminating.c @@ -0,0 +1,32 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include + +void functionC(int n); + +void functionA(int n) { + if (n > 0) { + printf("Function A: %d\n", n); + functionC(n - 1); + } +} + +void functionB(int n) { + if (n > 0) { + printf("Function B: %d\n", n); + functionC(n - 1); + } +} + +void functionC(int n) { + if (n > 0) { + printf("Function C: %d\n", n); + functionC(n); + } +} + +int main() { + int n = 5; + functionA(n + 1); + functionB(n + 7); + return 0; +} diff --git a/tests/regression/78-termination/48-dynamic-recursion-nonterminating.c b/tests/regression/78-termination/48-dynamic-recursion-nonterminating.c new file mode 100644 index 0000000000..d54c49fb43 --- /dev/null +++ b/tests/regression/78-termination/48-dynamic-recursion-nonterminating.c @@ -0,0 +1,10 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +void troll(void (*f) ()) +{ + f(f); +} + +int main() +{ + troll(troll); +} diff --git a/tests/regression/78-termination/49-longjmp.c b/tests/regression/78-termination/49-longjmp.c new file mode 100644 index 0000000000..be13cb286c --- /dev/null +++ b/tests/regression/78-termination/49-longjmp.c @@ -0,0 +1,11 @@ +// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra +#include +jmp_buf buf; +int main() +{ + if(setjmp(buf)) { + + } + + longjmp(buf, 1); +} diff --git a/tests/regression/78-termination/50-decreasing-signed-int.c b/tests/regression/78-termination/50-decreasing-signed-int.c new file mode 100644 index 0000000000..01daa5ee21 --- /dev/null +++ b/tests/regression/78-termination/50-decreasing-signed-int.c @@ -0,0 +1,13 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain octagon +int main() +{ + int x; + + if(x <= 0){ + return 0; + } + while (x > 0) { + x = x - 1; + } + return 0; +}