Add Mutex variant to ValueDomain

Author: sim642

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

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 "<value>\n<data>\nmutex\n</data>\n</value>\n"
     | `Bot -> BatPrintf.fprintf f "<value>\n<data>\nbottom\n</data>\n</value>\n"
     | `Top -> BatPrintf.fprintf f "<value>\n<data>\ntop\n</data>\n</value>\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 =