modify richvarinfo to make it possible to change all the other fields…

… of the resulting varinfo

src/analyses/c2poAnalysis.ml

@@ -73,7 +73,7 @@ struct
       t |> meet_conjs_opt [Equal (dummy_var, term, offset)] |>
       D.remove_may_equal_terms ask s lterm |>
       meet_conjs_opt [Equal (lterm, dummy_var, Z.zero)] |>
-      D.remove_terms_containing_variable @@ AssignAux lval_t
+      D.remove_terms_containing_aux_variable
     | _ -> (* this is impossible *) C2PODomain.top ()
 
   (** Assign Cil Lval to a right hand side that is already converted to
@@ -188,7 +188,8 @@ struct
   let remove_out_of_scope_vars t f =
     let local_vars = f.sformals @ f.slocals in
     let duplicated_vars = f.sformals in
-    D.remove_terms_containing_variables (ReturnAux (TVoid [])::Var.from_varinfo local_vars duplicated_vars) t
+    let t = D.remove_terms_containing_return_variable t in
+    D.remove_terms_containing_variables (Var.from_varinfo local_vars duplicated_vars) t
 
   let combine_env ctx var_opt expr f args t_context_opt t (ask: Queries.ask) =
     match ctx.local with

src/analyses/wrapperFunctionAnalysis.ml

@@ -144,6 +144,8 @@ module MallocWrapper : MCPSpec = struct
           Format.dprintf "@tid:%s" (ThreadLifted.show t)
       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)
   end
 
   module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)

src/cdomains/c2poDomain.ml

@@ -156,11 +156,18 @@ module D = struct
     | `Bot ->  BatPrintf.fprintf f "<value>\nbottom\n</value>\n"
 
   (** Remove terms from the data structure.
-      It removes all terms for which "var" is a subterm,
+      It removes all terms that contain an AssignAux variable,
       while maintaining all equalities about variables that are not being removed.*)
-  let remove_terms_containing_variable var cc =
-    if M.tracing then M.trace "c2po" "remove_terms_containing_variable: %s\n" (T.show (Addr var));
-    remove_terms (fun t -> Var.equal (T.get_var t) var) cc
+  let remove_terms_containing_aux_variable cc =
+    if M.tracing then M.trace "c2po" "remove_terms_containing_aux_variable\n";
+    remove_terms (fun t -> Var.is_assign_aux (T.get_var t)) cc
+
+  (** Remove terms from the data structure.
+      It removes all terms that contain an ReturnAux variable,
+      while maintaining all equalities about variables that are not being removed.*)
+  let remove_terms_containing_return_variable cc =
+    if M.tracing then M.trace "c2po" "remove_terms_containing_aux_variable\n";
+    remove_terms (fun t -> Var.is_return_aux (T.get_var t)) cc
 
   (** Remove terms from the data structure.
       It removes all terms which contain one of the "vars",

src/cdomains/duplicateVars.ml

@@ -6,19 +6,20 @@ open CilType
 open GoblintCil
 open Batteries
 open GoblintCil
+module M = Messages
 
 (** Variable Type used by the C-2PO  Analysis.
     It contains normal variables with a varinfo as well as auxiliary variables for
     assignment and return and duplicated variables for remembering the value of variables at the beginning of a function. *)
 module VarType = struct
   (* the hash/compare values should not depend on the type.
      But they have to be defined even though they are not used, for some reason.*)
-  let equal_typ _ _ = true
-  let hash_typ _ = 0
-  let compare_typ _ _ = 0
+  let equal_typ a b = Stdlib.compare a b = 0
+  let hash_typ x = Hashtbl.hash x
+  let compare_typ a b = Stdlib.compare a b
 
-  type t = AssignAux of (typ[@compare.ignore][@eq.ignore][@hash.ignore])
-         | ReturnAux of (typ[@compare.ignore][@eq.ignore][@hash.ignore])
+  type t = AssignAux of typ
+         | ReturnAux of typ
          | NormalVar of Varinfo.t
          | DuplicVar of Varinfo.t [@@deriving eq,ord,hash]
 
@@ -31,11 +32,20 @@ module VarType = struct
     | NormalVar v -> v.vname
     | DuplicVar v -> "c2po__" ^ v.vname ^ "'"
 
-  let name_varinfo v = match v with
-    | AssignAux t -> "AuxAssign"
-    | ReturnAux t -> "AuxReturn"
-    | NormalVar v -> string_of_int v.vid
-    | DuplicVar v -> "c2po__" ^ string_of_int v.vid ^ "'"
+  let get_type v = match v with
+    | AssignAux t | ReturnAux t -> t
+    | NormalVar v | DuplicVar v -> v.vtype
+
+  let is_assign_aux = function | AssignAux _ -> true | _ -> false
+  let is_return_aux = function | ReturnAux _ -> true | _ -> false
+
+  let varinfo_attributes v =
+    let open RichVarinfo.VarinfoDescription in
+    match v with
+    | AssignAux t -> ({(empty "AuxAssign") with vtype_=Some t})
+    | ReturnAux t -> ({(empty "AuxReturn") with vtype_=Some t})
+    | NormalVar v -> from_varinfo v
+    | DuplicVar v -> ({(from_varinfo v) with vname_="c2po__" ^ string_of_int v.vid ^ "'"})
 
   (* Description that gets appended to the varinfo-name in user output. *)
   let describe_varinfo (var: varinfo) v =
@@ -49,11 +59,10 @@ struct
   include VarType
   let dummy_varinfo typ: varinfo = VarVarinfoMap.to_varinfo (AssignAux typ)
   let return_varinfo typ = VarVarinfoMap.to_varinfo (ReturnAux typ)
-  let to_varinfo v = let var = VarVarinfoMap.to_varinfo v in
-    match v with
-    | AssignAux t -> {var with vtype = t}
-    | ReturnAux t -> {var with vtype = t}
-    | NormalVar v -> v
-    | DuplicVar v -> {v with vid = var.vid}
+  let to_varinfo v =
+    let res = VarVarinfoMap.to_varinfo v in
+    if M.tracing then M.trace "c2po-varinfo" "to_varinfo: %a -> %a" d_type (get_type v) d_type res.vtype;
+    res
+
 
 end

src/common/util/richVarinfo.ml

@@ -1,12 +1,5 @@
 open GoblintCil
 
-let create_var name = Cilfacade.create_var @@ makeGlobalVar name voidType
-
-let single ~name =
-  let vi = lazy (create_var name) in
-  fun () ->
-    Lazy.force vi
-
 module type VarinfoMap =
 sig
   type t
@@ -17,10 +10,78 @@ 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 name_varinfo: t -> string
+  val varinfo_attributes: t -> VarinfoDescription.t
 end
 
 module type H =
@@ -47,7 +108,7 @@ struct
     try
       XH.find !xh x
     with Not_found ->
-      let vi = create_var (X.name_varinfo x) in
+      let vi = create_var (X.varinfo_attributes x) in
       store_f x vi;
       vi
 

src/common/util/richVarinfo.mli

@@ -2,8 +2,6 @@
 
 open GoblintCil
 
-val single: name:string -> (unit -> varinfo)
-
 module type VarinfoMap =
 sig
   type t
@@ -14,10 +12,31 @@ 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 single: name:string -> (unit -> varinfo)
+
 module type G =
 sig
   include Hashtbl.HashedType
-  val name_varinfo: t -> string
+  val varinfo_attributes: t -> VarinfoDescription.t
 end
 
 module type H =