Fix octagon autotuner choosing non-integer variables

Author: sim642

src/autoTune.ml

@@ -334,17 +334,16 @@ type option = {
 (*Option for activating the octagon apron domain on selected vars*)
 module VariableMap = Map.Make(CilType.Varinfo)
 module VariableSet = Set.Make(CilType.Varinfo)
+module OctagonTracked = RelationCil.AutotuneTracked
 
 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, _)
   | CastE (_, e) -> extractVar e
-  | Lval ((Var info),_) when not (isGoblintStub info) -> Some info
+  | Lval ((Var info),_) when OctagonTracked.varinfo_tracked info -> Some info
   | _ -> None
 
 let extractBinOpVars e1 e2 =
@@ -376,7 +375,7 @@ class octagonVariableVisitor(varMap, globals) = object
         List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e2);
         DoChildren
       )
-    | Lval ((Var info),_) when not (isGoblintStub info) -> addOrCreateVarMapping varMap info 1 globals; SkipChildren
+    | Lval ((Var info),_) when OctagonTracked.varinfo_tracked info -> addOrCreateVarMapping varMap info 1 globals; SkipChildren
     (*Traverse down only operations fitting for linear equations*)
     | UnOp (LNot, _,_)
     | UnOp (Neg, _,_)

src/util/relationCil.ml

@@ -8,17 +8,33 @@ sig
   val varinfo_tracked: varinfo -> bool
 end
 
-module Tracked: Tracked =
+module TypeTracked =
 struct
   let is_pthread_int_type = function
     | TNamed ({tname = ("pthread_t" | "pthread_key_t" | "pthread_once_t" | "pthread_spinlock_t"); _}, _) -> true (* on Linux these pthread types are integral *)
     | _ -> false
 
   let type_tracked typ =
     isIntegralType typ && not (is_pthread_int_type typ)
+end
+
+(** To be used in relational analyses. *)
+module Tracked: Tracked =
+struct
+  include TypeTracked
 
   let varinfo_tracked vi =
     (* no vglob check here, because globals are allowed in relation, but just have to be handled separately *)
     let hasTrackAttribute = List.exists (fun (Attr(s,_)) -> s = "goblint_relation_track") in
     type_tracked vi.vtype && (not @@ GobConfig.get_bool "annotation.goblint_relation_track" || hasTrackAttribute vi.vattr)
 end
+
+(** To be used in autotuner. *)
+module AutotuneTracked: Tracked =
+struct
+  include TypeTracked
+
+  let isGoblintStub v = List.exists (fun (Attr(s,_)) -> s = "goblint_stub") v.vattr
+
+  let varinfo_tracked vi = type_tracked vi.vtype && not (isGoblintStub vi) (* must not check for goblint_relation_track because the autotuner wants to add them based on this *)
+end

tests/regression/29-svcomp/38-autotune-octagon-fun.t

@@ -1,8 +1,8 @@
-TODO: Should not annotate functions for octagon.
+Should not annotate functions for octagon.
 
   $ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagon 38-autotune-octagon-fun.c
   [Info] Enabled octagon domain ONLY for:
-  [Info] pthread_create, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r
+  [Info] i, count, tmp, count, i, j, i___0, j___0, k, size, r
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 5
     dead: 0