Autotuning of Configuration

docs/user-guide/annotating.md

@@ -26,6 +26,30 @@ The following string arguments are supported:
 4. `apron.context`/`apron.no-context` to override the `ana.apron.context` option.
 5. `widen`/`no-widen` to override the `ana.context.widen` option.
 
+### Apron attributes
+The Apron library can be set to only track variables with the attribute `goblint_apron_track`
+
+### Array attributes
+Arrays can be annotated with the domain that should be used for it ("unroll", "partitioned", or "trivial"):
+
+```c
+int x[4] __attribute__((goblint_array_domain("unroll")));
+__attribute__((goblint_array_domain("trivial"))) int x[4];
+
+struct array {
+	int arr[5] __attribute__((goblint_array_domain("partitioned")));
+};
+```
+It is also possible to annotate a type, so that all arrays of this type without an own attribute will use this one: 
+
+```c
+typedef int unrollInt __attribute__((goblint_array_domain("trivial")));
+unrollInt x[4];
+```
+
+One can also annotate pointer parameters. Inside the function of the parameter, Goblint tries to use the annotated domain for the arrays pointed at by that pointer. This is not guaranteed to work, as following the pointers is done only in the first analyzed function context.
+
+
 
 ## Functions
 Goblint-specific functions can be called in the code, where they assist the analyzer but have no runtime effect.

src/analyses/apron/apronAnalysis.apron.ml

