Merge pull request #1834 from goblint/autotune-octagon-fun

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/cdomains/apron/relationDomain.apron.ml

@@ -81,11 +81,7 @@ struct
     | _ -> None
 end
 
-module type Tracked =
-sig
-  val type_tracked: typ -> bool
-  val varinfo_tracked: varinfo -> bool
-end
+module type Tracked = RelationCil.Tracked
 
 module type S2 =
 sig

src/cdomains/apron/sharedFunctions.apron.ml

@@ -518,20 +518,7 @@ sig
   val eval_interval : Queries.ask -> t -> Texpr1.t -> Z.t option * Z.t option
 end
 
-module Tracked: RelationDomain.Tracked =
-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)
-
-  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
+module Tracked = RelationCil.Tracked
 
 module AssertionModule (V: SV) (AD: AssertionRelS) (Arg: ConvertArg) =
 struct

src/goblint_lib.ml

@@ -455,6 +455,7 @@ module SparseVector = SparseVector
 module ListMatrix = ListMatrix
 module RatOps = RatOps
 
+module RelationCil = RelationCil
 module SharedFunctions = SharedFunctions
 module GobApron = GobApron
 

src/util/relationCil.ml

@@ -0,0 +1,40 @@
+(** CIL utilities for relational analyses. *)
+
+open GoblintCil
+
+module type Tracked =
+sig
+  val type_tracked: typ -> bool
+  val varinfo_tracked: varinfo -> bool
+end
+
+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.c

@@ -0,0 +1,14 @@
+// CRAM
+
+#include <pthread.h>
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  return 0;
+}

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

@@ -0,0 +1,10 @@
+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] 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
+    total lines: 5
+

tests/regression/29-svcomp/dune

@@ -18,3 +18,8 @@
 (cram
  (applies_to 36-svcomp-arch)
  (enabled_if %{read:../../util/multilibAvailable})) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html
+
+(cram
+ (alias runaprontest)
+ (applies_to 38-autotune-octagon-fun)
+ (enabled_if %{lib-available:apron}))