Merge pull request #493 from goblint/annotations_via_options

Annotations via options

Author: michael-schwarz

src/analyses/base.ml

@@ -1100,8 +1100,8 @@ struct
     | `Struct _
     | `Union _ ->
       begin
-        let vars_in_paritioning = VD.affecting_vars value in
-        let dep_new = List.fold_left (fun dep var -> add_one_dep x var dep) st.deps vars_in_paritioning in
+        let vars_in_partitioning = VD.affecting_vars value in
+        let dep_new = List.fold_left (fun dep var -> add_one_dep x var dep) st.deps vars_in_partitioning in
         { st with deps = dep_new }
       end
     (* `List and `Blob cannot contain arrays *)
@@ -1282,7 +1282,7 @@ struct
     { st with cpa = List.fold_left f st.cpa v_list; deps = List.fold_left g st.deps v_list }
 
   (* Removes all partitionings done according to this variable *)
-  let rem_many_paritioning a (st:store) (v_list: varinfo list):store =
+  let rem_many_partitioning a (st:store) (v_list: varinfo list):store =
     (* Removes the partitioning information from all affected arrays, call before removing locals *)
     let rem_partitioning a (st:store) (x:varinfo):store =
       let affected_arrays =
@@ -1849,7 +1849,7 @@ struct
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | _ ->
       let locals = List.filter (fun v -> not (WeakUpdates.mem v st.weak)) (fundec.sformals @ fundec.slocals) in
-      let nst_part = rem_many_paritioning (Analyses.ask_of_ctx ctx) ctx.local locals in
+      let nst_part = rem_many_partitioning (Analyses.ask_of_ctx ctx) ctx.local locals in
       let nst: store = rem_many (Analyses.ask_of_ctx ctx) nst_part locals in
       match exp with
       | None -> nst

src/util/contextUtil.ml

@@ -1,6 +1,6 @@
 open Cil
 
-(** Definition of Goblint specific user defined C attributes **)
+(** Definition of Goblint specific user defined C attributes and their alternatives via options **)
 
 type attribute =
   | GobContext
@@ -19,10 +19,14 @@ let has_attribute s1 s2 al =
       | _ -> false
     ) al
 
+let has_option s1 s2 fd =
+  List.mem fd.svar.vname (GobConfig.get_string_list ("annotation." ^ s1 ^ "." ^ s2))
+
 let should_keep ~isAttr ~keepOption ~removeAttr ~keepAttr fd =
   let al = fd.svar.vattr in
   let s = attribute_to_string isAttr in
-  match GobConfig.get_bool keepOption, has_attribute s removeAttr al, has_attribute s keepAttr al with
+  let has_annot a = has_option s a fd || has_attribute s a al in
+  match GobConfig.get_bool keepOption, has_annot removeAttr, has_annot keepAttr with
   | _, true, true ->
     failwith (Printf.sprintf "ContextUtil.should_remove: conflicting context attributes %s and %s on %s" removeAttr keepAttr (CilType.Fundec.show fd))
   | _, false, true

src/util/defaults.ml

