From 0ed3a00216396b67e0083d71237476bfed9b8682 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Mar 2024 13:37:00 +0200 Subject: [PATCH 1/5] Trace apron unassume join --- src/analyses/apron/relationAnalysis.apron.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index c7b62e8d16..3bc57149c9 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -722,7 +722,9 @@ struct in let rel = RD.remove_vars st.rel (List.map RV.local (VH.values v_ins |> List.of_enum)) in (* remove temporary g#in-s *) + if M.tracing then M.traceli "apron" "unassume join\n"; let st = D.join ctx.local {st with rel} in (* (strengthening) join *) + if M.tracing then M.traceu "apron" "unassume join\n"; M.info ~category:Witness "relation unassumed invariant: %a" d_exp e_orig; st | _ -> From 88c0e2e3bf59abbf2471a2a9c4265e854580e4fb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Mar 2024 13:21:34 +0200 Subject: [PATCH 2/5] Make relational unassume test match paper example --- tests/regression/56-witness/25-apron-unassume-strengthening.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c index 974387fbec..b8a779ae0e 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.c +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.c @@ -4,10 +4,10 @@ int main() { int x, y; x = 0; - if (x < y) { + if (x <= y) { __goblint_check(x == 0); // UNKNOWN (intentional by unassume) __goblint_check(x >= 0); - __goblint_check(x < y); // TODO: https://github.com/goblint/analyzer/issues/1373 + __goblint_check(x <= y); } return 0; } From 7c625f994b1491f8763d761ee9ffec891f63ee3e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Mar 2024 13:36:37 +0200 Subject: [PATCH 3/5] Add old variant of 56-witness/25-apron-unassume-strengthening back with explanation --- .../25-apron-unassume-strengthening.c | 13 ++++++++- .../25-apron-unassume-strengthening.yml | 29 +++++++++++++++++++ 2 files changed, 41 insertions(+), 1 deletion(-) diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c index b8a779ae0e..94765fec4d 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.c +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none +// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none --set ana.apron.domain octagon #include int main() { @@ -9,5 +9,16 @@ int main() { __goblint_check(x >= 0); __goblint_check(x <= y); } + + // With type bounds we have y <= 2147483647. + if (x < y) { // Assuming this implies x <= 2147483646 in closure. + // Unassuming 0 <= x actually unassumes 0 <= x <= 2147483647. + // Thus, strengthening cannot add x < y back. + __goblint_check(x == 0); // UNKNOWN (intentional by unassume) + __goblint_check(x >= 0); + __goblint_check(x < y); // TODO? Used to work without type bounds: https://github.com/goblint/analyzer/issues/1373. + } + + // TODO: Why swapped with polyhedra? return 0; } diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.yml b/tests/regression/56-witness/25-apron-unassume-strengthening.yml index 75d4df8026..edf6435383 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.yml +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.yml @@ -27,3 +27,32 @@ string: x >= 0 type: assertion format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: dec4db01-03ed-47dd-ae55-c84f8dcd51ed + creation_time: 2022-09-13T11:38:16Z + producer: + name: Goblint + version: heads/yaml-witness-unassume-0-g82e0e31ba-dirty + command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''19-apron-unassume-strengthening.c'' + ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' + ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' + ''goblint-dir'' ''.goblint-56-19''' + task: + input_files: + - 25-apron-unassume-strengthening.c + input_file_hashes: + 25-apron-unassume-strengthening.c: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83 + data_model: LP64 + language: C + location: + file_name: 25-apron-unassume-strengthening.c + file_hash: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83 + line: 17 + column: 4 + function: main + location_invariant: + string: x >= 0 + type: assertion + format: C From 6051f2a3d86760359a3863f348712002d9fd0d77 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 11 Mar 2024 14:00:27 +0200 Subject: [PATCH 4/5] Fix inconsistent strengthening behavior with polyhedra --- src/cdomains/apron/apronDomain.apron.ml | 11 +++++++++-- .../56-witness/25-apron-unassume-strengthening.c | 2 -- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 2b8f360bc5..bdec5db221 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -639,14 +639,21 @@ struct (* Whether [con1] contains a var in [env]. *) let env_exists_mem_con1 env con1 = try - Lincons1.iter (fun _ var -> - if Environment.mem_var env var then + Lincons1.iter (fun coeff var -> + (* Lincons1 from polyhedra may contain variable with zero coefficient. + These are silently not printed! *) + if not (Coeff.is_zero coeff) && Environment.mem_var env var then raise Not_found ) con1; false with Not_found -> true in + let env_exists_mem_con1 env con1 = + let r = env_exists_mem_con1 env con1 in + if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B\n" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r; + r + in (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *) (* Put those constraints which strictly are in one argument's env first, to (hopefully) ensure they remain. *) let (x_cons1_some_y, x_cons1_only_x) = Array.partition (env_exists_mem_con1 y_env) x_cons1 in diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c index 94765fec4d..bd7d720326 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.c +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.c @@ -18,7 +18,5 @@ int main() { __goblint_check(x >= 0); __goblint_check(x < y); // TODO? Used to work without type bounds: https://github.com/goblint/analyzer/issues/1373. } - - // TODO: Why swapped with polyhedra? return 0; } From 4f1e7176ffb8cfb7f9c77d710b61bc81571f865e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Mar 2024 11:46:21 +0200 Subject: [PATCH 5/5] Use Stdlib.Exit instead of Not_found for env_exists_mem_con1 --- src/cdomains/apron/apronDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index bdec5db221..93f6511e47 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -643,10 +643,10 @@ struct (* Lincons1 from polyhedra may contain variable with zero coefficient. These are silently not printed! *) if not (Coeff.is_zero coeff) && Environment.mem_var env var then - raise Not_found + raise Stdlib.Exit (* found *) ) con1; false - with Not_found -> + with Stdlib.Exit -> (* found *) true in let env_exists_mem_con1 env con1 =