Introduce Printable.Either3

src/analyses/basePriv.ml

@@ -211,12 +211,12 @@ struct
   let thread_join ?(force=false) ask get e st = st
   let thread_return ask get set tid st = st
 
-  let invariant_global getg g =
-    match g with
-    | `Left _ -> (* mutex *)
-      Invariant.none
+  let invariant_global getg = function
     | `Right g' -> (* global *)
       ValueDomain.invariant_global (read_unprotected_global getg) g'
+    | _ -> (* mutex *)
+      Invariant.none
+
 end
 
 module PerMutexOplusPriv: S =
@@ -625,13 +625,11 @@ struct
     let get_mutex_inits' = CPA.find x get_mutex_inits in
     VD.join get_mutex_global_x' get_mutex_inits'
 
-  let invariant_global getg g =
-    match g with
-    | `Left (`Left _) -> (* mutex *)
-      Invariant.none
-    | `Left (`Right g') -> (* global *)
-      ValueDomain.invariant_global (read_unprotected_global getg) g'
-    | `Right _ -> (* thread *)
+  let invariant_global getg = function
+    | `Middle  g -> (* global *)
+      ValueDomain.invariant_global (read_unprotected_global getg) g
+    | `Left _
+    | `Right _ -> (* mutex or thread *)
       Invariant.none
 end
 
@@ -847,16 +845,15 @@ struct
 
   open Locksets
 
-  let invariant_global getg g =
-    match g with
-    | `Left _ -> (* mutex *)
-      Invariant.none
+  let invariant_global getg = function
     | `Right g' -> (* global *)
       ValueDomain.invariant_global (fun x ->
           GWeak.fold (fun s' tm acc ->
               WeakRange.fold_weak VD.join tm acc
             ) (G.weak (getg (V.global x))) (VD.bot ())
         ) g'
+    | _ -> (* mutex *)
+      Invariant.none
 
   let invariant_vars ask getg st =
     let module VS = Set.Make (CilType.Varinfo) in

src/analyses/commonPriv.ml

@@ -85,11 +85,10 @@ struct
   end
   module V =
   struct
-    (* TODO: Either3? *)
-    include Printable.Either (struct include Printable.Either (VMutex) (VMutexInits) let name () = "mutex" end) (VGlobal)
+    include Printable.Either3 (VMutex) (VMutexInits) (VGlobal)
     let name () = "MutexGlobals"
-    let mutex x: t = `Left (`Left x)
-    let mutex_inits: t = `Left (`Right ())
+    let mutex x: t = `Left x
+    let mutex_inits: t = `Middle ()
     let global x: t = `Right x
   end
 

src/common/domains/printable.ml

@@ -273,6 +273,40 @@ struct
     | `Right x -> `Right (Base2.relift x)
 end
 
+module Either3 (Base1: S) (Base2: S) (Base3: S) =
+struct
+  type t = [`Left of Base1.t | `Middle of Base2.t | `Right of Base3.t] [@@deriving eq, ord, hash]
+  include Std
+
+  let pretty () (state:t) =
+    match state with
+    | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
+    | `Middle n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
+    | `Right n -> Pretty.dprintf "%s:%a" (Base3.name ()) Base3.pretty n
+
+  let show state =
+    match state with
+    | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
+    | `Middle n -> (Base2.name ()) ^ ":" ^ Base2.show n
+    | `Right n -> (Base3.name ()) ^ ":" ^ Base3.show n
+
+  let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name ()
+  let printXml f = function
+    | `Left x  -> BatPrintf.fprintf f "<value><map>\n<key>\nLeft\n</key>\n%a</map>\n</value>\n" Base1.printXml x
+    | `Middle x  -> BatPrintf.fprintf f "<value><map>\n<key>\nMiddle\n</key>\n%a</map>\n</value>\n" Base2.printXml x
+    | `Right x -> BatPrintf.fprintf f "<value><map>\n<key>\nRight\n</key>\n%a</map>\n</value>\n" Base3.printXml x
+
+  let to_yojson = function
+    | `Left x -> `Assoc [ Base1.name (), Base1.to_yojson x ]
+    | `Middle x -> `Assoc [ Base2.name (), Base2.to_yojson x ]
+    | `Right x -> `Assoc [ Base3.name (), Base3.to_yojson x ]
+
+  let relift = function
+    | `Left x -> `Left (Base1.relift x)
+    | `Middle x -> `Middle (Base2.relift x)
+    | `Right x -> `Right (Base3.relift x)
+end
+
 module Option (Base: S) (N: Name) =
 struct
   type t = Base.t option [@@deriving eq, ord, hash]

src/framework/constraints.ml

@@ -1467,14 +1467,14 @@ struct
 
   module V =
   struct
-    include Printable.Either (S.V) (Printable.Either (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C)))
+    include Printable.Either3 (S.V) (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C))
     let name () = "longjmp"
     let s x = `Left x
-    let longjmpto x = `Right (`Left x)
-    let longjmpret x = `Right (`Right x)
+    let longjmpto x = `Middle x
+    let longjmpret x = `Right x
     let is_write_only = function
       | `Left x -> S.V.is_write_only x
-      | `Right _ -> false
+      | _ -> false
   end
 
   module G =
@@ -1511,15 +1511,15 @@ struct
       begin match g with
         | `Left g ->
           S.query (conv ctx) (WarnGlobal (Obj.repr g))
-        | `Right g ->
+        | _ ->
           Queries.Result.top q
       end
     | InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       begin match g with
         | `Left g ->
           S.query (conv ctx) (InvariantGlobal (Obj.repr g))
-        | `Right g ->
+        | _ ->
           Queries.Result.top q
       end
     | IterSysVars (vq, vf) ->