@@ -12,7 +12,7 @@ type category = Std             (** Parsing input, includes, standard stuff, etc
               | Incremental     (** Incremental features                          *)
               | Semantics       (** Semantics                                     *)
               | Transformations (** Transformations                               *)
-              | Annotation      (** Features for annotations                       *)
+              | Annotation      (** Features for annotations                      *)
               | Experimental    (** Experimental features of analyses             *)
               | Debugging       (** Debugging, tracing, etc.                      *)
               | Warnings        (** Filtering warnings                            *)
@@ -181,6 +181,24 @@ let _ = ()
 let _ = ()
       ; reg Annotation "annotation.int.enabled"   "false" "Enable manual annotation of functions with desired precision, i.e. the activated IntDomains."
       ; reg Annotation "annotation.int.privglobs" "true"  "Enables handling of privatized globals, by setting the precision to the heighest value, when annotation.int.enabled is true."
+      ; reg Annotation "annotation.goblint_context.base.no-non-ptr" "[]" ""
+      ; reg Annotation "annotation.goblint_context.base.non-ptr" "[]" ""
+      ; reg Annotation "annotation.goblint_context.base.no-int" "[]" ""
+      ; reg Annotation "annotation.goblint_context.base.int" "[]" ""
+      ; reg Annotation "annotation.goblint_context.base.no-interval" "[]" ""
+      ; reg Annotation "annotation.goblint_context.base.interval" "[]" ""
+      ; reg Annotation "annotation.goblint_context.apron.no-context" "[]" ""
+      ; reg Annotation "annotation.goblint_context.apron.context" "[]" ""
+      ; reg Annotation "annotation.goblint_context.no-widen" "[]" ""
+      ; reg Annotation "annotation.goblint_context.widen" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.no-def_exc" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.def_exc" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.no-interval" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.interval" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.no-enums" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.enums" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.no-congruence" "[]" ""
+      ; reg Annotation "annotation.goblint_precision.congruence" "[]" ""
 
 (* {4 category [Experimental]} *)
 let _ = ()

tests/regression/02-base/67-no-int-context-option.c

@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.interval --disable ana.context.widen --enable ana.base.context.int --set annotation.goblint_context.base.no-int[+] f
+#include <assert.h>
+
+int f(int x) {
+  if (x)
+    return f(x+1);
+  else
+    return x;
+}
+
+int main () {
+  int a = f(1);
+  assert(!a);
+  return 0;
+}

tests/regression/02-base/68-int-context-option.c

@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.interval --disable ana.context.widen --disable ana.base.context.int --set annotation.goblint_context.base.int[+] f
+#include <assert.h>
+
+int f(int x) {
+  if (x)
+    return x * f(x - 1);
+  else
+    return 1;
+}
+
+int main () {
+  int a = f(10);
+  assert(a == 3628800);
+  return 0;
+}

tests/regression/23-partitioned_arrays_last/01-simple_array.c

@@ -156,7 +156,7 @@ void example7(void) {
     assert(a[top] == 0); // UNKNOWN
 }
 
-// Check that the global variable is not used for paritioning
+// Check that the global variable is not used for partitioning
 void example8() {
     int a[10];
 

tests/regression/42-annotated-precision/01-def_exc.c

@@ -1,15 +1,18 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("def_exc", "interval"))) {
+int f(int in) __attribute__ ((goblint_precision("def_exc", "interval")));
+int main() __attribute__ ((goblint_precision("def_exc")));
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("def_exc"))) {
+int main() {
   int a = 0;
   assert(a); // FAIL!
   a = f(a);
   assert(a);
   return 0;
-}
+}

tests/regression/42-annotated-precision/02-interval.c

@@ -1,15 +1,18 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval"))) {
+int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval")));
+int main() __attribute__ ((goblint_precision("def_exc", "interval"))) ;
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("def_exc", "interval"))) {
+int main() {
   int a = 0;
   assert(a); // FAIL!
   a = f(a);
   assert(a);
   return 0;
-}
+}

tests/regression/42-annotated-precision/03-congruence.c

@@ -1,17 +1,20 @@
 // PARAM: --enable annotation.int.enabled --set ana.int.refinement fixpoint
 #include<assert.h>
 
-int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval"))) {
+int f(int in) __attribute__ ((goblint_precision("no-def_exc","interval")));
+int main() __attribute__ ((goblint_precision("no-def_exc","congruence")));
+
+int f(int in) {
   in++;
   return in;
 }
 
-int main() __attribute__ ((goblint_precision("no-def_exc","congruence"))) {
+int main() {
   int a = 0;
   int b = f(a);
   assert(b);
   a = b % 2;
   b = f(a);
   assert(b == 2);
   return 0;
-}
+}

tests/regression/42-annotated-precision/04-struct.c

@@ -6,12 +6,15 @@ struct a {
   int i;
 };
 
-void f(struct a *in) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence"))) {
+void f(struct a *in) __attribute__ ((goblint_precision("no-def_exc","interval", "congruence")));
+int main() __attribute__ ((goblint_precision("congruence")));
+
+void f(struct a *in) {
   in->i += 4;
   return;
 }
 
-int main() __attribute__ ((goblint_precision("congruence"))) {
+int main() {
   struct a a1, b1 = {"Jane", 3};
 
   a1.name = "John";
@@ -24,4 +27,4 @@ int main() __attribute__ ((goblint_precision("congruence"))) {
   b1.i = a1.i % 5;
   assert(b1.i); // FAIL!
   return 0;
-}
+}