Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce Printable.Either3 #1279

Merged
merged 1 commit into from
Dec 4, 2023
Merged

Introduce Printable.Either3 #1279

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 12 additions & 15 deletions src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/commonPriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
34 changes: 34 additions & 0 deletions src/common/domains/printable.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
12 changes: 6 additions & 6 deletions src/framework/constraints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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) ->
Expand Down