From 861f881bf1c7536914995344d7644fe2ee5bbe3e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 25 May 2022 12:57:47 +0300 Subject: [PATCH 1/6] Hide mutex structure contents in base analysis --- src/cdomains/valueDomain.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index f6c7bfbbd6..48b0e99786 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -854,6 +854,7 @@ struct let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in let r = match x, offs with + | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *) | `Blob (x,s,orig), `Index (_,ofs) -> begin let l', o' = shift_one_over l o in From 73c4fce80d603f723b209a367dfb18c148902a3e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 25 May 2022 17:01:16 +0300 Subject: [PATCH 2/6] Use bot instead of top for base mutex contents This avoids unknown value escape warnings. --- src/cdomains/valueDomain.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 48b0e99786..66095d7aa6 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -133,7 +133,7 @@ struct let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *) match t with - | t when is_mutex_type t -> `Top + | t when is_mutex_type t -> `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *) | TInt (ik,_) -> `Int (ID.top_of ik) | TPtr _ -> `Address AD.top_ptr | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci) @@ -854,7 +854,8 @@ struct let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in let r = match x, offs with - | _, _ when is_mutex_type t -> `Top (* hide mutex structure contents, not updated anyway *) + | _, _ when is_mutex_type t -> (* hide mutex structure contents, not updated anyway *) + `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *) | `Blob (x,s,orig), `Index (_,ofs) -> begin let l', o' = shift_one_over l o in From 2f80c776c1bf5e6b6aa36dab21c3a0967d7e3698 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 26 Jul 2022 14:19:29 +0300 Subject: [PATCH 3/6] Add Mutex variant to ValueDomain --- src/analyses/base.ml | 2 ++ src/cdomains/valueDomain.ml | 31 ++++++++++++++++++++++++++----- 2 files changed, 28 insertions(+), 5 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index ebf55d14a8..99a00c1451 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -429,6 +429,7 @@ struct | `Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty | `Int _ -> empty | `Thread _ -> empty (* thread IDs are abstract and nothing known can be reached from them *) + | `Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *) (* Get the list of addresses accessable immediately from a given address, thus * all pointers within a structure should be considered, but we don't follow @@ -567,6 +568,7 @@ struct ValueDomain.Structs.fold f s (empty, TS.bot (), false) | `Int _ -> (empty, TS.bot (), false) | `Thread _ -> (empty, TS.bot (), false) (* TODO: is this right? *) + | `Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *) in reachable_from_value (get (Analyses.ask_of_ctx ctx) ctx.global ctx.local adr None) in diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 66095d7aa6..bdb010ecc7 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -78,6 +78,7 @@ module rec Compound: S with type t = [ | `Array of CArrays.t | `Blob of Blobs.t | `Thread of Threads.t + | `Mutex | `Bot ] and type offs = (fieldinfo,IndexDomain.t) Lval.offs = struct @@ -90,6 +91,7 @@ struct | `Array of CArrays.t | `Blob of Blobs.t | `Thread of Threads.t + | `Mutex | `Bot ] [@@deriving eq, ord, hash] @@ -106,6 +108,7 @@ struct let rec bot_value (t: typ): t = match t with + | _ when is_mutex_type t -> `Mutex | TInt _ -> `Bot (*`Int (ID.bot ()) -- should be lower than any int or address*) | TPtr _ -> `Address (AD.bot ()) | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> bot_value fd.ftype) ci) @@ -128,12 +131,13 @@ struct | `Array x -> CArrays.is_bot x | `Blob x -> Blobs.is_bot x | `Thread x -> Threads.is_bot x + | `Mutex -> false | `Bot -> true | `Top -> false let rec init_value (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *) match t with - | t when is_mutex_type t -> `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *) + | t when is_mutex_type t -> `Mutex | TInt (ik,_) -> `Int (ID.top_of ik) | TPtr _ -> `Address AD.top_ptr | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> init_value fd.ftype) ci) @@ -149,6 +153,7 @@ struct let rec top_value (t: typ): t = match t with + | _ when is_mutex_type t -> `Mutex | TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik))) | TPtr _ -> `Address AD.top_ptr | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> top_value fd.ftype) ci) @@ -170,11 +175,13 @@ struct | `Array x -> CArrays.is_top x | `Blob x -> Blobs.is_top x | `Thread x -> Threads.is_top x + | `Mutex -> false | `Top -> true | `Bot -> false let rec zero_init_value (t:typ): t = match t with + | _ when is_mutex_type t -> `Mutex | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero) | TPtr _ -> `Address AD.null_ptr | TComp ({cstruct=true; _} as ci,_) -> `Struct (Structs.create (fun fd -> zero_init_value fd.ftype) ci) @@ -198,7 +205,7 @@ struct | _ -> `Top let tag_name : t -> string = function - | `Top -> "Top" | `Int _ -> "Int" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Bot -> "Bot" + | `Top -> "Top" | `Int _ -> "Int" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `Bot -> "Bot" include Printable.Std let name () = "compound" @@ -222,6 +229,7 @@ struct | `Array n -> CArrays.pretty () n | `Blob n -> Blobs.pretty () n | `Thread n -> Threads.pretty () n + | `Mutex -> text "mutex" | `Bot -> text bot_name | `Top -> text top_name @@ -234,6 +242,7 @@ struct | `Array n -> CArrays.show n | `Blob n -> Blobs.show n | `Thread n -> Threads.show n + | `Mutex -> "mutex" | `Bot -> bot_name | `Top -> top_name @@ -342,7 +351,8 @@ struct (*if v = `Bot || (match torg with Some x -> is_safe_cast t x | None -> false) then v else*) match v with | `Bot - | `Thread _ -> + | `Thread _ + | `Mutex -> v | _ -> let log_top (_,l,_,_) = Messages.tracel "cast" "log_top at %d: %a to %a is top!\n" l pretty v d_type t in @@ -445,6 +455,7 @@ struct | (`Thread x, `Thread y) -> Threads.leq x y | (`Int x, `Thread y) -> true | (`Address x, `Thread y) -> true + | (`Mutex, `Mutex) -> true | _ -> warn_type "leq" x y; false let rec join x y = @@ -475,6 +486,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Thread y (* TODO: ignores address! *) + | (`Mutex, `Mutex) -> `Mutex | _ -> warn_type "join" x y; `Top @@ -509,6 +521,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Thread y (* TODO: ignores address! *) + | (`Mutex, `Mutex) -> `Mutex | _ -> warn_type "join" x y; `Top @@ -540,6 +553,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Thread y (* TODO: ignores address! *) + | (`Mutex, `Mutex) -> `Mutex | _ -> warn_type "widen" x y; `Top @@ -566,6 +580,7 @@ struct | (`Thread x, `Thread y) -> Threads.leq x y | (`Int x, `Thread y) -> true | (`Address x, `Thread y) -> true + | (`Mutex, `Mutex) -> true | _ -> warn_type "leq" x y; false let rec meet x y = @@ -589,6 +604,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Address x (* TODO: ignores thread! *) + | (`Mutex, `Mutex) -> `Mutex | _ -> warn_type "meet" x y; `Bot @@ -619,6 +635,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Thread y (* TODO: ignores address! *) + | (`Mutex, `Mutex) -> `Mutex | _ -> warn_type "widen" x y; `Top @@ -640,6 +657,7 @@ struct | (`Address x, `Thread y) | (`Thread y, `Address x) -> `Address x (* TODO: ignores thread! *) + | (`Mutex, `Mutex) -> `Mutex | x, `Top | `Top, x -> x | x, `Bot | `Bot, x -> `Bot | _ -> @@ -854,8 +872,8 @@ struct let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in let r = match x, offs with - | _, _ when is_mutex_type t -> (* hide mutex structure contents, not updated anyway *) - `Bot (* use `Bot instead of `Top to avoid unknown value escape warnings *) + | `Mutex, _ -> (* hide mutex structure contents, not updated anyway *) + `Mutex | `Blob (x,s,orig), `Index (_,ofs) -> begin let l', o' = shift_one_over l o in @@ -1056,6 +1074,7 @@ struct | `Array n -> CArrays.printXml f n | `Blob n -> Blobs.printXml f n | `Thread n -> Threads.printXml f n + | `Mutex -> BatPrintf.fprintf f "\n\nmutex\n\n\n" | `Bot -> BatPrintf.fprintf f "\n\nbottom\n\n\n" | `Top -> BatPrintf.fprintf f "\n\ntop\n\n\n" @@ -1067,6 +1086,7 @@ struct | `Array n -> CArrays.to_yojson n | `Blob n -> Blobs.to_yojson n | `Thread n -> Threads.to_yojson n + | `Mutex -> `String "mutex" | `Bot -> `String "⊥" | `Top -> `String "⊤" @@ -1081,6 +1101,7 @@ struct | `Array n -> `Array (project_arr p n) | `Blob (v, s, z) -> `Blob (project p v, ID.project p s, z) | `Thread n -> `Thread n + | `Mutex -> `Mutex | `Bot -> `Bot | `Top -> `Top and project_addr p a = From bdc1eec5883ff3819479e891d5305f5c39d96c4b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 26 Jul 2022 14:40:14 +0300 Subject: [PATCH 4/6] Add option to hide standard globals --- src/framework/control.ml | 9 ++++++++- src/util/options.schema.json | 6 ++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index b3b21caac1..06b93ac0f8 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -228,8 +228,15 @@ struct let set_bad v st = Spec.assign {ctx with local = st} (var v) MyCFG.unknown_exp in + let is_std = function + | {vname = ("__tzname" | "__daylight" | "__timezone"); _} (* unix time.h *) + | {vname = ("tzname" | "daylight" | "timezone"); _} (* unix time.h *) + | {vname = ("stdin" | "stdout" | "stderr"); _} -> (* standard stdio.h *) + true + | _ -> false + in let add_externs s = function - | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) -> set_bad v s + | GVarDecl (v,_) when not (VS.mem v vars || isFunctionType v.vtype) && not (get_bool "exp.hide-std-globals" && is_std v) -> set_bad v s | _ -> s in foldGlobals file add_externs (Spec.startstate MyCFG.dummy_func.svar) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index e27d2d60a4..00fbcdeb59 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1364,6 +1364,12 @@ "Sets the unrolling factor for the loopUnrollingVisitor.", "type": "integer", "default": 0 + }, + "hide-std-globals": { + "title": "exp.hide-std-globals", + "description": "Hide standard extern globals from cluttering local states, e.g. stdout.", + "type": "boolean", + "default": true } }, "additionalProperties": false From 45a0afcd19edc17c493933393c790887aeeeb88c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Jul 2022 12:45:55 +0300 Subject: [PATCH 5/6] Reword exp.hide-std-globals description Co-authored-by: Julian Erhard --- src/util/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 00fbcdeb59..b5e04f3e9a 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1367,7 +1367,7 @@ }, "hide-std-globals": { "title": "exp.hide-std-globals", - "description": "Hide standard extern globals from cluttering local states, e.g. stdout.", + "description": "Hide standard extern globals (e.g. `stdout`) from cluttering local states.", "type": "boolean", "default": true } From 422a5d6ebff7a11621ad4aba22bff42fa33829c4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Jul 2022 12:48:15 +0300 Subject: [PATCH 6/6] Adapt is_bot_value and is_top_value of ValueDomain Mutex to unit lattice --- src/cdomains/valueDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index bdb010ecc7..a049fb9f03 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -131,7 +131,7 @@ struct | `Array x -> CArrays.is_bot x | `Blob x -> Blobs.is_bot x | `Thread x -> Threads.is_bot x - | `Mutex -> false + | `Mutex -> true | `Bot -> true | `Top -> false @@ -175,7 +175,7 @@ struct | `Array x -> CArrays.is_top x | `Blob x -> Blobs.is_top x | `Thread x -> Threads.is_top x - | `Mutex -> false + | `Mutex -> true | `Top -> true | `Bot -> false