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.

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

Improve readability of global invariants #1294

Merged
merged 12 commits into from
Dec 20, 2023
2 changes: 1 addition & 1 deletion src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ struct

module G =
struct
include Lattice.Lift2 (Priv.G) (VD) (Printable.DefaultNames)
include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (Priv.G) (VD)

let priv = function
| `Bot -> Priv.G.bot ()
Expand Down
14 changes: 2 additions & 12 deletions src/analyses/basePriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -544,7 +544,7 @@ struct
)
)
else (
if ConcDomain.ThreadSet.is_top tids then
if ConcDomain.ThreadSet.is_top tids then
st
else
match ConcDomain.ThreadSet.elements tids with
Expand Down Expand Up @@ -660,21 +660,11 @@ struct
struct
include VarinfoV (* [g]' *)
let name () = "unprotected"
let show x = show x ^ ":unprotected" (* distinguishable variant names for html *)
include Printable.SimpleShow (struct
type nonrec t = t
let show = show
end)
end
module VProt =
struct
include VarinfoV (* [g] *)
let name () = "protected"
let show x = show x ^ ":protected" (* distinguishable variant names for html *)
include Printable.SimpleShow (struct
type nonrec t = t
let show = show
end)
end
module V =
struct
Expand Down Expand Up @@ -809,7 +799,7 @@ struct
struct
(* weak: G -> (2^M -> WeakRange) *)
(* sync: M -> (2^M -> SyncRange) *)
include Lattice.Lift2 (GWeak) (GSync) (Printable.DefaultNames)
include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GWeak) (GSync)

let weak = function
| `Bot -> GWeak.bot ()
Expand Down
8 changes: 3 additions & 5 deletions src/analyses/commonPriv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -74,18 +74,16 @@ struct
struct
include LockDomain.Addr
let name () = "mutex"
let show x = show x ^ ":mutex" (* distinguishable variant names for html *)
end
module VMutexInits = Printable.UnitConf (struct let name = "MUTEX_INITS" end)
module VGlobal =
struct
include VarinfoV
let name () = "global"
let show x = show x ^ ":global" (* distinguishable variant names for html *)
end
module V =
struct
include Printable.Either3 (VMutex) (VMutexInits) (VGlobal)
include Printable.Either3Conf (struct include Printable.DefaultConf let expand2 = false end) (VMutex) (VMutexInits) (VGlobal)
let name () = "MutexGlobals"
let mutex x: t = `Left x
let mutex_inits: t = `Middle ()
Expand Down Expand Up @@ -173,7 +171,7 @@ struct

module V =
struct
include Printable.Either (MutexGlobals.V) (TID)
include Printable.EitherConf (struct let expand1 = false let expand2 = true end) (MutexGlobals.V) (TID)
let mutex x = `Left (MutexGlobals.V.mutex x)
let mutex_inits = `Left MutexGlobals.V.mutex_inits
let global x = `Left (MutexGlobals.V.global x)
Expand All @@ -200,7 +198,7 @@ struct

module G =
struct
include Lattice.Lift2 (GMutex) (GThread) (Printable.DefaultNames)
include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GMutex) (GThread)

let mutex = function
| `Bot -> GMutex.bot ()
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/loopTermination.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ let check_bounded ctx varinfo =
(** We want to record termination information of loops and use the loop
* statements for that. We use this lifting because we need to have a
* lattice. *)
module Statements = Lattice.Flat (CilType.Stmt) (Printable.DefaultNames)
module Statements = Lattice.Flat (CilType.Stmt)

(** The termination analysis considering loops and gotos *)
module Spec : Analyses.MCPSpec =
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/mCPRegistry.ml
Original file line number Diff line number Diff line change
Expand Up @@ -426,7 +426,7 @@ end

module DomVariantLattice (DLSpec : DomainListLatticeSpec) =
struct
include Lattice.Lift (DomVariantLattice0 (DLSpec)) (Printable.DefaultNames)
include Lattice.LiftConf (struct include Printable.DefaultConf let expand1 = false end) (DomVariantLattice0 (DLSpec))
let name () = "MCP.G"
end

Expand Down
2 changes: 1 addition & 1 deletion src/analyses/mutexAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ struct

module G =
struct
include Lattice.Lift2 (GProtecting) (GProtected) (Printable.DefaultNames)
include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (GProtecting) (GProtected)

let protecting = function
| `Bot -> GProtecting.bot ()
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/raceAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ struct

module G =
struct
include Lattice.Lift2 (OffsetTrie) (MemoSet) (Printable.DefaultNames)
include Lattice.Lift2Conf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (OffsetTrie) (MemoSet)

let access = function
| `Bot -> OffsetTrie.bot ()
Expand Down
12 changes: 6 additions & 6 deletions src/analyses/symbLocks.ml
Original file line number Diff line number Diff line change
Expand Up @@ -106,20 +106,20 @@ struct

module A =
struct
module E = struct
include Printable.Either (CilType.Offset) (ILock)

let pretty () = function
| `Left o -> Pretty.dprintf "p-lock:%a" (d_offset (text "*")) o
| `Right addr -> Pretty.dprintf "i-lock:%a" ILock.pretty addr
module PLock =
struct
include CilType.Offset
let name () = "p-lock"

let pretty = d_offset (text "*")
include Printable.SimplePretty (
struct
type nonrec t = t
let pretty = pretty
end
)
end
module E = Printable.Either (PLock) (ILock)
include SetDomain.Make (E)

let name () = "symblock"
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/threadId.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ struct

