From 1ecca1d218fd2a3b4353f8e01831e7a8f1f0a539 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Dec 2023 15:48:07 +0200 Subject: [PATCH] Add Lattice.Lift2Conf --- src/analyses/base.ml | 2 +- src/analyses/commonPriv.ml | 2 +- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/raceAnalysis.ml | 2 +- src/common/domains/printable.ml | 18 +++++++++++++----- src/domain/lattice.ml | 6 ++++-- 6 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 7cc937b201e..8c4bb67b0b1 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -54,7 +54,7 @@ struct module G = struct - include Lattice.Lift2 (Priv.G) (VD) (Printable.DefaultNames) + include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (Priv.G) (VD) (Printable.DefaultNames) let priv = function | `Bot -> Priv.G.bot () diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 0453862bc0d..1bf03581c26 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -198,7 +198,7 @@ struct module G = struct - include Lattice.Lift2 (GMutex) (GThread) (Printable.DefaultNames) + include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (GMutex) (GThread) (Printable.DefaultNames) let mutex = function | `Bot -> GMutex.bot () diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index ee050f55ca8..1b52f5dd40a 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -132,7 +132,7 @@ struct module G = struct - include Lattice.Lift2 (GProtecting) (GProtected) (Printable.DefaultNames) + include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (GProtecting) (GProtected) (Printable.DefaultNames) let protecting = function | `Bot -> GProtecting.bot () diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 9c2272fabb0..241bcb14f8f 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -194,7 +194,7 @@ struct module G = struct - include Lattice.Lift2 (OffsetTrie) (MemoSet) (Printable.DefaultNames) + include Lattice.Lift2Conf (struct let expand1 = false let expand2 = false end) (OffsetTrie) (MemoSet) (Printable.DefaultNames) let access = function | `Bot -> OffsetTrie.bot () diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 8311dd2ef0e..882cb30bf59 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -370,7 +370,7 @@ struct let relift = Option.map Base.relift end -module Lift2 (Base1: S) (Base2: S) (N: LiftingNames) = +module Lift2Conf (Conf: EitherConf) (Base1: S) (Base2: S) (N: LiftingNames) = struct type t = [`Bot | `Lifted1 of Base1.t | `Lifted2 of Base2.t | `Top] [@@deriving eq, ord, hash] include Std @@ -378,6 +378,7 @@ struct let pretty () (state:t) = match state with + (* TODO: expand *) | `Lifted1 n -> Base1.pretty () n | `Lifted2 n -> Base2.pretty () n | `Bot -> text bot_name @@ -385,6 +386,7 @@ struct let show state = match state with + (* TODO: expand *) | `Lifted1 n -> Base1.show n | `Lifted2 n -> Base2.show n | `Bot -> bot_name @@ -399,16 +401,22 @@ struct let printXml f = function | `Bot -> BatPrintf.fprintf f "\n\n%s\n\n\n" N.bot_name | `Top -> BatPrintf.fprintf f "\n\n%s\n\n\n" N.top_name - | `Lifted1 x -> BatPrintf.fprintf f "\n\n\nLifted1\n\n%a\n\n" Base1.printXml x - | `Lifted2 x -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\n" Base2.printXml x + | `Lifted1 x when Conf.expand1 -> BatPrintf.fprintf f "\n\n\nLifted1\n\n%a\n\n" Base1.printXml x + | `Lifted1 x -> Base1.printXml f x + | `Lifted2 x when Conf.expand2 -> BatPrintf.fprintf f "\n\n\nLifted2\n\n%a\n\n" Base2.printXml x + | `Lifted2 x -> Base2.printXml f x let to_yojson = function | `Bot -> `String N.bot_name | `Top -> `String N.top_name - | `Lifted1 x -> `Assoc [ Base1.name (), Base1.to_yojson x ] - | `Lifted2 x -> `Assoc [ Base2.name (), Base2.to_yojson x ] + | `Lifted1 x when Conf.expand1 -> `Assoc [ Base1.name (), Base1.to_yojson x ] + | `Lifted1 x -> Base1.to_yojson x + | `Lifted2 x when Conf.expand2 -> `Assoc [ Base2.name (), Base2.to_yojson x ] + | `Lifted2 x -> Base2.to_yojson x end +module Lift2 = Lift2Conf (struct let expand1 = true let expand2 = true end) + module type ProdConfiguration = sig val expand_fst: bool diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml index 9ea3f746350..448f801ec1e 100644 --- a/src/domain/lattice.ml +++ b/src/domain/lattice.ml @@ -336,9 +336,9 @@ struct | _ -> x end -module Lift2 (Base1: S) (Base2: S) (N: Printable.LiftingNames) = +module Lift2Conf (Conf: Printable.EitherConf) (Base1: S) (Base2: S) (N: Printable.LiftingNames) = struct - include Printable.Lift2 (Base1) (Base2) (N) + include Printable.Lift2Conf (Conf) (Base1) (Base2) (N) let bot () = `Bot let is_bot x = x = `Bot @@ -408,6 +408,8 @@ struct end +module Lift2 = Lift2Conf (struct let expand1 = true let expand2 = true end) + module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) = struct include Printable.ProdConf (C) (Base1) (Base2)