From 022a9bcaadc762c2f5d46db7d564c55dec58ba72 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Jan 2024 10:38:40 +0100 Subject: [PATCH 1/4] `affeq`: Fix array OOB in `invariant` --- .../apron/affineEqualityDomain.apron.ml | 2 +- tests/regression/63-affeq/19-witness.c | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 tests/regression/63-affeq/19-witness.c diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ab24515c28..ce3f2592f4 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -681,7 +681,7 @@ struct let invariant t = let invariant m = let earray = Lincons1.array_make t.env (Matrix.num_rows m) in - for i = 0 to Lincons1.array_length earray do + for i = 0 to (Lincons1.array_length earray -1) do let row = Matrix.get_row m i in let coeff_vars = List.map (fun x -> Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in diff --git a/tests/regression/63-affeq/19-witness.c b/tests/regression/63-affeq/19-witness.c new file mode 100644 index 0000000000..1659e01cb6 --- /dev/null +++ b/tests/regression/63-affeq/19-witness.c @@ -0,0 +1,18 @@ +//SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none --set ana.relation.privatization top --enable witness.yaml.enabled +// Identical to Example 63/01; additionally checking that writing out witnesses does not crash the analyzer +#include + +void main(void) { + int i; + int j; + int k; + i = 2; + j = k + 5; + + while (i < 100) { + __goblint_check(3 * i - j + k == 1); + i = i + 1; + j = j + 3; + } + __goblint_check(3 * i - j + k == 1); +} From f99f320118a84ec0c243ca3aeda40737e450e376 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Jan 2024 12:53:45 +0100 Subject: [PATCH 2/4] Simplify --- src/cdomains/apron/affineEqualityDomain.apron.ml | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ce3f2592f4..bc1cfe41cf 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -680,19 +680,15 @@ struct let invariant t = let invariant m = - let earray = Lincons1.array_make t.env (Matrix.num_rows m) in - for i = 0 to (Lincons1.array_length earray -1) do + let one_constraint i = let row = Matrix.get_row m i in let coeff_vars = List.map (fun x -> Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in - Lincons1.set_list (Lincons1.array_get earray i) coeff_vars (Some cst) - done; - let {lincons0_array; array_env}: Lincons1.earray = earray in - Array.enum lincons0_array - |> Enum.map (fun (lincons0: Lincons0.t) -> - Lincons1.{lincons0; env = array_env} - ) - |> List.of_enum + let e1 = Linexpr1.make t.env in + Linexpr1.set_list e1 coeff_vars (Some cst); + Lincons1.make e1 EQ + in + List.init (Matrix.num_rows m) (one_constraint) in BatOption.map_default invariant [] t.d From ca18e353f4beba13867628c96daf78fe3ae059bd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Jan 2024 14:14:28 +0100 Subject: [PATCH 3/4] Remark on issue with fractional coefficients --- tests/regression/63-affeq/19-witness.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tests/regression/63-affeq/19-witness.c b/tests/regression/63-affeq/19-witness.c index 1659e01cb6..541aceab29 100644 --- a/tests/regression/63-affeq/19-witness.c +++ b/tests/regression/63-affeq/19-witness.c @@ -15,4 +15,20 @@ void main(void) { j = j + 3; } __goblint_check(3 * i - j + k == 1); + + // Represented with fractional coefficients and thus not put into witness yet + + int a = 0; + int b = 0; + int z = 0; + + while(z < 100) { + a++; + b += 2; + z++; + + __goblint_check(2*z - b == 0); + // b == 2*z is put into the witness + } + } From a521bdf24abf6a24c3086fd25be30722f99b8d7b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Jan 2024 17:02:24 +0100 Subject: [PATCH 4/4] Rm spurious parens Co-authored-by: Julian Erhard --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index bc1cfe41cf..55937a323d 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -688,7 +688,7 @@ struct Linexpr1.set_list e1 coeff_vars (Some cst); Lincons1.make e1 EQ in - List.init (Matrix.num_rows m) (one_constraint) + List.init (Matrix.num_rows m) one_constraint in BatOption.map_default invariant [] t.d