@@ -147,6 +147,7 @@ struct
       )
       else (
         let v_out = Goblintutil.create_var @@ makeVarinfo false (v.vname ^ "#out") v.vtype in (* temporary local g#out for global g *)
+        v_out.vattr <- v.vattr; (*copy the attributes because the tracking may depend on them. Otherwise an assertion fails *)
         let st = {st with apr = AD.add_vars st.apr [V.local v_out]} in (* add temporary g#out *)
         let st' = {st with apr = f st v_out} in (* g#out = e; *)
         if M.tracing then M.trace "apron" "write_global %a %a\n" d_varinfo v d_varinfo v_out;

src/analyses/base.ml

@@ -87,14 +87,50 @@ struct
 
   let is_privglob v = GobConfig.get_bool "annotation.int.privglobs" && v.vglob
 
-  let project_val p_opt value is_glob =
-    match GobConfig.get_bool "annotation.int.enabled", is_glob, p_opt with
-    | true, true, _ -> VD.project PU.max_int_precision value
-    | true, false, Some p -> VD.project p value
-    | _ -> value
+  (*This is a bit of a hack to be able to change array domains if a pointer to an array is given as an argument*)
+  (*We have to prevent different domains to be used at the same time for the same array*)
+  (*After a function call, the domain has to be the same as before and we can not depend on the pointers staying the same*)
+  (*-> we determine the arrays a pointer can point to once at the beginning of a function*)
+  (*There surely is a better way, because this means that often the wrong one gets chosen*)
+  module VarH = Hashtbl.Make(CilType.Varinfo)
+  module VarMap = Map.Make(CilType.Varinfo)
+  let array_map = VarH.create 20
+
+  let add_to_array_map fundec arguments =
+    let rec pointedArrayMap = function
+      | [] -> VarMap.empty
+      | (info,value)::xs -> (
+        match value with
+          | `Address t when hasAttribute "goblint_array_domain" info.vattr -> (
+            let possibleVars = PreValueDomain.AD.to_var_may t in
+            List.fold_left (fun map arr -> VarMap.add arr (info.vattr) map) (pointedArrayMap xs) @@ List.filter (fun info -> isArrayType info.vtype) possibleVars
+          )
+          | _ -> pointedArrayMap xs
+      )
+    in
+    match VarH.find_option array_map fundec.svar with
+    | Some _ -> () (*We already have something -> do not change it*)
+    | None -> VarH.add array_map fundec.svar (pointedArrayMap arguments)
+
+  let attributes_varinfo info fundec =
+    let map = VarH.find array_map fundec.svar in
+    match VarMap.find_opt info map with
+    | Some attr ->  Some (attr, typeAttrs (info.vtype)) (*if the function has a different domain for this array, use it*)
+    | None -> Some (info.vattr, typeAttrs (info.vtype))
+
+  let project_val ask array_attr p_opt value is_glob =
+    let p = if GobConfig.get_bool "annotation.int.enabled" then (
+        if is_glob then
+          Some PU.max_int_precision
+        else p_opt
+      ) else None
+    in
+    let a = if GobConfig.get_bool "annotation.goblint_array_domain" then array_attr else None in
+    VD.project ask p a value
 
-  let project p_opt cpa =
-    CPA.mapi (fun varinfo value -> project_val p_opt value (is_privglob varinfo)) cpa
+  let project ask p_opt cpa fundec =
+    CPA.mapi (fun varinfo value -> project_val ask (attributes_varinfo varinfo fundec) p_opt value (is_privglob varinfo))
+    cpa
 
 
   (**************************************************************************
@@ -120,7 +156,8 @@ struct
     Priv.init ()
 
   let finalize () =
-    Priv.finalize ()
+    Priv.finalize ();
+    VarH.clear array_map
 
   (**************************************************************************
    * Abstract evaluation functions
@@ -1298,7 +1335,7 @@ struct
 
   let update_variable variable typ value cpa =
     if ((get_bool "exp.volatiles_are_top") && (is_always_unknown variable)) then
-      CPA.add variable (VD.top_value typ) cpa
+      CPA.add variable (VD.top_value ~varAttr:variable.vattr typ) cpa
     else
       CPA.add variable value cpa
 
@@ -1355,8 +1392,8 @@ struct
               lval_type
       in
       let update_offset old_value =
-        (* Projection to highest Precision *)
-        let projected_value = project_val None value (is_global a x) in
+        (* Projection globals to highest Precision *)
+        let projected_value = project_val a None None value (is_global a x) in
         let new_value = VD.update_offset a old_value offs projected_value lval_raw ((Var x), cil_offset) t in
         if WeakUpdates.mem x st.weak then
           VD.join old_value new_value
@@ -1384,7 +1421,7 @@ struct
            The case when invariant = true requires the old_value to be sound for the meet.
            Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *)
         let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsHeapVar x)) && offs = `NoOffset then begin
-            VD.bot_value lval_type
+            VD.bot_value ~varAttr:x.vattr lval_type
           end else
             Priv.read_global a priv_getg st x
         in
@@ -2166,7 +2203,7 @@ struct
           begin match Addr.to_var_offset (AD.choose lval_val) with
             | Some (x,offs) ->
               let t = v.vtype in
-              let iv = VD.bot_value t in (* correct bottom value for top level variable *)
+              let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *)
               if M.tracing then M.tracel "set" "init bot value: %a\n" VD.pretty iv;
               let nv = VD.update_offset (Analyses.ask_of_ctx ctx) iv offs rval_val (Some  (Lval lval)) lval t in (* do desired update to value *)
               set_savetop ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.from_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *)
@@ -2227,7 +2264,7 @@ struct
 
   let body ctx f =
     (* First we create a variable-initvalue pair for each variable *)
-    let init_var v = (AD.from_var v, v.vtype, VD.init_value v.vtype) in
+    let init_var v = (AD.from_var v, v.vtype, VD.init_value ~varAttr:v.vattr v.vtype) in
     (* Apply it to all the locals and then assign them all *)
     let inits = List.map init_var f.slocals in
     set_many ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local inits
@@ -2350,6 +2387,7 @@ struct
     in
     (* Assign parameters to arguments *)
     let pa = GobList.combine_short fundec.sformals vals in (* TODO: is it right to ignore missing formals/args? *)
+    add_to_array_map fundec pa;
     let new_cpa = CPA.add_list pa st'.cpa in
     (* List of reachable variables *)
     let reachable = List.concat_map AD.to_var_may (reachable_vars (Analyses.ask_of_ctx ctx) (get_ptrs vals) ctx.global st) in
@@ -2358,7 +2396,7 @@ struct
 
     (* Projection to Precision of the Callee *)
     let p = PU.int_precision_from_fundec fundec in
-    let new_cpa = project (Some p) new_cpa in
+    let new_cpa = project (Analyses.ask_of_ctx ctx) (Some p) new_cpa fundec in
 
     (* Identify locals of this fundec for which an outer copy (from a call down the callstack) is reachable *)
     let reachable_other_copies = List.filter (fun v -> match Cilfacade.find_scope_fundec v with Some scope -> CilType.Fundec.equal scope fundec | None -> false) reachable in
@@ -2720,9 +2758,13 @@ struct
       let nst = add_globals st fun_st in
 
       (* Projection to Precision of the Caller *)
-      let p = PrecisionUtil.int_precision_from_node () in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
-      let return_val = project_val (Some p) return_val (is_privglob (return_varinfo ())) in
-      let cpa' = project (Some p) nst.cpa in
+      let p = PrecisionUtil.int_precision_from_node ()in (* Since f is the fundec of the Callee we have to get the fundec of the current Node instead *)
+      let callerFundec = match !MyCFG.current_node with
+      | Some n -> Node.find_fundec n
+      | None -> failwith "callerfundec not found"
+      in
+      let return_val = project_val (Analyses.ask_of_ctx ctx) (attributes_varinfo (return_varinfo ()) callerFundec) (Some p) return_val (is_privglob (return_varinfo ())) in
+      let cpa' = project (Analyses.ask_of_ctx ctx) (Some p) nst.cpa callerFundec in
 
       let st = { nst with cpa = cpa'; weak = st.weak } in (* keep weak from caller *)
       match lval with