From a7bf70efa4eddfa5f40a6175cc0fe72fceff401b Mon Sep 17 00:00:00 2001 From: Johanna Schinabeck Date: Sun, 11 Feb 2024 15:47:47 +0100 Subject: [PATCH] deleted context gas from C, is just tracked in ctx.local; updated testcases --- src/framework/constraints.ml | 33 ++++----- .../80-context_gas/01-basic_tests.c | 33 --------- .../01-basic_tests_bound_sens.c | 16 ++++ .../80-context_gas/02-basic_tests_bound_ins.c | 16 ++++ .../02-multiple_function_chain_tests.c | 73 ------------------- .../80-context_gas/03-contextGas0.c | 12 +-- .../80-context_gas/04-contextGasNeg.c | 12 +-- .../80-context_gas/05-circle_call_sens.c | 44 +++++++++++ .../80-context_gas/06-circle_call.c | 51 ------------- .../80-context_gas/06-circle_call_ins.c | 41 +++++++++++ .../80-context_gas/07-loop_unrolling.c | 64 ---------------- ...ursion_sens.c => 07-main_recursion_sens.c} | 0 ...rsion_insens.c => 08-main_recursion_ins.c} | 2 +- .../{10-endless_loop.c => 09-endless_loop.c} | 0 ...d_handling.c => 10-thread_handling_sens.c} | 41 +++++------ .../80-context_gas/11-thread_handling_ins.c | 67 +++++++++++++++++ .../12-multiple_function_chain_sens.c | 51 +++++++++++++ .../13-multiple_function_chain_ins.c | 50 +++++++++++++ .../{05-ackermann.c => 14-ackermann.c} | 0 .../80-context_gas/15-compl_loop_unrolling.c | 32 ++++++++ .../80-context_gas/16-loop_unrolling_sens.c | 33 +++++++++ .../80-context_gas/17-loop_unrolling_ins.c | 25 +++++++ .../18-loop_unrolling_big_loop.c | 26 +++++++ 23 files changed, 438 insertions(+), 284 deletions(-) delete mode 100644 tests/regression/80-context_gas/01-basic_tests.c create mode 100644 tests/regression/80-context_gas/01-basic_tests_bound_sens.c create mode 100644 tests/regression/80-context_gas/02-basic_tests_bound_ins.c delete mode 100644 tests/regression/80-context_gas/02-multiple_function_chain_tests.c create mode 100644 tests/regression/80-context_gas/05-circle_call_sens.c delete mode 100644 tests/regression/80-context_gas/06-circle_call.c create mode 100644 tests/regression/80-context_gas/06-circle_call_ins.c delete mode 100644 tests/regression/80-context_gas/07-loop_unrolling.c rename tests/regression/80-context_gas/{08-main_recursion_sens.c => 07-main_recursion_sens.c} (100%) rename tests/regression/80-context_gas/{09-main_recursion_insens.c => 08-main_recursion_ins.c} (91%) rename tests/regression/80-context_gas/{10-endless_loop.c => 09-endless_loop.c} (100%) rename tests/regression/80-context_gas/{11-thread_handling.c => 10-thread_handling_sens.c} (56%) create mode 100644 tests/regression/80-context_gas/11-thread_handling_ins.c create mode 100644 tests/regression/80-context_gas/12-multiple_function_chain_sens.c create mode 100644 tests/regression/80-context_gas/13-multiple_function_chain_ins.c rename tests/regression/80-context_gas/{05-ackermann.c => 14-ackermann.c} (100%) create mode 100644 tests/regression/80-context_gas/15-compl_loop_unrolling.c create mode 100644 tests/regression/80-context_gas/16-loop_unrolling_sens.c create mode 100644 tests/regression/80-context_gas/17-loop_unrolling_ins.c create mode 100644 tests/regression/80-context_gas/18-loop_unrolling_big_loop.c diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 56ac2ea654..65ce60f897 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -500,7 +500,7 @@ end module NoContext = struct let name = "no context" end module IntConf = struct - let n () = get_int "ana.context.ctx_gas_value" + 1 + let n () = max_int let names x = Format.asprintf "%d" x end @@ -508,21 +508,20 @@ end If the context gas is 0, the remaining function calls are analyzed context insensitively (before the analysis is context sensitive) *) module ContextGasLifter (S:Spec) : Spec with module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf)) - and module C = Printable.Prod (Printable.Option (S.C) (NoContext)) (Printable.Chain (IntConf)) + and module C = Printable.Option (S.C) (NoContext) and module G = S.G = struct include S - module Context_Gas_Prod (Base1: Printable.S) (Base2: Printable.S) = + module Context_Gas_Prod (Base1: Lattice.S) (Base2: Lattice.S) = struct - include Printable.Prod (Base1) (Base2) + include Lattice.Prod (Base1) (Base2) let printXml f (x,y) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\nContext Gas Value\n\n%a\n\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x Base2.printXml y end - - module D = Lattice.Prod (S.D) (Lattice.Chain (IntConf)) - module C = Context_Gas_Prod (Printable.Option (S.C) (NoContext)) (Printable.Chain (IntConf)) + module D = Context_Gas_Prod (S.D) (Lattice.Chain (IntConf)) + module C = Printable.Option (S.C) (NoContext) module G = S.G module V = S.V module P = @@ -532,17 +531,15 @@ struct end (* returns context gas value of the given ctx *) - let cg_val ctx = - (* snd ctx.local = snd (ctx.context ()), but ctx.local must be used here due to initialization *) - snd ctx.local + let cg_val ctx = snd ctx.local let name () = S.name ()^" with context gas" - let startstate v = S.startstate v, (get_int "ana.context.ctx_gas_value") - let exitstate v = S.exitstate v, (get_int "ana.context.ctx_gas_value") (* TODO: probably doesn't matter*) + let startstate v = S.startstate v, get_int "ana.context.ctx_gas_value" + let exitstate v = S.exitstate v, get_int "ana.context.ctx_gas_value" (* TODO: probably doesn't matter*) let morphstate v (d,i) = S.morphstate v d, i let context fd (d,i) = - if i <= 0 then (None, 0) else ((Some (S.context fd d)), i) + if i <= 0 then None else Some (S.context fd d) let conv (ctx:(D.t,G.t,C.t,V.t) ctx): (S.D.t,G.t,S.C.t,V.t)ctx = if (cg_val ctx <= 0) @@ -551,7 +548,7 @@ struct ; context = (fun () -> ctx_failwith "no context (contextGas = 0)")} else {ctx with local = fst ctx.local ; split = (fun d es -> ctx.split (d, cg_val ctx) es) - ; context = (fun () -> Option.get (fst (ctx.context ())))} + ; context = (fun () -> Option.get (ctx.context ()))} let enter ctx r f args = let liftmap_tup = List.map (fun (x,y) -> (x, cg_val ctx), (y, max 0 (cg_val ctx - 1))) in @@ -561,8 +558,6 @@ struct let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in liftmap (S.threadenter (conv ctx) ~multiple lval f args) - let liftmap f ctx = List.map (fun (x) -> (x, cg_val ctx)) f - let sync ctx reason = S.sync (conv ctx) reason, cg_val ctx let query ctx q = S.query (conv ctx) q let assign ctx lval expr = S.assign (conv ctx) lval expr, cg_val ctx @@ -573,9 +568,9 @@ struct let asm ctx = S.asm (conv ctx), cg_val ctx let skip ctx = S.skip (conv ctx), cg_val ctx let special ctx r f args = S.special (conv ctx) r f args, cg_val ctx - let combine_env ctx r fe f args fc es f_ask = S.combine_env (conv ctx) r fe f args (Option.bind fc (fun x -> fst x)) (fst es) f_ask, cg_val ctx - let combine_assign ctx r fe f args fc es f_ask = S.combine_assign (conv ctx) r fe f args (Option.bind fc (fun x -> fst x)) (fst es) f_ask, cg_val ctx - let paths_as_set ctx = liftmap (S.paths_as_set (conv ctx)) ctx + let combine_env ctx r fe f args fc es f_ask = S.combine_env (conv ctx) r fe f args (Option.bind fc (fun x -> x)) (fst es) f_ask, cg_val ctx + let combine_assign ctx r fe f args fc es f_ask = S.combine_assign (conv ctx) r fe f args (Option.bind fc (fun x -> x)) (fst es) f_ask, cg_val ctx + let paths_as_set ctx = List.map (fun (x) -> (x, cg_val ctx)) @@ S.paths_as_set (conv ctx) let threadspawn ctx ~multiple lval f args fctx = S.threadspawn (conv ctx) ~multiple lval f args (conv fctx), cg_val ctx let event ctx e octx = S.event (conv ctx) e (conv octx), cg_val ctx end diff --git a/tests/regression/80-context_gas/01-basic_tests.c b/tests/regression/80-context_gas/01-basic_tests.c deleted file mode 100644 index 59c9f82981..0000000000 --- a/tests/regression/80-context_gas/01-basic_tests.c +++ /dev/null @@ -1,33 +0,0 @@ -// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 -// Basic examples - -int f(int x, int y) -{ - if (x == 0) - { - - return y; - } - return f(--x, --y); -} - -int main() -{ - int y = f(0, 0); - __goblint_check(y == 0); - - int y = f(5, 5); - __goblint_check(y == 0); - - int y = f(7, 7); - __goblint_check(y == 0); // boundary (included) - - int y = f(8, 8); - __goblint_check(y == 0); // UNKNOWN //boundary (excluded) - - int y = f(10, 10); - __goblint_check(y == 0); // UNKNOWN - - int y = f(1000, 1000); - __goblint_check(y == 0); // UNKNOWN -} \ No newline at end of file diff --git a/tests/regression/80-context_gas/01-basic_tests_bound_sens.c b/tests/regression/80-context_gas/01-basic_tests_bound_sens.c new file mode 100644 index 0000000000..dcc48381fb --- /dev/null +++ b/tests/regression/80-context_gas/01-basic_tests_bound_sens.c @@ -0,0 +1,16 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 +// Basic examples + +int f(int x, int y) +{ + if (x == 0) + { + return y; + } + return f(x - 1, y - 1); +} + +int main() +{ + __goblint_check(f(8, 8) == 0); // boundary (included) +} \ No newline at end of file diff --git a/tests/regression/80-context_gas/02-basic_tests_bound_ins.c b/tests/regression/80-context_gas/02-basic_tests_bound_ins.c new file mode 100644 index 0000000000..0cfa24f5c1 --- /dev/null +++ b/tests/regression/80-context_gas/02-basic_tests_bound_ins.c @@ -0,0 +1,16 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 +// Basic examples + +int f(int x, int y) +{ + if (x == 0) + { + return y; + } + return f(x - 1, y - 1); +} + +int main() +{ + __goblint_check(f(9, 9) == 0); // UNKNOWN //boundary (excluded) +} \ No newline at end of file diff --git a/tests/regression/80-context_gas/02-multiple_function_chain_tests.c b/tests/regression/80-context_gas/02-multiple_function_chain_tests.c deleted file mode 100644 index 912425d2fb..0000000000 --- a/tests/regression/80-context_gas/02-multiple_function_chain_tests.c +++ /dev/null @@ -1,73 +0,0 @@ -// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 -// Tests multiple recursive function calls -#include - -int h(int i) -{ - int res = 0; - if (i == 0) - { - res = 1; - } - if (i > 0) - { - res = h(--i); - } - return res; -} - -int g(int i) -{ - int res = 0; - if (i == 0) - { - res = 2; - } - if (i > 0) - { - res = h(--i); - } - return res; -} - -int f(int i) -{ - int res = 0; - if (i == 0) - { - res = 3; - } - if (i > 0) - { - res = g(--i); - } - return res; -} - -int main(void) -{ - __goblint_check(f(-5) == 0); - __goblint_check(f(0) == 3); - __goblint_check(f(1) == 2); - __goblint_check(f(2) == 1); - __goblint_check(f(7) == 1); // boundary (included) - __goblint_check(f(8) == 1); // UNKNOWN //boundary (excluded) - __goblint_check(f(20) == 1); // UNKNOWN - - __goblint_check(g(-10) == 0); - __goblint_check(g(0) == 2); - __goblint_check(g(1) == 1); - - __goblint_check(h(-10) == 0); - __goblint_check(h(0) == 1); - __goblint_check(h(7) == 1); // boundary (included) - __goblint_check(h(8) == 1); // UNKNOWN //boundary (excluded) - - int res1 = h(5); - int res2 = h(4); - int result = res1 + res2; - __goblint_check(result == 2); - - __goblint_check(f(g(h(7))) == 2); // h(7) = 1; g(1) = 1; f(1) = 2; - __goblint_check(f(g(h(8))) == 2); // UNKNOWN // h(8) = UNKNOWN -} diff --git a/tests/regression/80-context_gas/03-contextGas0.c b/tests/regression/80-context_gas/03-contextGas0.c index aadb93628c..dc445ba371 100644 --- a/tests/regression/80-context_gas/03-contextGas0.c +++ b/tests/regression/80-context_gas/03-contextGas0.c @@ -4,20 +4,12 @@ int f(int x, int y) { if (x == 0) { - return y; } - return f(--x, --y); + return f(x - 1, y - 1); } int main() { - int y = f(0, 0); - __goblint_check(y == 0); // UNKNOWN - - int y = f(5, 5); - __goblint_check(y == 0); // UNKNOWN - - int y = f(1000, 1000); - __goblint_check(y == 0); // UNKNOWN + __goblint_check(f(1000, 1000) == 0); // UNKNOWN } \ No newline at end of file diff --git a/tests/regression/80-context_gas/04-contextGasNeg.c b/tests/regression/80-context_gas/04-contextGasNeg.c index 0cd41b6199..30d2d4f9b2 100644 --- a/tests/regression/80-context_gas/04-contextGasNeg.c +++ b/tests/regression/80-context_gas/04-contextGasNeg.c @@ -4,20 +4,12 @@ int f(int x, int y) { if (x == 0) { - return y; } - return f(--x, --y); + return f(x - 1, y - 1); } int main() { - int y = f(0, 0); - __goblint_check(y == 0); // UNKNOWN - - int y = f(5, 5); - __goblint_check(y == 0); // UNKNOWN - - int y = f(1000, 1000); - __goblint_check(y == 0); // UNKNOWN + __goblint_check(f(5, 5) == 0); // UNKNOWN } \ No newline at end of file diff --git a/tests/regression/80-context_gas/05-circle_call_sens.c b/tests/regression/80-context_gas/05-circle_call_sens.c new file mode 100644 index 0000000000..b9a20432a9 --- /dev/null +++ b/tests/regression/80-context_gas/05-circle_call_sens.c @@ -0,0 +1,44 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 15 +// Checks if recursion in loops is handled properly +#include + +int f(int i); + +int g(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return f(i + 1); + } + return 11; +} + +int f(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return g(i - 2) + g(i - 3); + } + return 12; +} + +int main(void) +{ + __goblint_check(f(0) == 2); + __goblint_check(f(7) == 101); + __goblint_check(f(9) == 265); + __goblint_check(f(10) == 429); + + __goblint_check(g(0) == 1); + __goblint_check(g(3) == 25); + __goblint_check(g(6) == 101); + __goblint_check(g(8) == 265); +} diff --git a/tests/regression/80-context_gas/06-circle_call.c b/tests/regression/80-context_gas/06-circle_call.c deleted file mode 100644 index 2347ef0b70..0000000000 --- a/tests/regression/80-context_gas/06-circle_call.c +++ /dev/null @@ -1,51 +0,0 @@ -// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 15 -// Checks if recursion in loops is handled properly -#include - -int f(int i); - -int g(int i) -{ - int res = 0; - if (i == 0) - { - res = 1; - } - if (i > 0) - { - res = f(i + 1); - } - return res; -} - -int f(int i) -{ - int res = 0; - if (i == 0) - { - res = 2; - } - if (i > 0) - { - res = g(i - 2) + g(i - 3); - } - return res; -} - -int main(void) -{ - printf("%i, %i\n", f(200), g(10)); - - __goblint_check(f(0) == 2); - __goblint_check(f(3) == 2); - __goblint_check(f(7) == 13); - __goblint_check(f(8) == 21); // UNKNOWN //boundary (excluded) - __goblint_check(f(9) == 34); // UNKNOWN - __goblint_check(f(20) == 6765); // UNKNOWN - - __goblint_check(g(3) == 3); - __goblint_check(g(6) == 13); // boundary (included) - __goblint_check(g(7) == 21); // UNKNOWN - __goblint_check(g(8) == 34); // UNKNOWN - __goblint_check(g(20) == 10946); // UNKNOWN -} diff --git a/tests/regression/80-context_gas/06-circle_call_ins.c b/tests/regression/80-context_gas/06-circle_call_ins.c new file mode 100644 index 0000000000..feb97c1e2c --- /dev/null +++ b/tests/regression/80-context_gas/06-circle_call_ins.c @@ -0,0 +1,41 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 15 +// Checks if recursion in loops is handled properly +#include + +int f(int i); + +int g(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return f(i + 1); + } + return 11; +} + +int f(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return g(i - 2) + g(i - 3); + } + return 12; +} + +int main(void) +{ + + __goblint_check(f(13) == 233); // UNKNOWN + __goblint_check(f(20) == 6765); // UNKNOWN + + __goblint_check(g(13) == 377); // UNKNOWN + __goblint_check(g(20) == 10946); // UNKNOWN +} diff --git a/tests/regression/80-context_gas/07-loop_unrolling.c b/tests/regression/80-context_gas/07-loop_unrolling.c deleted file mode 100644 index 4463f0fab3..0000000000 --- a/tests/regression/80-context_gas/07-loop_unrolling.c +++ /dev/null @@ -1,64 +0,0 @@ -// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set exp.unrolling-factor 3 --set ana.context.ctx_gas_value 10 -// TODO -#include - -int f(int i) -{ - int res = 0; - if (i == 0) - { - res = 1; - } - if (i > 0) - { - res = f(--i); - } - return res; -} - -int main(void) -{ - for (int i = 1; i > 0; i--) - { - __goblint_check(f(2) == 1); - __goblint_check(f(2000) == 1); // UNKNOWN - } - - // loop should be completely unrolled - for (int i = 3; i > 0; i--) - { - __goblint_check(f(1) == 1); - __goblint_check(f(20) == 1); // UNKNOWN - } - - int res1 = 0; - int res2 = 0; - int result = 0; - - // context sensitive analysis - for (int i = 5; i > 0; i--) - { - res1 = f(3); - res2 = f(i); - __goblint_check(res1 == 1); - __goblint_check(res2 == 1); // TODO - result += res1 + res2; - } - __goblint_check(res1 == 1); - __goblint_check(res2 == 1); // TODO - __goblint_check(result == 10); // TODO - - for (int i = 5; i > 0; i--) - { - __goblint_check(f(0) == 1); - __goblint_check(f(7) == 1); // boundary (included)) - __goblint_check(f(8) == 1); // UNKNOWN //boundary (excluded) - } - - // high number of iterations - for (int i = 500; i > 0; i--) - { - __goblint_check(f(i) == 1); // UNKNOWN - __goblint_check(f(4) == 1); - } -} diff --git a/tests/regression/80-context_gas/08-main_recursion_sens.c b/tests/regression/80-context_gas/07-main_recursion_sens.c similarity index 100% rename from tests/regression/80-context_gas/08-main_recursion_sens.c rename to tests/regression/80-context_gas/07-main_recursion_sens.c diff --git a/tests/regression/80-context_gas/09-main_recursion_insens.c b/tests/regression/80-context_gas/08-main_recursion_ins.c similarity index 91% rename from tests/regression/80-context_gas/09-main_recursion_insens.c rename to tests/regression/80-context_gas/08-main_recursion_ins.c index bd0afdf563..f28ef0cd95 100644 --- a/tests/regression/80-context_gas/09-main_recursion_insens.c +++ b/tests/regression/80-context_gas/08-main_recursion_ins.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 // Without context insensitive analysis: Stack Overflow #include diff --git a/tests/regression/80-context_gas/10-endless_loop.c b/tests/regression/80-context_gas/09-endless_loop.c similarity index 100% rename from tests/regression/80-context_gas/10-endless_loop.c rename to tests/regression/80-context_gas/09-endless_loop.c diff --git a/tests/regression/80-context_gas/11-thread_handling.c b/tests/regression/80-context_gas/10-thread_handling_sens.c similarity index 56% rename from tests/regression/80-context_gas/11-thread_handling.c rename to tests/regression/80-context_gas/10-thread_handling_sens.c index 5077baa8f8..11db96e100 100644 --- a/tests/regression/80-context_gas/11-thread_handling.c +++ b/tests/regression/80-context_gas/10-thread_handling_sens.c @@ -4,44 +4,38 @@ int f(int i) { - int res = 0; if (i == 0) { - res = 1; + return 1; } if (i > 0) { - res = f(--i); + return f(i - 1); } - return res; } int g(int i) { - int res = 0; if (i == 0) { - res = 3; + return 2; } if (i > 0) { - res = g(--i); + return g(i - 1); } - return res; } int h(int i) { - int res = 0; if (i == 0) { - res = 2; + return 3; } if (i > 0) { - res = g(--i); + return g(i - 1); } - return res; } int procedure(int num_iterat) @@ -56,31 +50,32 @@ int procedure(int num_iterat) void *t_sens(void *arg) { int result = procedure(0); - __goblint_check(result == 8); + __goblint_check(result == 9); - result = procedure(5); - __goblint_check(result == 10); + result = procedure(6); + __goblint_check(result == 7); return NULL; } -void *t_insens(void *arg) +void *t_sens2(void *arg) { - int result = procedure(6); - __goblint_check(result == 10); // UNKNOWN + int result = procedure(1); + __goblint_check(result == 7); - result = procedure(60); - __goblint_check(result == 10); // UNKNOWN + result = procedure(8); + __goblint_check(result == 7); return NULL; } int main() { pthread_t id; + pthread_t id2; - // Creat the thread + // Create the thread pthread_create(&id, NULL, t_sens, NULL); - // Creat the thread - pthread_create(&id, NULL, t_insens, NULL); + // Create the thread + pthread_create(&id2, NULL, t_sens2, NULL); return 0; } diff --git a/tests/regression/80-context_gas/11-thread_handling_ins.c b/tests/regression/80-context_gas/11-thread_handling_ins.c new file mode 100644 index 0000000000..bd3ea86f80 --- /dev/null +++ b/tests/regression/80-context_gas/11-thread_handling_ins.c @@ -0,0 +1,67 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set ana.context.ctx_gas_value 10 +#include +#include + +int f(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return f(i - 1); + } +} + +int g(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return g(i - 1); + } +} + +int h(int i) +{ + if (i == 0) + { + return 3; + } + if (i > 0) + { + return g(i - 1); + } +} + +int procedure(int num_iterat) +{ + int res1 = f(num_iterat); + int res2 = g(num_iterat); + int res3 = h(num_iterat); + int res4 = h(num_iterat); + return res1 + res2 + res3 + res4; +} + +void *t_insens(void *arg) +{ + int result = procedure(9); + __goblint_check(result == 7); // UNKNOWN + + result = procedure(60); + __goblint_check(result == 7); // UNKNOWN + return NULL; +} + +int main() +{ + pthread_t id; + + // Create the thread + pthread_create(&id, NULL, t_insens, NULL); + return 0; +} diff --git a/tests/regression/80-context_gas/12-multiple_function_chain_sens.c b/tests/regression/80-context_gas/12-multiple_function_chain_sens.c new file mode 100644 index 0000000000..89c0d708f5 --- /dev/null +++ b/tests/regression/80-context_gas/12-multiple_function_chain_sens.c @@ -0,0 +1,51 @@ +// PARAM: --enable ana.int.interval_set --enable ana.context.ctx_gas --set ana.context.ctx_gas_value 10 +// Tests multiple recursive function calls +#include + +int h(int i) +{ + if (i == 0) + { + return 3; + } + if (i > 0) + { + return h(i - 1); + } +} + +int g(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return h(i - 1); + } +} + +int f(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return g(i - 1); + } +} + +int main(void) +{ + __goblint_check(f(10) == 3); + __goblint_check(f(8) == 3); + __goblint_check(h(5) == 3); + + __goblint_check(f(0) == 1); + __goblint_check(f(1) == 2); + __goblint_check(g(0) == 2); + __goblint_check(g(1) == 3); +} diff --git a/tests/regression/80-context_gas/13-multiple_function_chain_ins.c b/tests/regression/80-context_gas/13-multiple_function_chain_ins.c new file mode 100644 index 0000000000..321df17938 --- /dev/null +++ b/tests/regression/80-context_gas/13-multiple_function_chain_ins.c @@ -0,0 +1,50 @@ +// PARAM: --enable ana.int.interval_set --enable ana.context.ctx_gas --set ana.context.ctx_gas_value 10 +// Tests multiple recursive function calls +#include + +int h(int i) +{ + if (i == 0) + { + return 3; + } + if (i > 0) + { + return h(i - 1); + } +} + +int g(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return h(i - 1); + } +} + +int f(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return g(i - 1); + } +} + +int main(void) +{ + __goblint_check(f(11) == 3); // UNKNOWN + __goblint_check(g(12) == 3); // UNKNOWN + __goblint_check(g(20) == 3); // UNKNOWN + __goblint_check(f(20) == 3); // UNKNOWN + __goblint_check(h(40) == 3); // UNKNOWN + __goblint_check(h(300) == 3); // UNKNOWN + __goblint_check(f(300) == 3); // UNKNOWN +} diff --git a/tests/regression/80-context_gas/05-ackermann.c b/tests/regression/80-context_gas/14-ackermann.c similarity index 100% rename from tests/regression/80-context_gas/05-ackermann.c rename to tests/regression/80-context_gas/14-ackermann.c diff --git a/tests/regression/80-context_gas/15-compl_loop_unrolling.c b/tests/regression/80-context_gas/15-compl_loop_unrolling.c new file mode 100644 index 0000000000..bab565688c --- /dev/null +++ b/tests/regression/80-context_gas/15-compl_loop_unrolling.c @@ -0,0 +1,32 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set exp.unrolling-factor 3 --set ana.context.ctx_gas_value 10 +// TODO +#include + +int f(int i) +{ + if (i == 0) + { + return 11; + } + if (i > 0) + { + return f(i - 1); + } + return 1; +} + +int main(void) +{ + // loop should be completely unrolled + for (int i = 3; i > 0; i--) + { + __goblint_check(f(1) == 11); + __goblint_check(f(20) == 11); // UNKNOWN + } + + for (int i = 1; i > 0; i--) + { + __goblint_check(f(2) == 11); + __goblint_check(f(2000) == 11); // UNKNOWN + } +} diff --git a/tests/regression/80-context_gas/16-loop_unrolling_sens.c b/tests/regression/80-context_gas/16-loop_unrolling_sens.c new file mode 100644 index 0000000000..4c647bff7b --- /dev/null +++ b/tests/regression/80-context_gas/16-loop_unrolling_sens.c @@ -0,0 +1,33 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set exp.unrolling-factor 3 --set ana.context.ctx_gas_value 10 +// TODO +#include + +int f(int i) +{ + if (i == 0) + { + return 11; + } + if (i > 0) + { + return f(i - 1); + } + return 1; +} + +int main(void) +{ + int res1 = 0; + int res2 = 0; + + // context sensitive analysis + for (int i = 5; i > 0; i--) + { + res1 = f(3); + res2 = f(i); + __goblint_check(res1 == 11); + __goblint_check(res2 == 11); + } + __goblint_check(res1 == 11); + __goblint_check(res2 == 11); +} diff --git a/tests/regression/80-context_gas/17-loop_unrolling_ins.c b/tests/regression/80-context_gas/17-loop_unrolling_ins.c new file mode 100644 index 0000000000..ceab5a870f --- /dev/null +++ b/tests/regression/80-context_gas/17-loop_unrolling_ins.c @@ -0,0 +1,25 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set exp.unrolling-factor 3 --set ana.context.ctx_gas_value 10 +// TODO +#include + +int f(int i) +{ + if (i == 0) + { + return 11; + } + if (i > 0) + { + return f(i - 1); + } + return 1; +} + +int main(void) +{ + + for (int i = 5; i > 0; i--) + { + __goblint_check(f(11) == 11); // UNKNOWN + } +} diff --git a/tests/regression/80-context_gas/18-loop_unrolling_big_loop.c b/tests/regression/80-context_gas/18-loop_unrolling_big_loop.c new file mode 100644 index 0000000000..d8c5e2a013 --- /dev/null +++ b/tests/regression/80-context_gas/18-loop_unrolling_big_loop.c @@ -0,0 +1,26 @@ +// PARAM: --enable ana.context.ctx_gas --enable ana.int.interval_set --set exp.unrolling-factor 3 --set ana.context.ctx_gas_value 10 +// TODO +#include + +int f(int i) +{ + if (i == 0) + { + return 11; + } + if (i > 0) + { + return f(i - 1); + } + return 1; +} + +int main(void) +{ + // high number of iterations + for (int i = 500; i > 0; i--) + { + __goblint_check(f(i) == 11); // UNKNOWN + __goblint_check(f(4) == 11); + } +}