From cb9dc2feafbf3e600e5bb1787ed97d9e448746da Mon Sep 17 00:00:00 2001 From: Rebecca Ghidini Date: Wed, 11 Sep 2024 14:02:37 +0200 Subject: [PATCH] modify richvarinfo to make it possible to change all the other fields of the resulting varinfo --- src/analyses/c2poAnalysis.ml | 5 +- src/analyses/wrapperFunctionAnalysis.ml | 2 + src/cdomains/c2poDomain.ml | 15 +++-- src/cdomains/duplicateVars.ml | 41 ++++++++----- src/common/util/richVarinfo.ml | 79 ++++++++++++++++++++++--- src/common/util/richVarinfo.mli | 25 +++++++- 6 files changed, 133 insertions(+), 34 deletions(-) diff --git a/src/analyses/c2poAnalysis.ml b/src/analyses/c2poAnalysis.ml index a886b6f8ed..aab439e024 100644 --- a/src/analyses/c2poAnalysis.ml +++ b/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 diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index eb9ec6ce02..94f1dbda86 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/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) diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml index ad486a2f73..0d5f5063c2 100644 --- a/src/cdomains/c2poDomain.ml +++ b/src/cdomains/c2poDomain.ml @@ -156,11 +156,18 @@ module D = struct | `Bot -> BatPrintf.fprintf f "\nbottom\n\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", diff --git a/src/cdomains/duplicateVars.ml b/src/cdomains/duplicateVars.ml index a70f98634c..492e8f9bf3 100644 --- a/src/cdomains/duplicateVars.ml +++ b/src/cdomains/duplicateVars.ml @@ -6,6 +6,7 @@ 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 @@ -13,12 +14,12 @@ open GoblintCil 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 diff --git a/src/common/util/richVarinfo.ml b/src/common/util/richVarinfo.ml index d1918c40a6..78e6f576e1 100644 --- a/src/common/util/richVarinfo.ml +++ b/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 diff --git a/src/common/util/richVarinfo.mli b/src/common/util/richVarinfo.mli index 4e682734ee..7847eccd85 100644 --- a/src/common/util/richVarinfo.mli +++ b/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 =