From 5ee421656bba32dde785f3f079d3e1567c50b0dd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 12 Feb 2023 15:41:05 +0100 Subject: [PATCH 1/3] Introduce attribute `goblint_stub` for variables to prevent tracking it relationally --- lib/sv-comp/stub/src/sv-comp.c | 2 +- src/autoTune.ml | 4 ++-- tests/regression/46-apron2/30-autotune-stub.c | 15 +++++++++++++++ 3 files changed, 18 insertions(+), 3 deletions(-) create mode 100644 tests/regression/46-apron2/30-autotune-stub.c diff --git a/lib/sv-comp/stub/src/sv-comp.c b/lib/sv-comp/stub/src/sv-comp.c index 230d66eae0..12c04125d6 100644 --- a/lib/sv-comp/stub/src/sv-comp.c +++ b/lib/sv-comp/stub/src/sv-comp.c @@ -13,7 +13,7 @@ void __VERIFIER_assume(int expression) { if (!expression) { LOOP: goto LOOP; }; // #define __VERIFIER_nondet(X) X __VERIFIER_nondet_##X() { X val; return val; } #define __VERIFIER_nondet2(X, Y) \ X __VERIFIER_nondet_##Y() __attribute__((goblint_stub)); \ - X __VERIFIER_nondet_##Y() { X val; return val; } + X __VERIFIER_nondet_##Y() { X val __attribute__((goblint_stub)); return val; } #define __VERIFIER_nondet(X) __VERIFIER_nondet2(X, X) __VERIFIER_nondet2(_Bool, bool) diff --git a/src/autoTune.ml b/src/autoTune.ml index 67b4c80f36..0e7210ea9b 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -245,7 +245,7 @@ let isComparison = function let rec extractVar = function | UnOp (Neg, e, _) -> extractVar e - | Lval ((Var info),_) -> Some info + | Lval ((Var info),_) when not (List.exists (fun (Attr(s,_)) -> s = "goblint_stub") info.vattr) -> Some info | _ -> None let extractOctagonVars = function @@ -283,7 +283,7 @@ class octagonVariableVisitor(varMap, globals) = object handle varMap 5 globals (extractOctagonVars e2) ; DoChildren ) - | Lval ((Var info),_) -> handle varMap 1 globals (Some (`Right info)) ; SkipChildren + | Lval ((Var info),_) when not (List.exists (fun (Attr(s,_)) -> s = "goblint_stub") info.vattr) -> handle varMap 1 globals (Some (`Right info)) ; SkipChildren (*Traverse down only operations fitting for linear equations*) | UnOp (Neg, _,_) | BinOp (PlusA,_,_,_) diff --git a/tests/regression/46-apron2/30-autotune-stub.c b/tests/regression/46-apron2/30-autotune-stub.c new file mode 100644 index 0000000000..2e47bb0547 --- /dev/null +++ b/tests/regression/46-apron2/30-autotune-stub.c @@ -0,0 +1,15 @@ +//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled +// Check that autotuner respect goblint_stub attributes as hints to not track variables. +#include + +int main () { + // Normally these appear only inside our stubs to prevent tracking relational information for variables which will never have interesting values associated with them + int x __attribute__((goblint_stub)); + int y __attribute__((goblint_stub)); + + if( x < y) { + __goblint_check(x < y); //UNKNOWN! + } + + return 0; +} From c78ff6fe994829e93ac68065111c63497b168d39 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 14 Feb 2023 09:09:27 +0100 Subject: [PATCH 2/3] Use `//UNKNOWN` consistently --- tests/regression/46-apron2/30-autotune-stub.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/46-apron2/30-autotune-stub.c b/tests/regression/46-apron2/30-autotune-stub.c index 2e47bb0547..e1b7603c3b 100644 --- a/tests/regression/46-apron2/30-autotune-stub.c +++ b/tests/regression/46-apron2/30-autotune-stub.c @@ -8,7 +8,7 @@ int main () { int y __attribute__((goblint_stub)); if( x < y) { - __goblint_check(x < y); //UNKNOWN! + __goblint_check(x < y); //UNKNOWN } return 0; From 370fc2eb931de53470d877206dd3b75eb222a27d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 14 Feb 2023 09:12:40 +0100 Subject: [PATCH 3/3] Pull out checks for `goblint_stub` --- src/autoTune.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 0e7210ea9b..c412af061a 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -243,9 +243,11 @@ let isComparison = function | Lt | Gt | Le | Ge | Ne | Eq -> true | _ -> false +let isGoblintStub v = List.exists (fun (Attr(s,_)) -> s = "goblint_stub") v.vattr + let rec extractVar = function | UnOp (Neg, e, _) -> extractVar e - | Lval ((Var info),_) when not (List.exists (fun (Attr(s,_)) -> s = "goblint_stub") info.vattr) -> Some info + | Lval ((Var info),_) when not (isGoblintStub info) -> Some info | _ -> None let extractOctagonVars = function @@ -283,7 +285,7 @@ class octagonVariableVisitor(varMap, globals) = object handle varMap 5 globals (extractOctagonVars e2) ; DoChildren ) - | Lval ((Var info),_) when not (List.exists (fun (Attr(s,_)) -> s = "goblint_stub") info.vattr) -> handle varMap 1 globals (Some (`Right info)) ; SkipChildren + | Lval ((Var info),_) when not (isGoblintStub info) -> handle varMap 1 globals (Some (`Right info)) ; SkipChildren (*Traverse down only operations fitting for linear equations*) | UnOp (Neg, _,_) | BinOp (PlusA,_,_,_)