C2PO: Adapt C2PO such that is does not read attributes from richvarinfo vars.

The C2PO analysis maps some varinfos to varinfos via the RichVarinfo module. The code used to read some attributes from these variables from the result varinfos.
Thus, it required a change where the all the attributes of resulting rich varinfos can be specified. With this change, this is no longer necessary.

Author: jerhard

src/analyses/basePriv.ml

@@ -1197,11 +1197,7 @@ struct
   (* sync: M -> (2^M -> (G -> D)) *)
   include AbstractLockCenteredBase (ThreadMap) (LockCenteredBase.CPA)
 
-  let global_init_thread () =
-    let v =  RichVarinfo.VarinfoDescription.empty "global_init"  in
-    let v = {v with vtype_=Some GoblintCil.voidType } in
-    RichVarinfo.create_var v
-
+  let global_init_thread = RichVarinfo.single ~name:"global_init" ~typ:GoblintCil.voidType
   let current_thread (ask: Q.ask): Thread.t =
     if !AnalysisState.global_initialization then
       ThreadIdDomain.Thread.threadinit (global_init_thread ()) ~multiple:false

src/analyses/wrapperFunctionAnalysis.ml

@@ -145,7 +145,7 @@ module MallocWrapper : MCPSpec = struct
       in
       Format.asprintf "(alloc@sid:%s%t%t)" (Node.show_id node) tid uniq_count
 
-    let varinfo_attributes x = RichVarinfo.VarinfoDescription.empty (name_varinfo x)
+    let typ _ = GoblintCil.voidType
   end
 
   module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)

src/cdomains/c2poDomain.ml

@@ -245,8 +245,7 @@ module D = struct
     if M.tracing then M.trace "c2po" "remove_terms_not_containing_variables: %s\n" (List.fold_left (fun s v -> s ^"; " ^Var.show v) "" vars);
     let not_global_and_not_contains_variable t =
       let var = T.get_var t in
-      let var = Var.to_varinfo var in
-      (not var.vglob) && not (T.contains_variable vars t)
+      not (DuplicateVars.VarType.vglob var) && not (T.contains_variable vars t)
     in
     remove_terms not_global_and_not_contains_variable cc
 

src/cdomains/duplicateVars.ml

@@ -47,6 +47,19 @@ module VarType = struct
 
     List.of_seq complete
 
+  (* Need to lookup attributes such as vaddrof in the original varinfo *)
+  let vaddrof : t -> bool = function
+    | AssignAux _
+    | ReturnAux _ -> false
+    | NormalVar v
+    | DuplicVar v -> v.vaddrof
+
+  let vglob : t -> bool = function
+    | AssignAux _
+    | ReturnAux _ -> false
+    | NormalVar v
+    | DuplicVar v -> v.vglob
+
   let duplic_var_prefix =
     "c2po__"
   let duplic_var_postfix =
@@ -76,18 +89,19 @@ module VarType = struct
     | ReturnAux _ -> true
     | _ -> false
 
-  let varinfo_attributes v =
-    let open RichVarinfo.VarinfoDescription in
+  let name_varinfo v =
     match v with
     | AssignAux t ->
-      ({(empty "AuxAssign") with vtype_=Some t})
+      "AuxAssign"
     | ReturnAux t ->
-      ({(empty "AuxReturn") with vtype_=Some t})
+      "AuxReturn"
     | NormalVar v ->
-      from_varinfo v
+      v.vname
     | DuplicVar v ->
-      let vname_ = duplic_var_prefix ^ string_of_int v.vid ^ duplic_var_postfix in
-      from_varinfo {v with vname = vname_}
+      duplic_var_prefix ^ string_of_int v.vid ^ duplic_var_postfix
+
+  let typ v =
+    get_type v
 
   (* Description that gets appended to the varinfo-name in user output. *)
   let describe_varinfo (var: varinfo) v =

src/cdomains/unionFind.ml

@@ -216,14 +216,15 @@ module T = struct
     let lval = Lval (var, NoOffset) in
     Aux (vinfo, lval)
 
-  let term_of_varinfo vinfo =
-    let var = Var.to_varinfo vinfo in
+  (*  *)
+  let term_of_varinfo var_type =
+    let var = Var.to_varinfo var_type in
     let lval = Lval (Var var, NoOffset) in
 
-    if is_struct_type var.vtype || var.vaddrof then
-      Deref (Addr vinfo, Z.zero, lval)
+    if is_struct_type var.vtype || DuplicateVars.VarType.vaddrof var_type then
+      Deref (Addr var_type, Z.zero, lval)
     else
-      aux_term_of_varinfo vinfo
+      aux_term_of_varinfo var_type
 
   (** From a offset, compute the index in bits *)
   let offset_to_index ?typ offset =

src/common/util/richVarinfo.ml

@@ -1,5 +1,12 @@
 open GoblintCil
 
+let create_var name typ = Cilfacade.create_var @@ makeGlobalVar name typ
+
+let single ~name ~typ =
+  let vi = lazy (create_var name typ) in
+  fun () ->
+    Lazy.force vi
+
 module type VarinfoMap =
 sig
   type t
