Introduce attribute goblint_stub for variables to prevent tracking …

…it relationally

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)

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,_,_,_)

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 <goblint.h>
+
+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;
+}