module N =
struct
include Lattice.Flat (VNI) (struct let bot_name = "unknown node" let top_name = "unknown node" end)
include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "unknown node" let top_name = "unknown node" end) (VNI)
let name () = "wrapper call"
end
module TD = Thread.D
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/tutorials/signs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ end
* We then lift the above operations to the lattice. *)
module SL =
struct
include Lattice.Flat (Signs) (Printable.DefaultNames)
include Lattice.Flat (Signs)
let of_int i = `Lifted (Signs.of_int i)

let lt x y = match x, y with
Expand Down
5 changes: 3 additions & 2 deletions src/analyses/wrapperFunctionAnalysis0.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,8 @@ module ThreadCreateUniqueCount =
MakeUniqueCount (val unique_count_args_from_config "ana.thread.unique_thread_id_count")

(* since the query also references NodeFlatLattice, it also needs to reside here *)
module NodeFlatLattice = Lattice.Flat (Node) (struct
module NodeFlatLattice = Lattice.FlatConf (struct
include Printable.DefaultConf
let top_name = "Unknown node"
let bot_name = "Unreachable node"
end)
end) (Node)
10 changes: 6 additions & 4 deletions src/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1713,10 +1713,11 @@ end
module Flat (Base: IkindUnawareS) = (* identical to Lift, but goes to `Top/`Bot if Base raises Unknown/Error *)
struct
type int_t = Base.int_t
include Lattice.Flat (Base) (struct
include Lattice.FlatConf (struct
include Printable.DefaultConf
let top_name = "Unknown int"
let bot_name = "Error int"
end)
end) (Base)

let top_of ik = top ()
let bot_of ik = bot ()
Expand Down Expand Up @@ -1792,10 +1793,11 @@ end

module Lift (Base: IkindUnawareS) = (* identical to Flat, but does not go to `Top/Bot` if Base raises Unknown/Error *)
struct
include Lattice.LiftPO (Base) (struct
include Lattice.LiftPO (struct
include Printable.DefaultConf
let top_name = "MaxInt"
let bot_name = "MinInt"
end)
end) (Base)
type int_t = Base.int_t
let top_of ik = top ()
let bot_of ik = bot ()
Expand Down
2 changes: 1 addition & 1 deletion src/cdomains/mutexAttrDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ struct
end)
end

include Lattice.Flat(MutexKind) (struct let bot_name = "Uninitialized" let top_name = "Top" end)
include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "Uninitialized" let top_name = "Top" end) (MutexKind)

(* Needed because OS X is weird and assigns different constants than normal systems... :( *)
let recursive_int = lazy (
Expand Down
18 changes: 2 additions & 16 deletions src/cdomains/regionDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,23 +8,9 @@ module B = Printable.UnitConf (struct let name = "•" end)

module VFB =
struct
include Printable.Either (VF) (B)
include Printable.EitherConf (struct include Printable.DefaultConf let expand1 = false let expand2 = false end) (VF) (B)
let name () = "region"

let pretty () = function
| `Right () -> Pretty.text "•"
| `Left x -> VF.pretty () x

let show = function
| `Right () -> "•"
| `Left x -> VF.show x

let printXml f = function
| `Right () ->
BatPrintf.fprintf f "<value>\n<data>\n•\n</data>\n</value>\n"
| `Left x ->
BatPrintf.fprintf f "<value>\n<data>\n%a\n</data>\n</value>\n" VF.printXml x

let collapse (x:t) (y:t): bool =
match x,y with
| `Right (), `Right () -> true
Expand Down Expand Up @@ -252,4 +238,4 @@ struct
end

(* TODO: remove Lift *)
module RegionDom = Lattice.Lift (RegMap) (struct let top_name = "Unknown" let bot_name = "Error" end)
module RegionDom = Lattice.LiftConf (struct include Printable.DefaultConf let top_name = "Unknown" let bot_name = "Error" end) (RegMap)
2 changes: 1 addition & 1 deletion src/cdomains/stackDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ struct

module VarLat = Lattice.Fake (Basetype.Variables)

module Var = Lattice.Lift (VarLat) (struct let top_name="top" let bot_name="⊥" end)
module Var = Lattice.LiftConf (struct include Printable.DefaultConf let top_name="top" let bot_name="⊥" end) (VarLat)
include Lattice.Liszt (Var)

let top () : t = []
Expand Down
1 change: 1 addition & 0 deletions src/cdomains/symbLocksDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,7 @@ struct
end

include AddressDomain.AddressPrintable (Mval.MakePrintable (Offset.MakePrintable (Idx)))
let name () = "i-lock"

let rec conv_const_offset x =
match x with
Expand Down
6 changes: 4 additions & 2 deletions src/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -196,12 +196,14 @@ struct
end

module ThreadLiftNames = struct
include Printable.DefaultConf
let bot_name = "Bot Threads"
let top_name = "Top Threads"
let expand1 = false
end
module Lift (Thread: S) =
struct
include Lattice.Flat (Thread) (ThreadLiftNames)
include Lattice.FlatConf (ThreadLiftNames) (Thread)
let name () = "Thread"
end

Expand All @@ -217,7 +219,7 @@ struct
let name = "FlagConfiguredTID"
end)

module D = Lattice.Lift2(H.D)(P.D)(struct let bot_name = "bot" let top_name = "top" end)
module D = Lattice.Lift2 (H.D) (P.D)

let history_enabled () =
match GobConfig.get_string "ana.thread.domain" with
Expand Down
5 changes: 3 additions & 2 deletions src/cdomains/unionDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,11 @@ sig
end

module Field = struct
include Lattice.Flat (CilType.Fieldinfo) (struct
include Lattice.FlatConf (struct
include Printable.DefaultConf
let top_name = "Unknown field"
let bot_name = "If you see this, you are special!"
end)
end) (CilType.Fieldinfo)

let meet f g =
if equal f g then
Expand Down
Loading