@@ -10,78 +17,11 @@ sig
   val bindings: unit -> (t * varinfo) list
 end
 
-module VarinfoDescription = struct
-  (**This type is equal to `varinfo`, but the fields are not mutable and they are optional.
-     Only the name is not optional. *)
-  type t = {
-    vname_: string;
-    vtype_: typ option;
-    vattr_: attributes option;
-    vstorage_: storage option;
-    vglob_: bool option;
-    vinline_: bool option;
-    vdecl_: location option;
-    vinit_: initinfo option;
-    vaddrof_: bool option;
-    vreferenced_: bool option;
-  }
-
-  let from_varinfo (v: varinfo) =
-    {vname_=v.vname;
-     vtype_=Some v.vtype;
-     vattr_=Some v.vattr;
-     vstorage_=Some v.vstorage;
-     vglob_=Some v.vglob;
-     vinline_=Some v.vinline;
-     vdecl_=Some v.vdecl;
-     vinit_=Some v.vinit;
-     vaddrof_=Some v.vaddrof;
-     vreferenced_=Some v.vreferenced}
-
-  let empty name =
-    {vname_=name;
-     vtype_=None;
-     vattr_=None;
-     vstorage_=None;
-     vglob_=None;
-     vinline_=None;
-     vdecl_=None;
-     vinit_=None;
-     vaddrof_=None;
-     vreferenced_=None}
-
-  let update_varinfo (v: varinfo) (update: t) =
-    let open Batteries in
-    {vname=update.vname_;
-     vtype=Option.default v.vtype update.vtype_;
-     vattr=Option.default v.vattr update.vattr_;
-     vstorage=Option.default v.vstorage update.vstorage_;
-     vglob=Option.default v.vglob update.vglob_;
-     vinline=Option.default v.vinline update.vinline_;
-     vdecl=Option.default v.vdecl update.vdecl_;
-     vinit=Option.default v.vinit update.vinit_;
-     vid=v.vid;
-     vaddrof=Option.default v.vaddrof update.vaddrof_;
-     vreferenced=Option.default v.vreferenced update.vreferenced_;
-     vdescr=v.vdescr;
-     vdescrpure=v.vdescrpure;
-     vhasdeclinstruction=v.vhasdeclinstruction}
-end
-
-let create_var (vd: VarinfoDescription.t) =
-  Cilfacade.create_var (
-    VarinfoDescription.update_varinfo (makeGlobalVar vd.vname_ voidType) vd
-  )
-
-let single ~name =
-  let vi = lazy (create_var (VarinfoDescription.empty name)) in
-  fun () ->
-    Lazy.force vi
-
 module type G =
 sig
   include Hashtbl.HashedType
-  val varinfo_attributes: t -> VarinfoDescription.t
+  val name_varinfo: t -> string
+  val typ: t -> typ
 end
 
 module type H =
@@ -108,7 +48,7 @@ struct
     try
       XH.find !xh x
     with Not_found ->
-      let vi = create_var (X.varinfo_attributes x) in
+      let vi = create_var (X.name_varinfo x) (X.typ x) in
       store_f x vi;
       vi
 

src/common/util/richVarinfo.mli

@@ -2,6 +2,8 @@
 
 open GoblintCil
 
+val single: name:string -> typ:typ -> (unit -> varinfo)
+
 module type VarinfoMap =
 sig
   type t
@@ -12,32 +14,11 @@ sig
   val bindings: unit -> (t * varinfo) list
 end
 
-module VarinfoDescription:
-sig
-  type t = {
-    vname_: string;
-    vtype_: typ option;
-    vattr_: attributes option;
-    vstorage_: storage option;
-    vglob_: bool option;
-    vinline_: bool option;
-    vdecl_: location option;
-    vinit_: initinfo option;
-    vaddrof_: bool option;
-    vreferenced_: bool option;
-  }
-  val from_varinfo: varinfo -> t
-  val empty: string -> t
-  val update_varinfo: varinfo -> t -> varinfo
-end
-
-val create_var: VarinfoDescription.t -> varinfo
-val single: name:string -> (unit -> varinfo)
-
 module type G =
 sig
   include Hashtbl.HashedType
-  val varinfo_attributes: t -> VarinfoDescription.t
+  val name_varinfo: t -> string
+  val typ: t -> typ
 end
 
 module type H =

src/witness/witnessGhostVar.ml

@@ -5,7 +5,7 @@ type t =
   | Multithreaded
 [@@deriving eq, ord, hash]
 
-let show = function
+let name_varinfo = function
   | Locked (v, os) ->
     let name =
       if CilType.Varinfo.equal v LibraryFunctions.verifier_atomic_var then
@@ -25,9 +25,7 @@ let show = function
     name ^ offs os ^ "_locked"
   | Multithreaded -> "multithreaded"
 
-let varinfo_attributes l =
-  let name = show l in
-  RichVarinfo.VarinfoDescription.empty name
+let show = name_varinfo
 
 include Printable.SimpleShow (struct
     type nonrec t = t