Skip to content

Extract generic Spec domain and context lifters #1692

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

Merged
merged 6 commits into from
Mar 4, 2025
Merged

Extract generic Spec domain and context lifters #1692

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
98f8157
Extract generic Spec.C lifter from HashconsContextLifter
sim642 Feb 19, 2025
e7a3412
Extract generic Spec.D lifter from HashconsLifter
sim642 Feb 19, 2025
9eeff41
Flip Lattice.HConsed arguments for convenient lifting
sim642 Feb 19, 2025
00c16c2
Merge branch 'master' into generic-spec-lifters
sim642 Feb 24, 2025
4fe5985
Make generic Spec domain and context lifter name configurable
sim642 Feb 24, 2025
91ca675
Move comments about hashcons in SpecLifters
sim642 Mar 3, 2025
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
2 changes: 1 addition & 1 deletion src/domain/lattice.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ struct
end

(* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) =
module HConsed (Arg: sig val assume_idempotent: bool end) (Base:S) =
struct
include Printable.HConsed (Base)

Expand Down
2 changes: 1 addition & 1 deletion src/domain/mapDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ module HConsed (M: S) : S with
type key = M.key and
type value = M.value =
struct
include Lattice.HConsed (M) (struct let assume_idempotent = false end)
include Lattice.HConsed (struct let assume_idempotent = false end) (M)

type key = M.key
type value = M.value
Expand Down
143 changes: 51 additions & 92 deletions src/lifters/specLifters.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,26 @@ open GoblintCil
open Analyses
open GobConfig

module type NameLifter =
sig
val lift_name: string -> string
end

(** Lifts a [Spec] so that the domain is [Hashcons]d *)
module HashconsLifter (S:Spec)
module type LatticeLifter =
functor (L: Lattice.S) ->
sig
include Lattice.S

val lift: L.t -> t
val unlift: t -> L.t
end

module DomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec)
: Spec with module G = S.G
and module C = S.C
=
struct
module HConsedArg =
struct
(* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
(* see https://github.com/goblint/analyzer/issues/1005 *)
let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
end
module D = Lattice.HConsed (S.D) (HConsedArg)
module D = F (S.D)
module G = S.G
module C = S.C
module V = S.V
Expand All @@ -28,9 +34,9 @@ struct
let of_elt x = of_elt (D.unlift x)
end

let name () = S.name () ^" hashconsed"
let name () = N.lift_name (S.name ())

type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
type marshal = S.marshal
let init = S.init
let finalize = S.finalize

Expand Down Expand Up @@ -98,104 +104,50 @@ struct
D.lift @@ S.event (conv man) e (conv oman)
end

(** Lifts a [Spec] so that the context is [Hashcons]d. *)
module HashconsContextLifter (S:Spec)
: Spec with module D = S.D
and module G = S.G
and module C = Printable.HConsed (S.C)
=
(** Lifts a [Spec] so that the domain is [Hashcons]d *)
module HashconsLifter (S: Spec) = (* keep functor eta-expanded to look up option when lifter is actually used *)
struct
module D = S.D
module G = S.G
module C = Printable.HConsed (S.C)
module V = S.V
module P = S.P

let name () = S.name () ^" context hashconsed"

type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
let init = S.init
let finalize = S.finalize

let startstate = S.startstate
let exitstate = S.exitstate
let morphstate = S.morphstate

let conv man =
{ man with context = (fun () -> C.unlift (man.context ())) }

let context man fd = C.lift % S.context (conv man) fd
let startcontext () = C.lift @@ S.startcontext ()

let sync man reason =
S.sync (conv man) reason

let query man (type a) (q: a Queries.t): a Queries.result =
match q with
| Queries.IterPrevVars f ->
let g i (n, c, j) e = f i (n, Obj.repr (C.lift (Obj.obj c)), j) e in
S.query (conv man) (Queries.IterPrevVars g)
| _ -> S.query (conv man) q

let assign man lv e =
S.assign (conv man) lv e

let vdecl man v =
S.vdecl (conv man) v

let branch man e tv =
S.branch (conv man) e tv

let body man f =
S.body (conv man) f

let return man r f =
S.return (conv man) r f

let asm man =
S.asm (conv man)

let skip man =
S.skip (conv man)

let enter man r f args =
S.enter (conv man) r f args

let special man r f args =
S.special (conv man) r f args
module NameLifter =
struct
let lift_name x = x ^ " hashconsed"
end

let combine_env man r fe f args fc es f_ask =
S.combine_env (conv man) r fe f args (Option.map C.unlift fc) es f_ask
module HConsedArg =
struct
(* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
(* see https://github.com/goblint/analyzer/issues/1005 *)
let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
end

let combine_assign man r fe f args fc es f_ask =
S.combine_assign (conv man) r fe f args (Option.map C.unlift fc) es f_ask
include DomainLifter (NameLifter) (Lattice.HConsed (HConsedArg)) (S)

let threadenter man ~multiple lval f args =
S.threadenter (conv man) ~multiple lval f args
(* TODO: should marshal hashcons table to avoid relift altogether? *)
end

let threadspawn man ~multiple lval f args fman =
S.threadspawn (conv man) ~multiple lval f args (conv fman)
module type PrintableLifter =
functor (P: Printable.S) ->
sig
include Printable.S

let paths_as_set man = S.paths_as_set (conv man)
let event man e oman = S.event (conv man) e (conv oman)
end
val lift: P.t -> t
val unlift: t -> P.t
end

(** Lifts a [Spec] so that the context is [HashCached]. *)
module HashCachedContextLifter (S:Spec)
module ContextLifter (N: NameLifter) (F: PrintableLifter) (S:Spec)
: Spec with module D = S.D
and module G = S.G
and module C = Printable.HashCached (S.C)
and module C = F (S.C)
=
struct
module D = S.D
module G = S.G
module C = Printable.HashCached (S.C)
module C = F (S.C)
module V = S.V
module P = S.P

let name () = S.name () ^" context hashcached"
let name () = N.lift_name (S.name ())

type marshal = S.marshal
type marshal = S.marshal
let init = S.init
let finalize = S.finalize

Expand Down Expand Up @@ -262,6 +214,13 @@ struct
let event man e oman = S.event (conv man) e (conv oman)
end

(** Lifts a [Spec] so that the context is [Hashcons]d. *)
module HashconsContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashconsed" end) (Printable.HConsed)
(* TODO: should marshal hashcons table to avoid relift altogether? *)

(** Lifts a [Spec] so that the context is [HashCached]. *)
module HashCachedContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashcached" end) (Printable.HashCached)

(* see option ana.opt.equal *)
module OptEqual (S: Spec) = struct
module D = struct include S.D let equal x y = x == y || equal x y end
Expand Down
Loading