From 442c8e92f40c619b0c0df02623b7bf38adabe6dc Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 8 Oct 2019 06:24:48 -0700 Subject: [PATCH] [sledge] Distinguish program expressions and formula terms Summary: There are a number if issues with using the same type for expressions in code and in formulas. One is that the type systems of the two should be different. Another is that conflating the two compromises the ability of Llair to correctly express aspects such as integer overflow, floating point rounding, etc. Also, it could be beneficial to have more source locations for program expressions than makes sense for terms. This diff simply unshares Exp, leading to a copy named Term. Likewise, Reg is now a copy of Var. Simplifications to come. Reviewed By: bennostein Differential Revision: D17665250 fbshipit-source-id: 4359a80d5 --- sledge/src/control.ml | 54 +- sledge/src/control.mli | 4 +- sledge/src/domain/domain_sig.ml | 22 +- sledge/src/domain/relation.ml | 10 +- sledge/src/domain/relation.mli | 4 +- sledge/src/domain/unit.ml | 4 +- sledge/src/domain/used_globals.ml | 18 +- sledge/src/domain/used_globals.mli | 2 +- sledge/src/llair/exp.ml | 62 +- sledge/src/llair/exp.mli | 30 +- sledge/src/llair/frontend.ml | 43 +- sledge/src/llair/global.ml | 18 +- sledge/src/llair/global.mli | 4 +- sledge/src/llair/llair.ml | 68 +- sledge/src/llair/llair.mli | 42 +- sledge/src/llair/reg.ml | 10 + sledge/src/llair/reg.mli | 10 + sledge/src/report.ml | 4 +- sledge/src/sledge.ml | 8 +- sledge/src/symbheap/equality.ml | 118 +- sledge/src/symbheap/equality.mli | 26 +- sledge/src/symbheap/equality_test.ml | 56 +- sledge/src/symbheap/exec.ml | 218 +-- sledge/src/symbheap/exec.mli | 6 +- sledge/src/symbheap/sh.ml | 78 +- sledge/src/symbheap/sh.mli | 12 +- sledge/src/symbheap/sh_domain.ml | 91 +- sledge/src/symbheap/sh_domain.mli | 6 +- sledge/src/symbheap/sh_test.ml | 8 +- sledge/src/symbheap/solver.ml | 212 +-- sledge/src/symbheap/solver_test.ml | 34 +- sledge/src/symbheap/term.ml | 1465 +++++++++++++++++ sledge/src/symbheap/term.mli | 219 +++ .../exp_test.ml => symbheap/term_test.ml} | 80 +- .../exp_test.mli => symbheap/term_test.mli} | 0 sledge/src/{llair => symbheap}/var.ml | 2 +- sledge/src/{llair => symbheap}/var.mli | 2 +- 37 files changed, 2402 insertions(+), 648 deletions(-) create mode 100644 sledge/src/llair/reg.ml create mode 100644 sledge/src/llair/reg.mli create mode 100644 sledge/src/symbheap/term.ml create mode 100644 sledge/src/symbheap/term.mli rename sledge/src/{llair/exp_test.ml => symbheap/term_test.ml} (81%) rename sledge/src/{llair/exp_test.mli => symbheap/term_test.mli} (100%) rename sledge/src/{llair => symbheap}/var.ml (92%) rename sledge/src/{llair => symbheap}/var.mli (86%) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index d7780af7c..0246ab7b9 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -13,7 +13,7 @@ type exec_opts = { bound: int ; skip_throw: bool ; function_summaries: bool - ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t] + ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t] } module Make (Dom : Domain_sig.Dom) = struct @@ -31,15 +31,15 @@ module Make (Dom : Domain_sig.Dom) = struct val pop_throw : t -> init:'a - -> unwind:(Var.t list -> Var.Set.t -> Dom.from_call -> 'a -> 'a) + -> unwind:(Reg.t list -> Reg.Set.t -> Dom.from_call -> 'a -> 'a) -> (Dom.from_call * Llair.jump * t * 'a) option end = struct type t = | Return of { recursive: bool (** return from a possibly-recursive call *) ; dst: Llair.Jump.t - ; params: Var.t list - ; locals: Var.Set.t + ; params: Reg.t list + ; locals: Reg.Set.t ; from_call: Dom.from_call ; stk: t } | Throw of Llair.Jump.t * t @@ -248,9 +248,9 @@ module Make (Dom : Domain_sig.Dom) = struct | None -> [%Trace.info "queue empty"] ; () end - let used_globals : exec_opts -> Var.var -> Var.Set.t = + let used_globals : exec_opts -> Reg.reg -> Reg.Set.t = fun opts fn -> - [%Trace.call fun {pf} -> pf "%a" Var.pp fn] + [%Trace.call fun {pf} -> pf "%a" Reg.pp fn] ; ( match opts.globals with | `Declared set -> set @@ -261,21 +261,21 @@ module Make (Dom : Domain_sig.Dom) = struct fail "main analysis reached function %a that was not reached by \ used-globals pre-analysis " - Var.pp fn () ) ) + Reg.pp fn () ) ) |> - [%Trace.retn fun {pf} r -> pf "%a" Var.Set.pp r] + [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r] let exec_jump stk state block Llair.{dst; retreating} = Work.add ~prev:block ~retreating stk state dst - let summary_table = Hashtbl.create (module Var) + let summary_table = Hashtbl.create (module Reg) let exec_call opts stk state block call globals = let Llair.{callee; args; areturn; return; recursive} = call in let Llair.{name; params; freturn; locals; entry} = callee in [%Trace.call fun {pf} -> - pf "%a from %a with state %a" Var.pp name.var Var.pp - return.dst.parent.name.var Dom.pp state] + pf "%a from %a with state %a" Reg.pp name.reg Reg.pp + return.dst.parent.name.reg Dom.pp state] ; let dnf_states = if opts.function_summaries then Dom.dnf state else [state] @@ -290,7 +290,7 @@ module Make (Dom : Domain_sig.Dom) = struct else let maybe_summary_post = let state = fst (domain_call ~summaries:false state) in - Hashtbl.find summary_table name.var + Hashtbl.find summary_table name.reg >>= List.find_map ~f:(Dom.apply_summary state) in [%Trace.info @@ -320,23 +320,23 @@ module Make (Dom : Domain_sig.Dom) = struct [%Trace.printf "@[%t@]" (fun fs -> Hashtbl.iteri summary_table ~f:(fun ~key ~data -> - Format.fprintf fs "@[%a:@ @[%a@]@]@ " Var.pp key + Format.fprintf fs "@[%a:@ @[%a@]@]@ " Reg.pp key (List.pp "@," Dom.pp_summary) data ) )] let exec_return ~opts stk pre_state (block : Llair.block) exp = let Llair.{name; params; freturn; locals} = block.parent in [%Trace.call fun {pf} -> - pf "from %a with pre_state %a" Var.pp name.var Dom.pp pre_state] + pf "from %a with pre_state %a" Reg.pp name.reg Dom.pp pre_state] ; let summarize post_state = if opts.function_summaries then ( - let globals = used_globals opts name.var in + let globals = used_globals opts name.reg in let function_summary, post_state = Dom.create_summary ~locals post_state - ~formals:(Set.union (Var.Set.of_list params) globals) + ~formals:(Set.union (Reg.Set.of_list params) globals) in - Hashtbl.add_multi summary_table ~key:name.var ~data:function_summary ; + Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ; pp_st () ; post_state ) else post_state @@ -359,7 +359,7 @@ module Make (Dom : Domain_sig.Dom) = struct opts.function_summaries && List.exists (Config.find_list "entry-points") - ~f:(String.equal (Var.name name.var)) + ~f:(String.equal (Reg.name name.reg)) then summarize exit_state |> (ignore : Dom.t -> unit) ; Work.skip ) |> @@ -367,7 +367,7 @@ module Make (Dom : Domain_sig.Dom) = struct let exec_throw stk pre_state (block : Llair.block) exc = let func = block.parent in - [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var] + [%Trace.call fun {pf} -> pf "from %a" Reg.pp func.name.reg] ; let unwind params scope from_call state = Dom.retn params (Some func.fthrow) from_call @@ -390,7 +390,7 @@ module Make (Dom : Domain_sig.Dom) = struct Stack.t -> Dom.t -> Llair.block - -> Var.t option + -> Reg.t option -> Llair.jump -> Work.x = fun stk state block areturn return -> @@ -423,7 +423,7 @@ module Make (Dom : Domain_sig.Dom) = struct Dom.exec_assume state (Exp.eq ptr (Exp.label - ~parent:(Var.name jump.dst.parent.name.var) + ~parent:(Reg.name jump.dst.parent.name.reg) ~name:jump.dst.lbl)) with | Some state -> exec_jump stk state block jump |> Work.seq x @@ -439,7 +439,7 @@ module Make (Dom : Domain_sig.Dom) = struct List.fold callees ~init:Work.skip ~f:(fun x callee -> ( match Dom.exec_intrinsic ~skip_throw:opts.skip_throw state - areturn callee.name.var args + areturn callee.name.reg args with | Some (Error ()) -> Report.invalid_access_term @@ -452,7 +452,7 @@ module Make (Dom : Domain_sig.Dom) = struct exec_skip_func stk state block areturn return | None -> exec_call opts stk state block {call with callee} - (used_globals opts callee.name.var) ) + (used_globals opts callee.name.reg) ) |> Work.seq x ) ) | Return {exp} -> exec_return ~opts stk state block exp | Throw {exc} -> @@ -481,12 +481,12 @@ module Make (Dom : Domain_sig.Dom) = struct let entry_points = Config.find_list "entry-points" in List.find_map ~f:(Llair.Func.find pgm.functions) entry_points |> function - | Some {name= {var}; locals; params= []; entry} -> + | Some {name= {reg}; locals; params= []; entry} -> Some (Work.init (fst (Dom.call ~summaries:opts.function_summaries - ~globals:(used_globals opts var) [] None [] ~locals + ~globals:(used_globals opts reg) [] None [] ~locals (Dom.init pgm.globals))) entry) | _ -> None @@ -501,9 +501,9 @@ module Make (Dom : Domain_sig.Dom) = struct |> [%Trace.retn fun {pf} _ -> pf ""] - let compute_summaries opts pgm : Dom.summary list Var.Map.t = + let compute_summaries opts pgm : Dom.summary list Reg.Map.t = assert opts.function_summaries ; exec_pgm opts pgm ; - Hashtbl.fold summary_table ~init:Var.Map.empty ~f:(fun ~key ~data map -> + Hashtbl.fold summary_table ~init:Reg.Map.empty ~f:(fun ~key ~data map -> match data with [] -> map | _ -> Map.set map ~key ~data ) end diff --git a/sledge/src/control.mli b/sledge/src/control.mli index f7e1543bc..802c5fbce 100644 --- a/sledge/src/control.mli +++ b/sledge/src/control.mli @@ -11,11 +11,11 @@ type exec_opts = { bound: int (** Loop/recursion unrolling bound *) ; skip_throw: bool (** Treat throw as unreachable *) ; function_summaries: bool (** Use function summarisation *) - ; globals: [`Per_function of Var.Set.t Var.Map.t | `Declared of Var.Set.t] + ; globals: [`Per_function of Reg.Set.t Reg.Map.t | `Declared of Reg.Set.t] (** Either a per-function used-globals map or a program-wide set *) } module Make (Dom : Domain_sig.Dom) : sig val exec_pgm : exec_opts -> Llair.t -> unit - val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Var.Map.t + val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Reg.Map.t end diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index 26b2d169c..428767610 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -15,15 +15,15 @@ module type Dom = sig val join : t -> t -> t option val is_false : t -> bool val exec_assume : t -> Exp.t -> t option - val exec_kill : t -> Var.t -> t - val exec_move : t -> Var.t -> Exp.t -> t + val exec_kill : t -> Reg.t -> t + val exec_move : t -> Reg.t -> Exp.t -> t val exec_inst : t -> Llair.inst -> (t, unit) result val exec_intrinsic : skip_throw:bool -> t - -> Var.t option - -> Var.t + -> Reg.t option + -> Reg.t -> Exp.t list -> (t, unit) result option @@ -31,17 +31,17 @@ module type Dom = sig val call : summaries:bool - -> globals:Var.Set.t + -> globals:Reg.Set.t -> Exp.t list - -> Var.t option - -> Var.t list - -> locals:Var.Set.t + -> Reg.t option + -> Reg.t list + -> locals:Reg.Set.t -> t -> t * from_call val recursion_beyond_bound : [`skip | `prune] - val post : Var.Set.t -> from_call -> t -> t - val retn : Var.t list -> Var.t option -> from_call -> t -> t + val post : Reg.Set.t -> from_call -> t -> t + val retn : Reg.t list -> Reg.t option -> from_call -> t -> t val dnf : t -> t list val resolve_callee : @@ -52,7 +52,7 @@ module type Dom = sig val pp_summary : summary pp val create_summary : - locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t + locals:Reg.Set.t -> formals:Reg.Set.t -> t -> summary * t val apply_summary : t -> summary -> t option end diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index a1fb3f4cc..990fa66ea 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -12,8 +12,8 @@ module type State_domain_sig = sig include Domain_sig.Dom val create_summary : - locals:Var.Set.t - -> formals:Var.Set.t + locals:Reg.Set.t + -> formals:Reg.Set.t -> entry:t -> current:t -> summary * t @@ -77,8 +77,8 @@ module Make (State_domain : State_domain_sig) = struct pf "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ globals: {@[%a@]}@ current: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Var.Set.pp locals Var.Set.pp globals + (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp) + (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals State_domain.pp current] ; let caller_current, state_from_call = @@ -91,7 +91,7 @@ module Make (State_domain : State_domain_sig) = struct [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] let post locals {state_from_call; caller_entry} (_, current) = - [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals] + [%Trace.call fun {pf} -> pf "locals: %a" Reg.Set.pp locals] ; (caller_entry, State_domain.post locals state_from_call current) |> diff --git a/sledge/src/domain/relation.mli b/sledge/src/domain/relation.mli index 0e28b3f15..6ef12d598 100644 --- a/sledge/src/domain/relation.mli +++ b/sledge/src/domain/relation.mli @@ -12,8 +12,8 @@ module type State_domain_sig = sig include Domain_sig.Dom val create_summary : - locals:Var.Set.t - -> formals:Var.Set.t + locals:Reg.Set.t + -> formals:Reg.Set.t -> entry:t -> current:t -> summary * t diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index 8b628f1cf..5978bcc15 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -29,8 +29,8 @@ let retn _ _ _ _ = () let dnf () = [()] let resolve_callee lookup ptr _ = - match Var.of_exp ptr with - | Some callee -> (lookup (Var.name callee), ()) + match Reg.of_exp ptr with + | Some callee -> (lookup (Reg.name callee), ()) | None -> ([], ()) type summary = unit diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index e91e39248..479733b09 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -7,11 +7,11 @@ (** Used-globals abstract domain *) -type t = Var.Set.t [@@deriving equal, sexp_of] +type t = Reg.Set.t [@@deriving equal, sexp_of] -let pp = Set.pp Var.pp +let pp = Set.pp Reg.pp let report_fmt_thunk = Fn.flip pp -let empty = Var.Set.empty +let empty = Reg.Set.empty let init globals = [%Trace.info @@ -24,10 +24,10 @@ let is_false _ = false let post _ _ state = state let retn _ _ from_call post = Set.union from_call post let dnf t = [t] -let add_if_global gs v = if Var.global v then Set.add gs v else gs +let add_if_global gs v = if Reg.global v then Set.add gs v else gs let used_globals ?(init = empty) exp = - Exp.fold_vars exp ~init ~f:add_if_global + Exp.fold_regs exp ~init ~f:add_if_global let exec_assume st exp = Some (used_globals ~init:st exp) let exec_kill st _ = st @@ -44,7 +44,7 @@ let exec_inst st inst = Result.iter ~f:(fun uses -> pf "post:{%a}" pp uses)] let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = - let name = Var.name intrinsic in + let name = Reg.name intrinsic in if List.exists [ "malloc"; "aligned_alloc"; "calloc"; "posix_memalign"; "realloc" @@ -66,11 +66,11 @@ let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st = let resolve_callee lookup ptr st = let st = used_globals ~init:st ptr in - match Var.of_exp ptr with - | Some callee -> (lookup (Var.name callee), st) + match Reg.of_exp ptr with + | Some callee -> (lookup (Reg.name callee), st) | None -> ([], st) -(* A function summary is the set of global variables accessed by that +(* A function summary is the set of global registers accessed by that function and its transitive callees *) type summary = t diff --git a/sledge/src/domain/used_globals.mli b/sledge/src/domain/used_globals.mli index c20d91544..ee281a6dc 100644 --- a/sledge/src/domain/used_globals.mli +++ b/sledge/src/domain/used_globals.mli @@ -7,4 +7,4 @@ (** Used-globals abstract domain *) -include Domain_sig.Dom with type summary = Var.Set.t +include Domain_sig.Dom with type summary = Reg.Set.t diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 51643fe88..3704cd674 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -58,7 +58,7 @@ module rec T : sig | Memory of {siz: t; arr: t} | Concat of {args: t vector} (* nullary *) - | Var of {id: int; name: string; global: bool} + | Reg of {id: int; name: string; global: bool} | Nondet of {msg: string} | Label of {parent: string; name: string} (* curried application *) @@ -123,7 +123,7 @@ and T0 : sig | Splat of {byt: t; siz: t} | Memory of {siz: t; arr: t} | Concat of {args: t vector} - | Var of {id: int; name: string; global: bool} + | Reg of {id: int; name: string; global: bool} | Nondet of {msg: string} | Label of {parent: string; name: string} | App of {op: t; arg: t} @@ -167,7 +167,7 @@ end = struct | Splat of {byt: t; siz: t} | Memory of {siz: t; arr: t} | Concat of {args: t vector} - | Var of {id: int; name: string; global: bool} + | Reg of {id: int; name: string; global: bool} | Nondet of {msg: string} | Label of {parent: string; name: string} | App of {op: t; arg: t} @@ -236,10 +236,10 @@ let uncurry = uncurry_ [] let rec pp ?is_x fs exp = - let get_var_style var = + let get_reg_style reg = match is_x with | None -> `None - | Some is_x -> if not (is_x var) then `Bold else `Cyan + | Some is_x -> if not (is_x reg) then `Bold else `Cyan in let pp_ pp fs exp = let pf fmt = @@ -247,12 +247,12 @@ let rec pp ?is_x fs exp = Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt in match exp with - | Var {name; id= 0; global= true} as var -> - Trace.pp_styled (get_var_style var) "%@%s" fs name - | Var {name; id= 0; global= false} as var -> - Trace.pp_styled (get_var_style var) "%%%s" fs name - | Var {name; id; _} as var -> - Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id + | Reg {name; id= 0; global= true} as reg -> + Trace.pp_styled (get_reg_style reg) "%@%s" fs name + | Reg {name; id= 0; global= false} as reg -> + Trace.pp_styled (get_reg_style reg) "%%%s" fs name + | Reg {name; id; _} as reg -> + Trace.pp_styled (get_reg_style reg) "%%%s_%d" fs name id | Nondet {msg} -> pf "nondet \"%s\"" msg | Label {name} -> pf "%s" name | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null" @@ -455,7 +455,7 @@ let invariant ?(partial = false) e = assert_arity 0 ; assert (Z.numbits data <= bits) ) | Integer _ -> assert false - | Var {id; global; _} -> + | Reg {id; global; _} -> assert_arity 0 ; assert ((not global) || id = 0) | Nondet _ | Label _ | Float _ -> assert_arity 0 @@ -500,13 +500,13 @@ let bits_of_int exp = | None -> violates invariant exp ) | _ -> fail "bits_of_int" () -(** Variables are the expressions constructed by [Var] *) -module Var = struct +(** Registers are the expressions constructed by [Reg] *) +module Reg = struct include T let pp = pp - type var = t + type reg = t module Set = struct include ( @@ -553,7 +553,7 @@ module Var = struct if !@status = 0 then demangled else None let pp_demangled fs = function - | Var {name} -> ( + | Reg {name} -> ( match demangle name with | Some demangled when not (String.equal name demangled) -> Format.fprintf fs "“%s”" demangled @@ -562,25 +562,25 @@ module Var = struct let invariant x = Invariant.invariant [%here] x [%sexp_of: t] - @@ fun () -> match x with Var _ -> invariant x | _ -> assert false + @@ fun () -> match x with Reg _ -> invariant x | _ -> assert false - let id = function Var {id} -> id | x -> violates invariant x - let name = function Var {name} -> name | x -> violates invariant x - let global = function Var {global} -> global | x -> violates invariant x + let id = function Reg {id} -> id | x -> violates invariant x + let name = function Reg {name} -> name | x -> violates invariant x + let global = function Reg {global} -> global | x -> violates invariant x let of_exp = function - | Var _ as v -> Some (v |> check invariant) + | Reg _ as x -> Some (x |> check invariant) | _ -> None let program ?global name = - Var {id= 0; name; global= Option.is_some global} |> check invariant + Reg {id= 0; name; global= Option.is_some global} |> check invariant let fresh name ~(wrt : Set.t) = let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in - let x' = Var {name; id= max + 1; global= false} in + let x' = Reg {name; id= max + 1; global= false} in (x', Set.add wrt x') - (** Variable renaming substitutions *) + (** Register renaming substitutions *) module Subst = struct type t = T.t Map.M(T).t [@@deriving compare, equal, sexp] @@ -675,15 +675,15 @@ let fold_exps e ~init ~f = let iter_exps e ~f = fold_exps e ~init:() ~f:(fun () e -> f e) -let fold_vars e ~init ~f = +let fold_regs e ~init ~f = fold_exps e ~init ~f:(fun z -> function - | Var _ as v -> f z (v :> Var.t) | _ -> z ) + | Reg _ as x -> f z (x :> Reg.t) | _ -> z ) -let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty +let fv e = fold_regs e ~f:Set.add ~init:Reg.Set.empty (** Construct *) -let var x = x +let reg x = x let nondet msg = Nondet {msg} |> check invariant let label ~parent ~name = Label {parent; name} |> check invariant let integer data typ = Integer {data; typ} |> check invariant @@ -1331,7 +1331,7 @@ let map e ~f = let rename sub e = let rec rename_ sub e = match e with - | Var _ -> Var.Subst.apply sub e + | Reg _ -> Reg.Subst.apply sub e | _ -> map ~f:(rename_ sub) e in rename_ sub e |> check (invariant ~partial:true) @@ -1349,7 +1349,7 @@ let is_false = function let rec is_constant e = let is_constant_bin x y = is_constant x && is_constant y in match e with - | Var _ | Nondet _ -> false + | Reg _ | Nondet _ -> false | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y} -> is_constant_bin x y @@ -1413,4 +1413,4 @@ let solve e f = solve_ e f empty_map |> [%Trace.retn fun {pf} -> - function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"] + function Some s -> pf "%a" Reg.Subst.pp s | None -> pf "false"] diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index d65546bce..0acc9a7a1 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -27,10 +27,10 @@ and t = private (** Iterated concatenation of a single byte *) | Memory of {siz: t; arr: t} (** Size-tagged byte-array *) | Concat of {args: t vector} (** Byte-array concatenation *) - | Var of {id: int; name: string; global: bool} + | Reg of {id: int; name: string; global: bool} (** Local variable / virtual register *) | Nondet of {msg: string} - (** Anonymous local variable with arbitrary value, representing + (** Anonymous register with arbitrary value, representing non-deterministic approximation of value described by [msg] *) | Label of {parent: string; name: string} (** Address of named code block within parent function *) @@ -81,28 +81,28 @@ val pp_full : ?is_x:(exp -> bool) -> t pp val pp : t pp val invariant : ?partial:bool -> t -> unit -(** Exp.Var is re-exported as Var *) -module Var : sig +(** Exp.Reg is re-exported as Reg *) +module Reg : sig type t = private exp [@@deriving compare, equal, hash, sexp] - type var = t + type reg = t include Comparator.S with type t := t module Set : sig - type t = (var, comparator_witness) Set.t + type t = (reg, comparator_witness) Set.t [@@deriving compare, equal, sexp] val pp_full : ?is_x:(exp -> bool) -> t pp val pp : t pp val empty : t - val of_option : var option -> t - val of_list : var list -> t + val of_option : reg option -> t + val of_list : reg list -> t + val of_vector : reg vector -> t val union_list : t list -> t - val of_vector : var vector -> t end module Map : sig - type 'a t = (var, 'a, comparator_witness) Map.t + type 'a t = (reg, 'a, comparator_witness) Map.t [@@deriving compare, equal, sexp] val empty : 'a t @@ -126,7 +126,7 @@ module Var : sig val pp : t pp val empty : t val freshen : Set.t -> wrt:Set.t -> t - val extend : t -> replace:var -> with_:var -> t + val extend : t -> replace:reg -> with_:reg -> t val invert : t -> t val exclude : t -> Set.t -> t val restrict : t -> Set.t -> t @@ -140,7 +140,7 @@ end (** Construct *) -val var : Var.t -> t +val reg : Reg.t -> t val nondet : string -> t val label : parent:string -> name:string -> t val null : t @@ -200,18 +200,18 @@ val size_of : Typ.t -> t option (** Access *) val iter : t -> f:(t -> unit) -> unit -val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a +val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a val fold_exps : t -> init:'a -> f:('a -> t -> 'a) -> 'a val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a (** Transform *) val map : t -> f:(t -> t) -> t -val rename : Var.Subst.t -> t -> t +val rename : Reg.Subst.t -> t -> t (** Query *) -val fv : t -> Var.Set.t +val fv : t -> Reg.Set.t val is_true : t -> bool val is_false : t -> bool val typ : t -> Typ.t option diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index a7fb3d175..4d21eb448 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -288,9 +288,10 @@ let xlate_float : Llvm.llvalue -> Exp.t = let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in Exp.float data -let xlate_name ?global llv = Var.program ?global (find_name llv) +let xlate_name ?global : Llvm.llvalue -> Reg.t = + fun llv -> Reg.program ?global (find_name llv) -let xlate_name_opt : Llvm.llvalue -> Var.t option = +let xlate_name_opt : Llvm.llvalue -> Reg.t option = fun instr -> match Llvm.classify_type (Llvm.type_of instr) with | Void -> None @@ -357,11 +358,11 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t = let fname = Llvm.value_name func in match xlate_intrinsic_exp fname with | Some intrinsic when inline || should_inline llv -> intrinsic x llv - | _ -> Exp.var (xlate_name llv) ) + | _ -> Exp.reg (xlate_name llv) ) | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg) |Argument -> - Exp.var (xlate_name llv) - | Function | GlobalVariable -> Exp.var (xlate_global x llv).var + Exp.reg (xlate_name llv) + | Function | GlobalVariable -> Exp.reg (xlate_global x llv).reg | GlobalAlias -> xlate_value x (Llvm.operand llv 0) | ConstantInt -> xlate_int x llv | ConstantFP -> xlate_float llv @@ -407,7 +408,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t = | Select | GetElementPtr | ExtractElement | InsertElement | ShuffleVector | ExtractValue | InsertValue ) as opcode ) -> if inline || should_inline llv then xlate_opcode x llv opcode - else Exp.var (xlate_name llv) + else Exp.reg (xlate_name llv) | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv) | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv () | Instruction (CatchPad | CleanupPad | CatchSwitch) -> @@ -630,15 +631,15 @@ type pop_thunk = Loc.t -> Llair.inst list let pop_stack_frame_of_function : Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk = fun func entry_blk -> - let append_stack_vars blk vars = + let append_stack_regs blk regs = Llvm.fold_right_instrs - (fun instr vars -> + (fun instr regs -> match Llvm.instr_opcode instr with - | Alloca -> xlate_name instr :: vars - | _ -> vars ) - blk vars + | Alloca -> xlate_name instr :: regs + | _ -> regs ) + blk regs in - let entry_vars = append_stack_vars entry_blk [] in + let entry_regs = append_stack_regs entry_blk [] in Llvm.iter_blocks (fun blk -> if not (Poly.equal entry_blk blk) then @@ -652,8 +653,8 @@ let pop_stack_frame_of_function : blk ) func ; let pop retn_loc = - List.map entry_vars ~f:(fun var -> - Llair.Inst.free ~ptr:(Exp.var var) ~loc:retn_loc ) + List.map entry_regs ~f:(fun reg -> + Llair.Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc ) in pop @@ -690,7 +691,7 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype = the PHIs of [dst] translated to a move. *) let xlate_jump : x - -> ?reg_exps:(Var.var * Exp.t) list + -> ?reg_exps:(Reg.reg * Exp.t) list -> Llvm.llvalue -> Llvm.llbasicblock -> Loc.t @@ -753,7 +754,7 @@ let pp_code fs (insts, term, blocks) = let rec xlate_func_name x llv = match Llvm.classify_value llv with - | Function -> Exp.var (xlate_name ~global:() llv) + | Function -> Exp.reg (xlate_name ~global:() llv) | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv) | Argument | Instruction _ -> xlate_value x llv | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0) @@ -1076,8 +1077,8 @@ let xlate_instr : passing a value for the selector which the handler code tests to e.g. either cleanup or rethrow. *) let i32, tip, cxa_exception = landingpad_typs x instr in - let exc = Exp.var (Var.program (find_name instr ^ ".exc")) in - let ti = Var.program (name ^ ".ti") in + let exc = Exp.reg (Reg.program (find_name instr ^ ".exc")) in + let ti = Reg.program (name ^ ".ti") in (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *) let load_ti = let typ = cxa_exception in @@ -1093,7 +1094,7 @@ let xlate_instr : let len = Exp.integer (Z.of_int (size_of x typ)) Typ.siz in Llair.Inst.load ~reg:ti ~ptr ~len ~loc in - let ti = Exp.var ti in + let ti = Exp.reg ti in let typeid = xlate_llvm_eh_typeid_for x tip ti in let lbl = name ^ ".unwind" in let param = xlate_name instr in @@ -1245,10 +1246,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = let freturn = match name.typ with | Pointer {elt= Function {return= Some _; _}} -> - Some (Var.program "freturn") + Some (Reg.program "freturn") | _ -> None in - let fthrow = Var.program "fthrow" in + let fthrow = Reg.program "fthrow" in ( match Llvm.block_begin llf with | Before entry_blk -> let pop = pop_stack_frame_of_function llf entry_blk in diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml index 4397be474..634a847c7 100644 --- a/sledge/src/llair/global.ml +++ b/sledge/src/llair/global.ml @@ -7,27 +7,27 @@ (** Global variables *) -type t = {var: Var.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t} +type t = {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t} [@@deriving compare, equal, hash, sexp] -let pp fs {var} = - let name = Var.name var in +let pp fs {reg} = + let name = Reg.name reg in let pf pp = Format.pp_open_box fs 2 ; Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp in - pf "@%s%a" name Var.pp_demangled var + pf "@%s%a" name Reg.pp_demangled reg -let pp_defn fs {var; init; typ; loc} = - Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Var.pp var Loc.pp loc +let pp_defn fs {reg; init; typ; loc} = + Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp typ Reg.pp reg Loc.pp loc (Option.pp "@ = @[%a@]" (fun fs (init, _) -> Exp.pp fs init)) init let invariant g = Invariant.invariant [%here] g [%sexp_of: t] @@ fun () -> - let {var; typ} = g in + let {reg; typ} = g in assert (Typ.is_sized typ) ; - assert (Var.global var) + assert (Reg.global reg) -let mk ?init var typ loc = {var; init; typ; loc} |> check invariant +let mk ?init reg typ loc = {reg; init; typ; loc} |> check invariant diff --git a/sledge/src/llair/global.mli b/sledge/src/llair/global.mli index a545f6eb3..0d22cfc88 100644 --- a/sledge/src/llair/global.mli +++ b/sledge/src/llair/global.mli @@ -8,7 +8,7 @@ (** Global variables *) type t = private - {var: Var.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t} + {reg: Reg.t; init: (Exp.t * int) option; typ: Typ.t; loc: Loc.t} [@@deriving compare, equal, hash, sexp] val pp : t pp @@ -16,4 +16,4 @@ val pp_defn : t pp include Invariant.S with type t := t -val mk : ?init:Exp.t * int -> Var.t -> Typ.t -> Loc.t -> t +val mk : ?init:Exp.t * int -> Reg.t -> Typ.t -> Loc.t -> t diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index cb573ff27..37835a476 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -10,15 +10,15 @@ [@@@warning "+9"] type inst = - | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t} - | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t} + | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t} + | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t} | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t} | Memset of {dst: Exp.t; byt: Exp.t; len: Exp.t; loc: Loc.t} | Memcpy of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t} | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t} - | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t} + | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t} | Free of {ptr: Exp.t; loc: Loc.t} - | Nondet of {reg: Var.t option; msg: string; loc: Loc.t} + | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t} | Abort of {loc: Loc.t} [@@deriving sexp] @@ -31,7 +31,7 @@ and 'a call = { callee: 'a ; typ: Typ.t ; args: Exp.t list - ; areturn: Var.t option + ; areturn: Reg.t option ; return: jump ; throw: jump option ; mutable recursive: bool @@ -57,10 +57,10 @@ and cfg = block vector (* [entry] is not part of [cfg] since it cannot be jumped to, only called. *) and func = { name: Global.t - ; params: Var.t list - ; freturn: Var.t option - ; fthrow: Var.t - ; locals: Var.Set.t + ; params: Reg.t list + ; freturn: Reg.t option + ; fthrow: Reg.t + ; locals: Reg.Set.t ; entry: block ; cfg: cfg } @@ -87,7 +87,7 @@ let sexp_of_term = function { callee: Exp.t ; typ: Typ.t ; args: Exp.t list - ; areturn: Var.t option + ; areturn: Reg.t option ; return: jump ; throw: jump option ; recursive: bool @@ -102,7 +102,7 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} = { lbl: label ; cmnd: cmnd ; term: term - ; parent: Var.t = parent.name.var + ; parent: Reg.t = parent.name.reg ; sort_index: int }] let sexp_of_cfg v = [%sexp_of: block vector] v @@ -110,10 +110,10 @@ let sexp_of_cfg v = [%sexp_of: block vector] v let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} = [%sexp { name: Global.t - ; params: Var.t list - ; freturn: Var.t option - ; fthrow: Var.t - ; locals: Var.Set.t + ; params: Reg.t list + ; freturn: Reg.t option + ; fthrow: Reg.t + ; locals: Reg.Set.t ; entry: block ; cfg: cfg }] @@ -131,10 +131,10 @@ let pp_inst fs inst = match inst with | Move {reg_exps; loc} -> let regs, exps = Vector.unzip reg_exps in - pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs + pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Reg.pp) regs (Vector.pp ",@ " Exp.pp) exps Loc.pp loc | Load {reg; ptr; len; loc} -> - pf "@[<2>%a@ := load %a@ %a;@]\t%a" Var.pp reg Exp.pp len Exp.pp ptr + pf "@[<2>%a@ := load %a@ %a;@]\t%a" Reg.pp reg Exp.pp len Exp.pp ptr Loc.pp loc | Store {ptr; exp; len; loc} -> pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp @@ -149,19 +149,19 @@ let pp_inst fs inst = pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src Loc.pp loc | Alloc {reg; num; len; loc} -> - pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp + pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Reg.pp reg Exp.pp num Exp.pp len Loc.pp loc | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc | Nondet {reg; msg; loc} -> pf "@[<2>%anondet \"%s\";@]\t%a" - (Option.pp "%a := " Var.pp) + (Option.pp "%a := " Reg.pp) reg msg Loc.pp loc | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc let pp_args pp_arg fs args = Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_arg) (List.rev args) -let pp_param fs var = Var.pp fs var +let pp_param fs reg = Reg.pp fs reg let pp_jump fs {dst; retreating} = Format.fprintf fs "@[<2>%s%%%s@]" @@ -190,7 +190,7 @@ let pp_term fs term = tbl Loc.pp loc | Call {callee; args; areturn; return; throw; recursive; loc; _} -> pf "@[<2>@[<7>%acall @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a" - (Option.pp "%a := " Var.pp) + (Option.pp "%a := " Reg.pp) areturn (if recursive then "↑" else "") Exp.pp callee (pp_args Exp.pp) args pp_jump return @@ -219,13 +219,13 @@ let rec dummy_block = ; sort_index= 0 } and dummy_func = - let dummy_var = Var.program ~global:() "dummy" in + let dummy_reg = Reg.program ~global:() "dummy" in let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in - { name= Global.mk dummy_var dummy_ptr_typ Loc.none + { name= Global.mk dummy_reg dummy_ptr_typ Loc.none ; params= [] ; freturn= None - ; fthrow= dummy_var - ; locals= Var.Set.empty + ; fthrow= dummy_reg + ; locals= Reg.Set.empty ; entry= dummy_block ; cfg= Vector.empty } @@ -270,7 +270,7 @@ module Inst = struct |Abort _ -> vs - let locals inst = union_locals inst Var.Set.empty + let locals inst = union_locals inst Reg.Set.empty let fold_exps inst ~init ~f = match inst with @@ -408,7 +408,7 @@ module Func = struct ( match name.typ with | Pointer {elt= Function {return; _}} -> return | _ -> None ) - (Option.pp " %a := " Var.pp) + (Option.pp " %a := " Reg.pp) freturn Global.pp name (pp_args pp_param) params (fun fs -> if is_undefined func then Format.fprintf fs " #%i@]" sort_index @@ -451,7 +451,7 @@ module Func = struct let locals_block locals block = locals_cmnd (Term.union_locals block.term locals) block.cmnd in - let init = locals_block Var.Set.empty entry in + let init = locals_block Reg.Set.empty entry in Vector.fold ~f:locals_block cfg ~init in let func = {name; params; freturn; fthrow; locals; entry; cfg} in @@ -509,17 +509,17 @@ module Block_label = struct end module BlockQ = Hash_queue.Make (Block_label) -module FuncQ = Hash_queue.Make (Var) +module FuncQ = Hash_queue.Make (Reg) let set_derived_metadata functions = let compute_roots functions = let roots = FuncQ.create () in Map.iter functions ~f:(fun func -> - FuncQ.enqueue_back_exn roots func.name.var func ) ; + FuncQ.enqueue_back_exn roots func.name.reg func ) ; Map.iter functions ~f:(fun func -> Func.fold_term func ~init:() ~f:(fun () -> function | Call {callee; _} -> ( - match Var.of_exp callee with + match Reg.of_exp callee with | Some callee -> FuncQ.remove roots callee |> (ignore : [> ] -> unit) | None -> () ) @@ -543,7 +543,7 @@ let set_derived_metadata functions = | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump | Call ({callee; return; throw; _} as call) -> ( match - Var.of_exp callee >>| Var.name >>= Func.find functions + Reg.of_exp callee >>| Reg.name >>= Func.find functions with | Some func -> if Set.mem ancestors func.entry then call.recursive <- true @@ -575,7 +575,7 @@ let set_derived_metadata functions = List.fold functions ~init:(Map.empty (module String)) ~f:(fun m func -> - Map.add_exn m ~key:(Var.name func.name.var) ~data:func ) + Map.add_exn m ~key:(Reg.name func.name.reg) ~data:func ) in let roots = compute_roots functions in let tips_to_roots = topsort functions roots in @@ -589,7 +589,7 @@ let invariant pgm = assert ( not (Vector.contains_dup pgm.globals ~compare:(fun g1 g2 -> - Var.compare g1.Global.var g2.Global.var )) ) + Reg.compare g1.Global.reg g2.Global.reg )) ) let mk ~globals ~functions = { globals= Vector.of_list_rev globals diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 1636efd54..430cbe8e5 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -10,10 +10,10 @@ (** Instructions for memory manipulation or other non-control effects. *) type inst = private - | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t} + | Move of {reg_exps: (Reg.t * Exp.t) vector; loc: Loc.t} (** Move each value [exp] into corresponding register [reg]. All of the moves take effect simultaneously. *) - | Load of {reg: Var.t; ptr: Exp.t; len: Exp.t; loc: Loc.t} + | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t} (** Read a [len]-byte value from the contents of memory at address [ptr] into [reg]. *) | Store of {ptr: Exp.t; exp: Exp.t; len: Exp.t; loc: Loc.t} @@ -25,12 +25,12 @@ type inst = private if ranges overlap. *) | Memmov of {dst: Exp.t; src: Exp.t; len: Exp.t; loc: Loc.t} (** Copy [len] bytes starting from address [src] to [dst]. *) - | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t} + | Alloc of {reg: Reg.t; num: Exp.t; len: Exp.t; loc: Loc.t} (** Allocate a block of memory large enough to store [num] elements of [len] bytes each and bind [reg] to the first address. *) | Free of {ptr: Exp.t; loc: Loc.t} (** Deallocate the previously allocated block at address [ptr]. *) - | Nondet of {reg: Var.t option; msg: string; loc: Loc.t} + | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t} (** Bind [reg] to an arbitrary value, representing non-deterministic approximation of behavior described by [msg]. *) | Abort of {loc: Loc.t} (** Trigger abnormal program termination *) @@ -49,7 +49,7 @@ and 'a call = { callee: 'a ; typ: Typ.t (** Type of the callee. *) ; args: Exp.t list (** Stack of arguments, first-arg-last. *) - ; areturn: Var.t option (** Register to receive return value. *) + ; areturn: Reg.t option (** Register to receive return value. *) ; return: jump (** Return destination. *) ; throw: jump option (** Handler destination. *) ; mutable recursive: bool @@ -89,10 +89,10 @@ and cfg parameters are the function parameters. *) and func = private { name: Global.t - ; params: Var.t list (** Formal parameters, first-param-last stack *) - ; freturn: Var.t option - ; fthrow: Var.t - ; locals: Var.Set.t (** Local variables *) + ; params: Reg.t list (** Formal parameters, first-param-last stack *) + ; freturn: Reg.t option + ; fthrow: Reg.t + ; locals: Reg.Set.t (** Local registers *) ; entry: block ; cfg: cfg } @@ -112,18 +112,18 @@ module Inst : sig type t = inst val pp : t pp - val move : reg_exps:(Var.t * Exp.t) vector -> loc:Loc.t -> inst - val load : reg:Var.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst + val move : reg_exps:(Reg.t * Exp.t) vector -> loc:Loc.t -> inst + val load : reg:Reg.t -> ptr:Exp.t -> len:Exp.t -> loc:Loc.t -> inst val store : ptr:Exp.t -> exp:Exp.t -> len:Exp.t -> loc:Loc.t -> inst val memset : dst:Exp.t -> byt:Exp.t -> len:Exp.t -> loc:Loc.t -> inst val memcpy : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst val memmov : dst:Exp.t -> src:Exp.t -> len:Exp.t -> loc:Loc.t -> inst - val alloc : reg:Var.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst + val alloc : reg:Reg.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst val free : ptr:Exp.t -> loc:Loc.t -> inst - val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst + val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst val abort : loc:Loc.t -> inst val loc : inst -> Loc.t - val locals : inst -> Var.Set.t + val locals : inst -> Reg.Set.t val fold_exps : inst -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a end @@ -154,7 +154,7 @@ module Term : sig func:Exp.t -> typ:Typ.t -> args:Exp.t list - -> areturn:Var.t option + -> areturn:Reg.t option -> return:jump -> throw:jump option -> loc:Loc.t @@ -184,18 +184,18 @@ module Func : sig val mk : name:Global.t - -> params:Var.t list - -> freturn:Var.t option - -> fthrow:Var.t + -> params:Reg.t list + -> freturn:Reg.t option + -> fthrow:Reg.t -> entry:block -> cfg:block vector -> func val mk_undefined : name:Global.t - -> params:Var.t list - -> freturn:Var.t option - -> fthrow:Var.t + -> params:Reg.t list + -> freturn:Reg.t option + -> fthrow:Reg.t -> t val find : functions -> string -> func option diff --git a/sledge/src/llair/reg.ml b/sledge/src/llair/reg.ml new file mode 100644 index 000000000..bccfa565a --- /dev/null +++ b/sledge/src/llair/reg.ml @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Variables *) + +include Exp.Reg diff --git a/sledge/src/llair/reg.mli b/sledge/src/llair/reg.mli new file mode 100644 index 000000000..568b21b70 --- /dev/null +++ b/sledge/src/llair/reg.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Variables *) + +include module type of Exp.Reg diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 0e8dde708..ff91c5561 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -16,8 +16,8 @@ let unknown_call call = (fun fs (call : Llair.Term.t) -> match call with | Call {callee} -> ( - match Var.of_exp callee with - | Some var -> Var.pp_demangled fs var + match Reg.of_exp callee with + | Some reg -> Reg.pp_demangled fs reg | None -> Exp.pp fs callee ) | _ -> () ) call Llair.Term.pp call] diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index a7933e77f..16a3a0935 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -75,14 +75,14 @@ let used_globals pgm preanalyze = { bound= 1 ; skip_throw= false ; function_summaries= true - ; globals= `Declared Var.Set.empty } + ; globals= `Declared Reg.Set.empty } pgm in - `Per_function (Map.map summary_table ~f:Var.Set.union_list) + `Per_function (Map.map summary_table ~f:Reg.Set.union_list) else `Declared - (Vector.fold pgm.globals ~init:Var.Set.empty ~f:(fun acc g -> - Set.add acc g.var )) + (Vector.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g -> + Set.add acc g.reg )) let analyze = let%map_open bound = diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 1837d9231..9076fe833 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -7,11 +7,11 @@ (** Equality over uninterpreted functions and linear rational arithmetic *) -type 'a exp_map = 'a Map.M(Exp).t [@@deriving compare, equal, sexp] +type 'a term_map = 'a Map.M(Term).t [@@deriving compare, equal, sexp] -let empty_map = Map.empty (module Exp) +let empty_map = Map.empty (module Term) -type subst = Exp.t exp_map [@@deriving compare, equal, sexp] +type subst = Term.t term_map [@@deriving compare, equal, sexp] (** see also [invariant] *) type t = @@ -24,7 +24,7 @@ type t = let classes r = Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls -> - if Exp.equal key data then cls + if Term.equal key data then cls else Map.add_multi cls ~key:data ~data:key ) (** Pretty-printing *) @@ -36,17 +36,17 @@ let pp fs {sat; rep} = in Format.fprintf fs "[@[%a@]]" (List.pp ";@ " pp_assoc) alist in - let pp_exp_v fs (k, v) = if not (Exp.equal k v) then Exp.pp fs v in + let pp_term_v fs (k, v) = if not (Term.equal k v) then Term.pp fs v in Format.fprintf fs "@[{@[sat= %b;@ rep= %a@]}@]" sat - (pp_alist Exp.pp pp_exp_v) + (pp_alist Term.pp pp_term_v) (Map.to_alist rep) let pp_classes ?is_x fs r = List.pp "@ @<2>∧ " (fun fs (key, data) -> - Format.fprintf fs "@[%a@ = %a@]" (Exp.pp_full ?is_x) key - (List.pp "@ = " (Exp.pp_full ?is_x)) - (List.sort ~compare:Exp.compare data) ) + Format.fprintf fs "@[%a@ = %a@]" (Term.pp_full ?is_x) key + (List.pp "@ = " (Term.pp_full ?is_x)) + (List.sort ~compare:Term.compare data) ) fs (Map.to_alist (classes r)) @@ -66,17 +66,17 @@ let pp_diff fs (r, s) = | k, `Unequal vv -> Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_sdiff_val vv in - let pp_sdiff_exp_map = - let pp_sdiff_exp fs (u, v) = - Format.fprintf fs "-- %a ++ %a" Exp.pp u Exp.pp v + let pp_sdiff_term_map = + let pp_sdiff_term fs (u, v) = + Format.fprintf fs "-- %a ++ %a" Term.pp u Term.pp v in - pp_sdiff_map (pp_sdiff_elt Exp.pp Exp.pp pp_sdiff_exp) Exp.equal + pp_sdiff_map (pp_sdiff_elt Term.pp Term.pp pp_sdiff_term) Term.equal in let pp_sat fs = if not (Bool.equal r.sat s.sat) then Format.fprintf fs "sat= @[-- %b@ ++ %b@];@ " r.sat s.sat in - let pp_rep fs = pp_sdiff_exp_map "rep" fs r.rep s.rep in + let pp_rep fs = pp_sdiff_term_map "rep" fs r.rep s.rep in Format.fprintf fs "@[{@[%t%t@]}@]" pp_sat pp_rep (** Invariant *) @@ -85,68 +85,68 @@ let pp_diff fs (r, s) = let in_car r e = Map.mem r.rep e let rec iter_max_solvables e ~f = - match Exp.classify e with - | `Interpreted -> Exp.iter ~f:(iter_max_solvables ~f) e + match Term.classify e with + | `Interpreted -> Term.iter ~f:(iter_max_solvables ~f) e | _ -> f e let invariant r = Invariant.invariant [%here] r [%sexp_of: t] @@ fun () -> Map.iteri r.rep ~f:(fun ~key:a ~data:_ -> - (* no interpreted exps in carrier *) - assert (Poly.(Exp.classify a <> `Interpreted)) ; - (* carrier is closed under sub-expressions *) + (* no interpreted terms in carrier *) + assert (Poly.(Term.classify a <> `Interpreted)) ; + (* carrier is closed under subterms *) iter_max_solvables a ~f:(fun b -> assert ( in_car r b - || Trace.fail "@[subexp %a of %a not in carrier of@ %a@]" Exp.pp - b Exp.pp a pp r ) ) ) + || Trace.fail "@[subterm %a of %a not in carrier of@ %a@]" + Term.pp b Term.pp a pp r ) ) ) (** Core operations *) let true_ = {sat= true; rep= empty_map} |> check invariant -(** apply a subst to an exp *) +(** apply a subst to a term *) let apply s a = try Map.find_exn s a with Caml.Not_found -> a -(** apply a subst to maximal non-interpreted subexps *) +(** apply a subst to maximal non-interpreted subterms *) let rec norm s a = - match Exp.classify a with - | `Interpreted -> Exp.map ~f:(norm s) a - | `Simplified -> apply s (Exp.map ~f:(norm s) a) + match Term.classify a with + | `Interpreted -> Term.map ~f:(norm s) a + | `Simplified -> apply s (Term.map ~f:(norm s) a) | `Atomic | `Uninterpreted -> apply s a -(** exps are congruent if equal after normalizing subexps *) +(** terms are congruent if equal after normalizing subterms *) let congruent r a b = - Exp.equal (Exp.map ~f:(norm r.rep) a) (Exp.map ~f:(norm r.rep) b) + Term.equal (Term.map ~f:(norm r.rep) a) (Term.map ~f:(norm r.rep) b) (** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *) let lookup r a = With_return.with_return @@ fun {return} -> (* congruent specialized to assume [a] canonized and [b] non-interpreted *) - let semi_congruent r a b = Exp.equal a (Exp.map ~f:(apply r.rep) b) in + let semi_congruent r a b = Term.equal a (Term.map ~f:(apply r.rep) b) in Map.iteri r.rep ~f:(fun ~key ~data -> if semi_congruent r a key then return data ) ; a -(** rewrite an exp into canonical form using rep and, for uninterpreted - exps, congruence composed with rep *) +(** rewrite a term into canonical form using rep and, for uninterpreted + terms, congruence composed with rep *) let rec canon r a = - match Exp.classify a with - | `Interpreted -> Exp.map ~f:(canon r) a - | `Simplified | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a) + match Term.classify a with + | `Interpreted -> Term.map ~f:(canon r) a + | `Simplified | `Uninterpreted -> lookup r (Term.map ~f:(canon r) a) | `Atomic -> apply r.rep a -(** add an exp to the carrier *) +(** add a term to the carrier *) let rec extend a r = - match Exp.classify a with - | `Interpreted | `Simplified -> Exp.fold ~f:extend a ~init:r + match Term.classify a with + | `Interpreted | `Simplified -> Term.fold ~f:extend a ~init:r | `Uninterpreted -> Map.find_or_add r.rep a ~if_found:(fun _ -> r) ~default:a - ~if_added:(fun rep -> Exp.fold ~f:extend a ~init:{r with rep}) + ~if_added:(fun rep -> Term.fold ~f:extend a ~init:{r with rep}) | `Atomic -> r let extend a r = extend a r |> check invariant @@ -155,15 +155,15 @@ let compose r s = let rep = Map.map ~f:(norm s) r.rep in let rep = Map.merge_skewed rep s ~combine:(fun ~key v1 v2 -> - if Exp.equal v1 v2 then v1 - else fail "domains intersect: %a" Exp.pp key () ) + if Term.equal v1 v2 then v1 + else fail "domains intersect: %a" Term.pp key () ) in {r with rep} let merge a b r = - [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r] + [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r] ; - ( match Exp.solve a b with + ( match Term.solve a b with | Some s -> compose r s | None -> {r with sat= false} ) |> @@ -171,15 +171,15 @@ let merge a b r = pf "%a" pp_diff (r, r') ; invariant r'] -(** find an unproved equation between congruent exps *) +(** find an unproved equation between congruent terms *) let find_missing r = With_return.with_return @@ fun {return} -> Map.iteri r.rep ~f:(fun ~key:a ~data:a' -> Map.iteri r.rep ~f:(fun ~key:b ~data:b' -> if - Exp.compare a b < 0 - && (not (Exp.equal a' b')) + Term.compare a b < 0 + && (not (Term.equal a' b')) && congruent r a b then return (Some (a', b')) ) ) ; None @@ -207,15 +207,15 @@ let and_eq a b r = let b' = canon r b in let r = extend a' r in let r = extend b' r in - if Exp.equal a' b' then r else close (merge a' b' r) + if Term.equal a' b' then r else close (merge a' b' r) (** Exposed interface *) let is_true {sat; rep} = - sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Exp.equal a a') + sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a') let is_false {sat} = not sat -let entails_eq r d e = Exp.equal (canon r d) (canon r e) +let entails_eq r d e = Term.equal (canon r d) (canon r e) let entails r s = Map.for_alli s.rep ~f:(fun ~key:e ~data:e' -> entails_eq r e e') @@ -227,15 +227,15 @@ let class_of r e = e' :: Map.find_multi (classes r) e' let difference r a b = - [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r] + [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r] ; let a = canon r a in let b = canon r b in - ( if Exp.equal a b then Some Z.zero + ( if Term.equal a b then Some Z.zero else - match (Exp.typ a, Exp.typ b) with + match (Term.typ a, Term.typ b) with | Some typ, _ | _, Some typ -> ( - match normalize r (Exp.sub typ a b) with + match normalize r (Term.sub typ a b) with | Integer {data} -> Some data | _ -> None ) | _ -> None ) @@ -265,17 +265,17 @@ let or_ r s = let rs = merge_mems rs s r in rs -(* assumes that f is injective and for any set of exps E, f[E] is disjoint +(* assumes that f is injective and for any set of terms E, f[E] is disjoint from E *) -let map_exps ({sat= _; rep} as r) ~f = +let map_terms ({sat= _; rep} as r) ~f = [%Trace.call fun {pf} -> pf "%a" pp r] ; let map m = Map.fold m ~init:m ~f:(fun ~key ~data m -> let key' = f key in let data' = f data in - if Exp.equal key' key then - if Exp.equal data' data then m else Map.set m ~key ~data:data' + if Term.equal key' key then + if Term.equal data' data then m else Map.set m ~key ~data:data' else Map.remove m key |> Map.add_exn ~key:key' ~data:data' ) in let rep' = map rep in @@ -285,12 +285,12 @@ let map_exps ({sat= _; rep} as r) ~f = pf "%a" pp_diff (r, r') ; invariant r'] -let rename r sub = map_exps r ~f:(Exp.rename sub) +let rename r sub = map_terms r ~f:(Term.rename sub) -let fold_exps r ~init ~f = +let fold_terms r ~init ~f = Map.fold r.rep ~f:(fun ~key ~data z -> f (f z data) key) ~init let fold_vars r ~init ~f = - fold_exps r ~init ~f:(fun init -> Exp.fold_vars ~f ~init) + fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init) let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli index 52d236d72..6dcdf15eb 100644 --- a/sledge/src/symbheap/equality.mli +++ b/sledge/src/symbheap/equality.mli @@ -11,14 +11,14 @@ type t [@@deriving compare, equal, sexp] val pp : t pp -val pp_classes : ?is_x:(Exp.t -> bool) -> t pp +val pp_classes : ?is_x:(Term.t -> bool) -> t pp include Invariant.S with type t := t val true_ : t -(** The diagonal relation, which only equates each exp with itself. *) +(** The diagonal relation, which only equates each term with itself. *) -val and_eq : Exp.t -> Exp.t -> t -> t +val and_eq : Term.t -> Term.t -> t -> t (** Conjoin an equation to a relation. *) val and_ : t -> t -> t @@ -31,7 +31,7 @@ val rename : t -> Var.Subst.t -> t (** Apply a renaming substitution to the relation. *) val fv : t -> Var.Set.t -(** The variables occurring in the exps of the relation. *) +(** The variables occurring in the terms of the relation. *) val is_true : t -> bool (** Test if the relation is diagonal. *) @@ -39,24 +39,24 @@ val is_true : t -> bool val is_false : t -> bool (** Test if the relation is empty / inconsistent. *) -val entails_eq : t -> Exp.t -> Exp.t -> bool +val entails_eq : t -> Term.t -> Term.t -> bool (** Test if an equation is entailed by a relation. *) val entails : t -> t -> bool (** Test if one relation entails another. *) -val class_of : t -> Exp.t -> Exp.t list -(** Equivalence class of [e]: all the expressions in [f] in the relation - such that [e = f] is implied by the relation. *) +val class_of : t -> Term.t -> Term.t list +(** Equivalence class of [e]: all the terms [f] in the relation such that [e + = f] is implied by the relation. *) -val normalize : t -> Exp.t -> Exp.t -(** Normalize an exp [e] to [e'] such that [e = e'] is implied by the - relation, where [e'] and its sub-exps are expressed in terms of the +val normalize : t -> Term.t -> Term.t +(** Normalize a term [e] to [e'] such that [e = e'] is implied by the + relation, where [e'] and its subterms are expressed in terms of the relation's canonical representatives of each equivalence class. *) -val difference : t -> Exp.t -> Exp.t -> Z.t option +val difference : t -> Term.t -> Term.t -> Z.t option (** The difference as an offset. [difference r a b = Some k] if [r] implies [a = b+k], or [None] if [a] and [b] are not equal up to an integer offset. *) -val fold_exps : t -> init:'a -> f:('a -> Exp.t -> 'a) -> 'a +val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml index e63fb626f..20327461b 100644 --- a/sledge/src/symbheap/equality_test.ml +++ b/sledge/src/symbheap/equality_test.ml @@ -18,12 +18,12 @@ let%test_module _ = let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r) let i8 = Typ.integer ~bits:8 let i64 = Typ.integer ~bits:64 - let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz - let ( + ) = Exp.add Typ.siz - let ( - ) = Exp.sub Typ.siz - let ( * ) = Exp.mul Typ.siz - let f = Exp.convert ~dst:i64 ~src:i8 - let g = Exp.rem + let ( ! ) i = Term.integer (Z.of_int i) Typ.siz + let ( + ) = Term.add Typ.siz + let ( - ) = Term.sub Typ.siz + let ( * ) = Term.mul Typ.siz + let f = Term.convert ~dst:i64 ~src:i8 + let g = Term.rem let wrt = Var.Set.empty let t_, wrt = Var.fresh "t" ~wrt let u_, wrt = Var.fresh "u" ~wrt @@ -32,13 +32,13 @@ let%test_module _ = let x_, wrt = Var.fresh "x" ~wrt let y_, wrt = Var.fresh "y" ~wrt let z_, _ = Var.fresh "z" ~wrt - let t = Exp.var t_ - let u = Exp.var u_ - let v = Exp.var v_ - let w = Exp.var w_ - let x = Exp.var x_ - let y = Exp.var y_ - let z = Exp.var z_ + let t = Term.var t_ + let u = Term.var u_ + let v = Term.var v_ + let w = Term.var w_ + let x = Term.var x_ + let y = Term.var y_ + let z = Term.var z_ let f1 = of_eqs [(!0, !1)] let%test _ = is_false f1 @@ -212,9 +212,9 @@ let%test_module _ = %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}] let%expect_test _ = - printf (List.pp " , " Exp.pp) (Equality.class_of r7 t) ; - printf (List.pp " , " Exp.pp) (Equality.class_of r7 x) ; - printf (List.pp " , " Exp.pp) (Equality.class_of r7 z) ; + printf (List.pp " , " Term.pp) (Equality.class_of r7 t) ; + printf (List.pp " , " Term.pp) (Equality.class_of r7 x) ; + printf (List.pp " , " Term.pp) (Equality.class_of r7 z) ; [%expect {| %t_1 @@ -235,7 +235,7 @@ let%test_module _ = {sat= true; rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} |}] - let%test _ = normalize r7' w |> Exp.equal v + let%test _ = normalize r7' w |> Term.equal v let%test _ = entails_eq (of_eqs [(g w x, g y z); (x, z)]) (g w x) (g w z) @@ -275,10 +275,10 @@ let%test_module _ = let%expect_test _ = pp_classes r10 ; pp r10 ; - Format.printf "@.%a@." Exp.pp (z - (x + !8)) ; - Format.printf "@.%a@." Exp.pp (normalize r10 (z - (x + !8))) ; - Format.printf "@.%a@." Exp.pp (x + !8 - z) ; - Format.printf "@.%a@." Exp.pp (normalize r10 (x + !8 - z)) ; + Format.printf "@.%a@." Term.pp (z - (x + !8)) ; + Format.printf "@.%a@." Term.pp (normalize r10 (z - (x + !8))) ; + Format.printf "@.%a@." Term.pp (x + !8 - z) ; + Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ; [%expect {| (%z_7 + -16) = %x_5 @@ -308,7 +308,7 @@ let%test_module _ = let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}] - let r13 = of_eqs [(Exp.eq x !2, y); (Exp.dq x !2, z); (y, z)] + let r13 = of_eqs [(Term.eq x !2, y); (Term.dq x !2, z); (y, z)] let%expect_test _ = pp r13 ; @@ -319,15 +319,15 @@ let%test_module _ = let%test _ = not (is_false r13) (* incomplete *) - let a = Exp.dq x !0 + let a = Term.dq x !0 let r14 = of_eqs [(a, a); (x, !1)] let%expect_test _ = pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}] - let%test _ = entails_eq r14 a (Exp.bool true) + let%test _ = entails_eq r14 a (Term.bool true) - let b = Exp.dq y !0 + let b = Term.dq y !0 let r14 = of_eqs [(a, b); (x, !1)] let%expect_test _ = @@ -336,10 +336,10 @@ let%test_module _ = {| {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}] - let%test _ = entails_eq r14 a (Exp.bool true) - let%test _ = entails_eq r14 b (Exp.bool true) + let%test _ = entails_eq r14 a (Term.bool true) + let%test _ = entails_eq r14 b (Term.bool true) - let b = Exp.convert ~dst:i64 ~src:i8 (Exp.dq x !0) + let b = Term.convert ~dst:i64 ~src:i8 (Term.dq x !0) let r15 = of_eqs [(b, b); (x, !1)] let%expect_test _ = diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 3b33e3d46..7e3393c73 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -17,11 +17,13 @@ type xseg = {us: Var.Set.t; xs: Var.Set.t; seg: Sh.seg} let fresh_var nam us xs = let var, us = Var.fresh nam ~wrt:us in - (Exp.var var, us, Set.add xs var) + (Term.var var, us, Set.add xs var) let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us = - let freshen exp nam us xs = - match exp with Some exp -> (exp, us, xs) | None -> fresh_var nam us xs + let freshen term nam us xs = + match term with + | Some term -> (term, us, xs) + | None -> fresh_var nam us xs in let bas, us, xs = freshen bas "b" us xs in let len, us, xs = freshen len "m" us xs in @@ -29,8 +31,8 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us = let arr, us, xs = freshen arr "a" us xs in {us; xs; seg= {loc; bas; len; siz; arr}} -let null_eq ptr = Sh.pure (Exp.eq Exp.null ptr) -let zero = Exp.integer Z.zero Typ.siz +let null_eq ptr = Sh.pure (Term.eq Term.null ptr) +let zero = Term.integer Z.zero Typ.siz (* Overwritten variables renaming and remaining modified variables. [ws] are the written variables; [rs] are the variables read or in the @@ -63,12 +65,12 @@ let move_spec us reg_exps = let ws, rs = Vector.fold reg_exps ~init:(Var.Set.empty, Var.Set.empty) ~f:(fun (ws, rs) (reg, exp) -> - (Set.add ws reg, Set.union rs (Exp.fv exp)) ) + (Set.add ws reg, Set.union rs (Term.fv exp)) ) in let sub, ms, _ = assign ~ws ~rs ~us in let post = Vector.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) -> - Sh.and_ (Exp.eq (Exp.var reg) (Exp.rename sub exp)) post ) + Sh.and_ (Term.eq (Term.var reg) (Term.rename sub exp)) post ) in {xs; foot; sub; ms; post} @@ -82,7 +84,7 @@ let load_spec us reg ptr len = let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in let post = Sh.and_ - (Exp.eq (Exp.var reg) (Exp.rename sub seg.arr)) + (Term.eq (Term.var reg) (Term.rename sub seg.arr)) (Sh.rename sub foot) in {xs; foot; sub; ms; post} @@ -104,7 +106,7 @@ let store_spec us ptr exp len = let memset_spec us dst byt len = let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in let foot = Sh.seg seg in - let post = Sh.seg {seg with arr= Exp.splat ~byt ~siz:len} in + let post = Sh.seg {seg with arr= Term.splat ~byt ~siz:len} in {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ } @@ -115,7 +117,7 @@ let memcpy_eq_spec us dst src len = let {us= _; xs; seg} = fresh_seg ~loc:dst ~len us in let dst_heap = Sh.seg seg in let foot = - Sh.and_ (Exp.eq dst src) (Sh.and_ (Exp.eq len zero) dst_heap) + Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len zero) dst_heap) in let post = dst_heap in {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} @@ -145,7 +147,7 @@ let memcpy_specs us dst src len = let memmov_eq_spec us dst src len = let {us= _; xs; seg= dst_seg} = fresh_seg ~loc:dst ~len us in let dst_heap = Sh.seg dst_seg in - let foot = Sh.and_ (Exp.eq dst src) dst_heap in + let foot = Sh.and_ (Term.eq dst src) dst_heap in let post = dst_heap in {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} @@ -163,17 +165,17 @@ let memmov_foot us dst src len = let arr_dst, us, xs = fresh_var "a" us xs in let arr_mid, us, xs = fresh_var "a" us xs in let arr_src, us, xs = fresh_var "a" us xs in - let src_dst = Exp.sub Typ.siz src dst in - let mem_dst = Exp.memory ~siz:src_dst ~arr:arr_dst in - let siz_mid = Exp.sub Typ.siz len src_dst in - let mem_mid = Exp.memory ~siz:siz_mid ~arr:arr_mid in - let mem_src = Exp.memory ~siz:src_dst ~arr:arr_src in - let mem_dst_mid_src = Exp.concat [|mem_dst; mem_mid; mem_src|] in + let src_dst = Term.sub Typ.siz src dst in + let mem_dst = Term.memory ~siz:src_dst ~arr:arr_dst in + let siz_mid = Term.sub Typ.siz len src_dst in + let mem_mid = Term.memory ~siz:siz_mid ~arr:arr_mid in + let mem_src = Term.memory ~siz:src_dst ~arr:arr_src in + let mem_dst_mid_src = Term.concat [|mem_dst; mem_mid; mem_src|] in let siz_dst_mid_src, us, xs = fresh_var "m" us xs in let arr_dst_mid_src, _, xs = fresh_var "a" us xs in let eq_mem_dst_mid_src = - Exp.eq mem_dst_mid_src - (Exp.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src) + Term.eq mem_dst_mid_src + (Term.memory ~siz:siz_dst_mid_src ~arr:arr_dst_mid_src) in let seg = Sh.seg @@ -181,8 +183,8 @@ let memmov_foot us dst src len = in let foot = Sh.and_ eq_mem_dst_mid_src - (Sh.and_ (Exp.lt dst src) - (Sh.and_ (Exp.lt src (Exp.add Typ.ptr dst len)) seg)) + (Sh.and_ (Term.lt dst src) + (Sh.and_ (Term.lt src (Term.add Typ.ptr dst len)) seg)) in (xs, bas, siz, mem_dst, mem_mid, mem_src, foot) @@ -194,12 +196,12 @@ let memmov_dn_spec us dst src len = let xs, bas, siz, _, mem_mid, mem_src, foot = memmov_foot us dst src len in - let mem_mid_src_src = Exp.concat [|mem_mid; mem_src; mem_src|] in + let mem_mid_src_src = Term.concat [|mem_mid; mem_src; mem_src|] in let siz_mid_src_src, us, xs = fresh_var "m" us xs in let arr_mid_src_src, _, xs = fresh_var "a" us xs in let eq_mem_mid_src_src = - Exp.eq mem_mid_src_src - (Exp.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src) + Term.eq mem_mid_src_src + (Term.memory ~siz:siz_mid_src_src ~arr:arr_mid_src_src) in let post = Sh.and_ eq_mem_mid_src_src @@ -220,12 +222,12 @@ let memmov_up_spec us dst src len = let xs, bas, siz, mem_src, mem_mid, _, foot = memmov_foot us src dst len in - let mem_src_src_mid = Exp.concat [|mem_src; mem_src; mem_mid|] in + let mem_src_src_mid = Term.concat [|mem_src; mem_src; mem_mid|] in let siz_src_src_mid, us, xs = fresh_var "m" us xs in let arr_src_src_mid, _, xs = fresh_var "a" us xs in let eq_mem_src_src_mid = - Exp.eq mem_src_src_mid - (Exp.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid) + Term.eq mem_src_src_mid + (Term.memory ~siz:siz_src_src_mid ~arr:arr_src_src_mid) in let post = Sh.and_ eq_mem_src_src_mid @@ -250,12 +252,12 @@ let memmov_specs us dst src len = *) let alloc_spec us reg num len = let foot = Sh.emp in - let siz = Exp.mul Typ.siz num len in + let siz = Term.mul Typ.siz num len in let sub, ms, us = - assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us + assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in let post = Sh.seg seg in {xs; foot; sub; ms; post} @@ -293,12 +295,12 @@ let dallocx_spec us ptr = let malloc_spec us reg siz = let foot = Sh.emp in let sub, ms, us = - assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us + assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in - let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in + let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in {xs; foot; sub; ms; post} (* { s≠0 } @@ -306,14 +308,14 @@ let malloc_spec us reg siz = * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ } *) let mallocx_spec us reg siz = - let foot = Sh.pure Exp.(dq siz zero) in + let foot = Sh.pure Term.(dq siz zero) in let sub, ms, us = - assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us + assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz us in - let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in + let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in {xs; foot; sub; ms; post} (* { emp } @@ -322,18 +324,18 @@ let mallocx_spec us reg siz = *) let calloc_spec us reg num len = let foot = Sh.emp in - let siz = Exp.mul Typ.siz num len in + let siz = Term.mul Typ.siz num len in let sub, ms, us = - assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Exp.fv siz) ~us + assign ~ws:(Set.add Var.Set.empty reg) ~rs:(Term.fv siz) ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in - let arr = Exp.splat ~byt:(Exp.integer Z.zero Typ.byt) ~siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in + let arr = Term.splat ~byt:(Term.integer Z.zero Typ.byt) ~siz in let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in - let post = Sh.or_ (null_eq (Exp.var reg)) (Sh.seg seg) in + let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in {xs; foot; sub; ms; post} -let size_of_ptr = Option.value_exn (Exp.size_of Typ.ptr) +let size_of_ptr = Option.value_exn (Term.size_of Typ.ptr) (* { p-[_;_)->⟨W,_⟩ } * posix_memalign r p s @@ -347,7 +349,7 @@ let posix_memalign_spec us reg ptr siz = let sub, ms, us = assign ~ws:(Set.add Var.Set.empty reg) - ~rs:(Set.union foot.us (Exp.fv siz)) + ~rs:(Set.union foot.us (Term.fv siz)) ~us in let q, us, xs = fresh_var "q" us xs in @@ -355,13 +357,13 @@ let posix_memalign_spec us reg ptr siz = let {us= _; xs; seg= qseg} = fresh_seg ~loc:q ~bas:q ~len:siz ~siz ~xs us in - let eok = Exp.integer (Z.of_int 0) Typ.int in - let enomem = Exp.integer (Z.of_int 12) Typ.int in + let eok = Term.integer (Z.of_int 0) Typ.int in + let enomem = Term.integer (Z.of_int 12) Typ.int in let post = Sh.or_ - (Sh.and_ (Exp.eq (Exp.var reg) enomem) (Sh.rename sub foot)) + (Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot)) (Sh.and_ - (Exp.eq (Exp.var reg) eok) + (Term.eq (Term.var reg) eok) (Sh.rename sub (Sh.star (Sh.seg pseg') (Sh.seg qseg)))) in {xs; foot; sub; ms; post} @@ -381,20 +383,20 @@ let realloc_spec us reg ptr siz = let sub, ms, us = assign ~ws:(Set.add Var.Set.empty reg) - ~rs:(Set.union foot.us (Exp.fv siz)) + ~rs:(Set.union foot.us (Term.fv siz)) ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in let a0 = pseg.arr in let a1 = rseg.arr in let a2, _, xs = fresh_var "a" us xs in let post = Sh.or_ - (Sh.and_ Exp.(eq loc null) (Sh.rename sub foot)) + (Sh.and_ Term.(eq loc null) (Sh.rename sub foot)) (Sh.and_ - Exp.( + Term.( conditional ~cnd:(le len siz) ~thn: (eq (memory ~siz ~arr:a1) @@ -422,21 +424,21 @@ let rallocx_spec us reg ptr siz = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in let pheap = Sh.seg pseg in - let foot = Sh.and_ Exp.(dq siz zero) pheap in + let foot = Sh.and_ Term.(dq siz zero) pheap in let sub, ms, us = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in + let loc = Term.var reg in + let siz = Term.rename sub siz in let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in let a0 = pseg.arr in let a1 = rseg.arr in let a2, _, xs = fresh_var "a" us xs in let post = Sh.or_ - (Sh.and_ Exp.(eq loc null) (Sh.rename sub pheap)) + (Sh.and_ Term.(eq loc null) (Sh.rename sub pheap)) (Sh.and_ - Exp.( + Term.( conditional ~cnd:(le len siz) ~thn: (eq (memory ~siz ~arr:a1) @@ -460,17 +462,17 @@ let rallocx_spec us reg ptr siz = let xallocx_spec us reg ptr siz ext = let len, us, xs = fresh_var "m" us Var.Set.empty in let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in - let foot = Sh.and_ Exp.(dq siz zero) (Sh.seg seg) in + let foot = Sh.and_ Term.(dq siz zero) (Sh.seg seg) in let sub, ms, us = assign ~ws:(Set.add Var.Set.empty reg) - ~rs:Set.(union foot.us (union (Exp.fv siz) (Exp.fv ext))) + ~rs:Set.(union foot.us (union (Term.fv siz) (Term.fv ext))) ~us in - let reg = Exp.var reg in - let ptr = Exp.rename sub ptr in - let siz = Exp.rename sub siz in - let ext = Exp.rename sub ext in + let reg = Term.var reg in + let ptr = Term.rename sub ptr in + let siz = Term.rename sub siz in + let ext = Term.rename sub ext in let {us; xs; seg= seg'} = fresh_seg ~loc:ptr ~bas:ptr ~len:reg ~siz:reg ~xs us in @@ -479,7 +481,7 @@ let xallocx_spec us reg ptr siz ext = let a2, _, xs = fresh_var "a" us xs in let post = Sh.and_ - Exp.( + Term.( and_ (conditional ~cnd:(le len siz) ~thn: @@ -506,7 +508,7 @@ let sallocx_spec us reg ptr = let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in let foot = Sh.seg seg in let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in - let post = Sh.and_ Exp.(eq (var reg) len) (Sh.rename sub foot) in + let post = Sh.and_ Term.(eq (var reg) len) (Sh.rename sub foot) in {xs; foot; sub; ms; post} (* { p-[p;m)->⟨m,α⟩ } @@ -518,7 +520,7 @@ let malloc_usable_size_spec us reg ptr = let {us; xs; seg} = fresh_seg ~loc:ptr ~bas:ptr ~len ~siz:len ~xs us in let foot = Sh.seg seg in let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in - let post = Sh.and_ Exp.(le len (var reg)) (Sh.rename sub foot) in + let post = Sh.and_ Term.(le len (var reg)) (Sh.rename sub foot) in {xs; foot; sub; ms; post} (* { s≠0 } @@ -527,15 +529,15 @@ let malloc_usable_size_spec us reg ptr = *) let nallocx_spec us reg siz = let xs = Var.Set.empty in - let foot = Sh.pure (Exp.dq siz zero) in + let foot = Sh.pure (Term.dq siz zero) in let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in - let loc = Exp.var reg in - let siz = Exp.rename sub siz in - let post = Sh.or_ (null_eq loc) (Sh.pure (Exp.eq loc siz)) in + let loc = Term.var reg in + let siz = Term.rename sub siz in + let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in {xs; foot; sub; ms; post} let size_of_int_mul n = - Exp.mul Typ.siz (Option.value_exn (Exp.size_of Typ.siz)) n + Term.mul Typ.siz (Option.value_exn (Term.size_of Typ.siz)) n (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 } * mallctl r i w n @@ -547,8 +549,8 @@ let mallctl_read_spec us r i w n = let a, _, xs = fresh_var "a" us xs in let foot = Sh.and_ - Exp.(eq w null) - (Sh.and_ Exp.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg))) + Term.(eq w null) + (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg))) in let rseg' = {rseg with arr= a} in let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in @@ -569,8 +571,8 @@ let mallctlbymib_read_spec us p l r i w n = let a, _, xs = fresh_var "a" us xs in let foot = Sh.and_ - Exp.(eq w null) - (Sh.and_ Exp.(eq n zero) (Sh.star const (Sh.seg rseg))) + Term.(eq w null) + (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg))) in let rseg' = {rseg with arr= a} in let post = Sh.star (Sh.seg rseg') const in @@ -583,7 +585,7 @@ let mallctlbymib_read_spec us p l r i w n = let mallctl_write_spec us r i w n = let {us= _; xs; seg} = fresh_seg ~loc:w ~siz:n us in let post = Sh.seg seg in - let foot = Sh.and_ Exp.(eq r null) (Sh.and_ Exp.(eq i zero) post) in + let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} (* { p-[_;_)->⟨W×l,_⟩ * r=0 * i=0 * w-[_;_)->⟨n,_⟩ } @@ -596,7 +598,7 @@ let mallctlbymib_write_spec us p l r i w n = let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in let {us= _; xs; seg= wseg} = fresh_seg ~loc:w ~siz:n ~xs us in let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in - let foot = Sh.and_ Exp.(eq r null) (Sh.and_ Exp.(eq i zero) post) in + let foot = Sh.and_ Term.(eq r null) (Sh.and_ Term.(eq i zero) post) in {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} let mallctl_specs us r i w n = @@ -641,12 +643,14 @@ let strlen_spec us reg ptr = let sub, ms, _ = assign ~ws:(Set.add Var.Set.empty reg) ~rs:foot.us ~us in let {Sh.loc= p; bas= b; len= m; _} = seg in let ret = - Exp.sub Typ.siz - (Exp.sub Typ.siz (Exp.add Typ.siz b m) p) - (Exp.integer Z.one Typ.siz) + Term.sub Typ.siz + (Term.sub Typ.siz (Term.add Typ.siz b m) p) + (Term.integer Z.one Typ.siz) in let post = - Sh.and_ (Exp.eq (Exp.var reg) (Exp.rename sub ret)) (Sh.rename sub foot) + Sh.and_ + (Term.eq (Term.var reg) (Term.rename sub ret)) + (Sh.rename sub foot) in {xs; foot; sub; ms; post} @@ -705,20 +709,38 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result = fun pre inst -> [%Trace.info "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ; - assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ; + assert ( + Set.disjoint (Sh.fv pre) (Var.Set.of_regs (Llair.Inst.locals inst)) ) ; let us = pre.us in match inst with - | Move {reg_exps; _} -> exec_spec pre (move_spec us reg_exps) - | Load {reg; ptr; len; _} -> exec_spec pre (load_spec us reg ptr len) - | Store {ptr; exp; len; _} -> exec_spec pre (store_spec us ptr exp len) - | Memset {dst; byt; len; _} -> exec_spec pre (memset_spec us dst byt len) + | Move {reg_exps; _} -> + exec_spec pre + (move_spec us + (Vector.map reg_exps ~f:(fun (r, e) -> + (Var.of_reg r, Term.of_exp e) ))) + | Load {reg; ptr; len; _} -> + exec_spec pre + (load_spec us (Var.of_reg reg) (Term.of_exp ptr) (Term.of_exp len)) + | Store {ptr; exp; len; _} -> + exec_spec pre + (store_spec us (Term.of_exp ptr) (Term.of_exp exp) (Term.of_exp len)) + | Memset {dst; byt; len; _} -> + exec_spec pre + (memset_spec us (Term.of_exp dst) (Term.of_exp byt) + (Term.of_exp len)) | Memcpy {dst; src; len; _} -> - exec_specs pre (memcpy_specs us dst src len) + exec_specs pre + (memcpy_specs us (Term.of_exp dst) (Term.of_exp src) + (Term.of_exp len)) | Memmov {dst; src; len; _} -> - exec_specs pre (memmov_specs us dst src len) - | Alloc {reg; num; len; _} -> exec_spec pre (alloc_spec us reg num len) - | Free {ptr; _} -> exec_spec pre (free_spec us ptr) - | Nondet {reg= Some reg; _} -> Ok (kill pre reg) + exec_specs pre + (memmov_specs us (Term.of_exp dst) (Term.of_exp src) + (Term.of_exp len)) + | Alloc {reg; num; len; _} -> + exec_spec pre + (alloc_spec us (Var.of_reg reg) (Term.of_exp num) (Term.of_exp len)) + | Free {ptr; _} -> exec_spec pre (free_spec us (Term.of_exp ptr)) + | Nondet {reg= Some reg; _} -> Ok (kill pre (Var.of_reg reg)) | Nondet {reg= None; _} -> Ok pre | Abort _ -> Error () @@ -728,13 +750,13 @@ let intrinsic ~skip_throw : Sh.t -> Var.t option -> Var.t - -> Exp.t list + -> Term.t list -> (Sh.t, unit) result option = fun pre areturn intrinsic actuals -> [%Trace.info "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]" (Option.pp "%a := " Var.pp) - areturn Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals) + areturn Var.pp intrinsic (List.pp ",@ " Term.pp) (List.rev actuals) Sh.pp pre] ; let us = pre.us in let name = diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index c379acc39..f91ce13c8 100644 --- a/sledge/src/symbheap/exec.mli +++ b/sledge/src/symbheap/exec.mli @@ -7,9 +7,9 @@ (** Symbolic Execution *) -val assume : Sh.t -> Exp.t -> Sh.t option +val assume : Sh.t -> Term.t -> Sh.t option val kill : Sh.t -> Var.t -> Sh.t -val move : Sh.t -> Var.t -> Exp.t -> Sh.t +val move : Sh.t -> Var.t -> Term.t -> Sh.t val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result val intrinsic : @@ -17,5 +17,5 @@ val intrinsic : -> Sh.t -> Var.t option -> Var.t - -> Exp.t list + -> Term.t list -> (Sh.t, unit) result option diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 7ac767768..5ee90ae70 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -9,14 +9,14 @@ [@@@warning "+9"] -type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t} +type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t} [@@deriving compare, equal, sexp] type starjunction = { us: Var.Set.t ; xs: Var.Set.t ; cong: Equality.t - ; pure: Exp.t list + ; pure: Term.t list ; heap: seg list ; djns: disjunction list } [@@deriving compare, equal, sexp] @@ -29,12 +29,12 @@ let map_seg {loc; bas; len; siz; arr} ~f = {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr} let pp_seg ?is_x fs {loc; bas; len; siz; arr} = - let exp_pp = Exp.pp_full ?is_x in - Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" exp_pp loc + let term_pp = Term.pp_full ?is_x in + Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc (fun fs (bas, len) -> - if (not (Exp.equal loc bas)) || not (Exp.equal len siz) then - Format.fprintf fs " %a, %a " exp_pp bas exp_pp len ) - (bas, len) exp_pp (Exp.memory ~siz ~arr) + if (not (Term.equal loc bas)) || not (Term.equal len siz) then + Format.fprintf fs " %a, %a " term_pp bas term_pp len ) + (bas, len) term_pp (Term.memory ~siz ~arr) let pp_seg_norm cong fs seg = pp_seg fs (map_seg seg ~f:(Equality.normalize cong)) @@ -46,7 +46,7 @@ let pp_us ?(pre = ("" : _ fmt)) fs us = let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} = Format.pp_open_hvbox fs 0 ; let all_xs = Set.union all_xs xs in - let is_x var = Set.mem all_xs (Option.value_exn (Var.of_exp var)) in + let is_x var = Set.mem all_xs (Option.value_exn (Var.of_term var)) in pp_us fs us ; let xs_i_vs, xs_d_vs = Set.inter_diff vs xs in if not (Set.is_empty xs_i_vs) then ( @@ -57,15 +57,15 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} = let first = Equality.is_true cong in if not first then Format.fprintf fs " " ; Equality.pp_classes ~is_x fs cong ; - let pure_exps = + let pure_terms = List.filter_map pure ~f:(fun e -> let e' = Equality.normalize cong e in - if Exp.is_true e' then None else Some e' ) + if Term.is_true e' then None else Some e' ) in List.pp ~pre:(if first then " " else "@ @<2>∧ ") - "@ @<2>∧ " (Exp.pp_full ~is_x) fs pure_exps ; - let first = first && List.is_empty pure_exps in + "@ @<2>∧ " (Term.pp_full ~is_x) fs pure_terms ; + let first = first && List.is_empty pure_terms in if List.is_empty heap then Format.fprintf fs ( if first then if List.is_empty djns then " emp" else "" @@ -78,11 +78,12 @@ let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} = (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap) ~compare:(fun s1 s2 -> let b_o = function - | Exp.App {op= App {op= Add _; arg}; arg= Integer {data; _}} -> + | Term.App {op= App {op= Add _; arg}; arg= Integer {data; _}} + -> (arg, data) | e -> (e, Z.zero) in - [%compare: Exp.t * (Exp.t * Z.t)] + [%compare: Term.t * (Term.t * Z.t)] (s1.bas, b_o s1.loc) (s2.bas, b_o s2.loc) )) ; let first = first && List.is_empty heap in @@ -105,34 +106,34 @@ and pp_djn vs all_xs fs = function let pp = pp Var.Set.empty Var.Set.empty let pp_djn = pp_djn Var.Set.empty Var.Set.empty -let fold_exps_seg {loc; bas; len; siz; arr} ~init ~f = - let f b z = Exp.fold_exps b ~init:z ~f in +let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f = + let f b z = Term.fold_terms b ~init:z ~f in f loc (f bas (f len (f siz (f arr init)))) let fold_vars_seg seg ~init ~f = - fold_exps_seg seg ~init ~f:(fun init -> Exp.fold_vars ~f ~init) + fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init) let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty -let fold_exps fold_exps {us= _; xs= _; cong; pure; heap; djns} ~init ~f = - Equality.fold_exps ~init cong ~f +let fold_terms fold_terms {us= _; xs= _; cong; pure; heap; djns} ~init ~f = + Equality.fold_terms ~init cong ~f |> fun init -> - List.fold ~init pure ~f:(fun init -> Exp.fold_exps ~f ~init) + List.fold ~init pure ~f:(fun init -> Term.fold_terms ~f ~init) |> fun init -> - List.fold ~init heap ~f:(fun init -> fold_exps_seg ~f ~init) + List.fold ~init heap ~f:(fun init -> fold_terms_seg ~f ~init) |> fun init -> - List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_exps) + List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_terms) let rec fv_union init q = Set.diff - (fold_exps fv_union q ~init ~f:(fun init -> - Exp.fold_vars ~f:Set.add ~init )) + (fold_terms fv_union q ~init ~f:(fun init -> + Term.fold_vars ~f:Set.add ~init )) q.xs let fv q = fv_union Var.Set.empty q let invariant_pure = function - | Exp.Integer {data; typ} -> + | Term.Integer {data; typ} -> assert (Typ.equal Typ.bool typ) ; assert (not (Z.is_false data)) | _ -> assert true @@ -186,11 +187,11 @@ let rec simplify {us; xs; cong; pure; heap; djns} = (** Quantification and Vocabulary *) let rename_seg sub ({loc; bas; len; siz; arr} as h) = - let loc = Exp.rename sub loc in - let bas = Exp.rename sub bas in - let len = Exp.rename sub len in - let siz = Exp.rename sub siz in - let arr = Exp.rename sub arr in + let loc = Term.rename sub loc in + let bas = Term.rename sub bas in + let len = Term.rename sub len in + let siz = Term.rename sub siz in + let arr = Term.rename sub arr in ( if loc == h.loc && bas == h.bas && len == h.len && siz == h.siz && arr == h.arr @@ -203,7 +204,7 @@ let rename_seg sub ({loc; bas; len; siz; arr} as h) = invariant *) let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) = let cong = Equality.rename cong sub in - let pure = List.map_preserving_phys_equal pure ~f:(Exp.rename sub) in + let pure = List.map_preserving_phys_equal pure ~f:(Term.rename sub) in let heap = List.map_preserving_phys_equal heap ~f:(rename_seg sub) in let djns = List.map_preserving_phys_equal djns ~f:(fun d -> @@ -375,10 +376,10 @@ let or_ q1 q2 = invariant q ; assert (Set.equal q.us (Set.union q1.us q2.us))] -let rec pure (e : Exp.t) = - [%Trace.call fun {pf} -> pf "%a" Exp.pp e] +let rec pure (e : Term.t) = + [%Trace.call fun {pf} -> pf "%a" Term.pp e] ; - let us = Exp.fv e in + let us = Term.fv e in ( match e with | Integer {data; typ= Integer {bits= 1}} -> if Z.is_false data then false_ us else emp @@ -388,7 +389,7 @@ let rec pure (e : Exp.t) = -> or_ (star (pure cnd) (pure thn)) - (star (pure (Exp.not_ Typ.bool cnd)) (pure els)) + (star (pure (Term.not_ Typ.bool cnd)) (pure els)) | App {op= App {op= Eq; arg= e1}; arg= e2} -> let cong = Equality.(and_eq e1 e2 true_) in if Equality.is_false cong then false_ us @@ -401,7 +402,7 @@ let and_ e q = star (pure e) q let seg pt = let us = fv_seg pt in - if Exp.equal Exp.null pt.loc then false_ us + if Term.equal Term.null pt.loc then false_ us else {emp with us; heap= [pt]} |> check invariant (** Update *) @@ -423,9 +424,10 @@ let is_emp = function let is_false = function | {djns= [[]]; _} -> true | {cong; pure; heap; _} -> - List.exists pure ~f:(fun b -> Exp.is_false (Equality.normalize cong b)) + List.exists pure ~f:(fun b -> + Term.is_false (Equality.normalize cong b) ) || List.exists heap ~f:(fun seg -> - Equality.entails_eq cong seg.loc Exp.null ) + Equality.entails_eq cong seg.loc Term.null ) let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) = let heap = emp.heap in diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index 94198f72f..c8a61a992 100644 --- a/sledge/src/symbheap/sh.mli +++ b/sledge/src/symbheap/sh.mli @@ -11,13 +11,13 @@ size [siz], contained in an enclosing allocation-block starting at [bas] of length [len]. Byte-array expressions are either [Var]iables or [Splat] vectors. *) -type seg = {loc: Exp.t; bas: Exp.t; len: Exp.t; siz: Exp.t; arr: Exp.t} +type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t} type starjunction = private { us: Var.Set.t (** vocabulary / variable context of formula *) ; xs: Var.Set.t (** existentially-bound variables *) ; cong: Equality.t (** congruence induced by rest of formula *) - ; pure: Exp.t list (** conjunction of pure boolean constraints *) + ; pure: Term.t list (** conjunction of pure boolean constraints *) ; heap: seg list (** star-conjunction of segment atomic formulas *) ; djns: disjunction list (** star-conjunction of disjunctions *) } @@ -25,7 +25,7 @@ and disjunction = starjunction list type t = starjunction [@@deriving equal, compare, sexp] -val pp_seg : ?is_x:(Exp.t -> bool) -> seg pp +val pp_seg : ?is_x:(Term.t -> bool) -> seg pp val pp_seg_norm : Equality.t -> seg pp val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp val pp : t pp @@ -53,10 +53,10 @@ val or_ : t -> t -> t (** Disjoin formulas, extending to a common vocabulary, and avoiding capturing existentials. *) -val pure : Exp.t -> t +val pure : Term.t -> t (** Atomic pure boolean constraint formula. *) -val and_ : Exp.t -> t -> t +val and_ : Term.t -> t -> t (** Conjoin a boolean constraint to a formula. *) val and_cong : Equality.t -> t -> t @@ -65,7 +65,7 @@ val and_cong : Equality.t -> t -> t (** Update *) -val with_pure : Exp.t list -> t -> t +val with_pure : Term.t list -> t -> t (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and [pure] are defined in the same vocabulary, induce the same congruence, etc. It can essentially only be used when [pure] is logically equivalent diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index 391b406b9..2cbd543ba 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -19,29 +19,38 @@ let report_fmt_thunk = Fn.flip pp let init globals = Vector.fold globals ~init:Sh.emp ~f:(fun q -> function - | {Global.var; init= Some (arr, siz)} -> - let loc = Exp.var var in - let len = Exp.integer (Z.of_int siz) Typ.siz in + | {Global.reg; init= Some (arr, siz)} -> + let loc = Term.var (Var.of_reg reg) in + let len = Term.integer (Z.of_int siz) Typ.siz in + let arr = Term.of_exp arr in Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr}) | _ -> q ) let join l r = Some (Sh.or_ l r) let is_false = Sh.is_false -let exec_assume = Exec.assume -let exec_kill = Exec.kill -let exec_move = Exec.move +let exec_assume q b = Exec.assume q (Term.of_exp b) +let exec_kill q r = Exec.kill q (Var.of_reg r) +let exec_move q r e = Exec.move q (Var.of_reg r) (Term.of_exp e) let exec_inst = Exec.inst -let exec_intrinsic = Exec.intrinsic + +let exec_intrinsic ~skip_throw q r i es = + Exec.intrinsic ~skip_throw q + (Option.map ~f:Var.of_reg r) + (Var.of_reg i) + (List.map ~f:Term.of_exp es) + let dnf = Sh.dnf -let exp_eq_class_has_only_vars_in fvs cong exp = +let term_eq_class_has_only_vars_in fvs cong term = [%Trace.call fun {pf} -> - pf "@[ fvs: @[%a@] @,cong: @[%a@] @,exp: @[%a@]@]" Var.Set.pp fvs - Equality.pp cong Exp.pp exp] + pf "@[ fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs + Equality.pp cong Term.pp term] ; - let exp_has_only_vars_in fvs exp = Set.is_subset (Exp.fv exp) ~of_:fvs in - let exp_eq_class = Equality.class_of cong exp in - List.exists ~f:(exp_has_only_vars_in fvs) exp_eq_class + let term_has_only_vars_in fvs term = + Set.is_subset (Term.fv term) ~of_:fvs + in + let term_eq_class = Equality.class_of cong term in + List.exists ~f:(term_has_only_vars_in fvs) term_eq_class |> [%Trace.retn fun {pf} -> pf "%b"] @@ -55,16 +64,16 @@ let garbage_collect (q : t) ~wrt = else let new_set = List.fold ~init:current q.heap ~f:(fun current seg -> - if exp_eq_class_has_only_vars_in current q.cong seg.loc then + if term_eq_class_has_only_vars_in current q.cong seg.loc then List.fold (Equality.class_of q.cong seg.arr) ~init:current - ~f:(fun c e -> Set.union c (Exp.fv e)) + ~f:(fun c e -> Set.union c (Term.fv e)) else current ) in all_reachable_vars current new_set q in let r_vars = all_reachable_vars Var.Set.empty wrt q in Sh.filter_heap q ~f:(fun seg -> - exp_eq_class_has_only_vars_in r_vars q.cong seg.loc ) + term_eq_class_has_only_vars_in r_vars q.cong seg.loc ) |> [%Trace.retn fun {pf} -> pf "%a" pp] @@ -79,15 +88,19 @@ let call ~summaries ~globals actuals areturn formals ~locals q = pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \ globals: {@[%a@]}@ q: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Var.Set.pp locals Var.Set.pp globals pp q] + (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp) + (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q] ; + let actuals = List.map ~f:Term.of_exp actuals in + let areturn = Option.map ~f:Var.of_reg areturn in + let formals = List.map ~f:Var.of_reg formals in + let locals = Var.Set.of_regs locals in let q', freshen_locals = Sh.freshen q ~wrt:(Set.add_list formals locals) in let and_eq q formal actual = - let actual' = Exp.rename freshen_locals actual in - Sh.and_ (Exp.eq (Exp.var formal) actual') q + let actual' = Term.rename freshen_locals actual in + Sh.and_ (Term.eq (Term.var formal) actual') q in let and_eqs formals actuals q = List.fold2_exn ~f:and_eq formals actuals ~init:q @@ -101,7 +114,8 @@ let call ~summaries ~globals actuals areturn formals ~locals q = them *) let formals_set = Var.Set.of_list formals in let function_summary_pre = - garbage_collect q'' ~wrt:(Set.union formals_set globals) + garbage_collect q'' + ~wrt:(Set.union formals_set (Var.Set.of_regs globals)) in [%Trace.info "function summary pre %a" pp function_summary_pre] ; let foot = Sh.exists formals_set function_summary_pre in @@ -124,8 +138,9 @@ let recursion_beyond_bound = `prune (** Leave scope of locals: existentially quantify locals. *) let post locals _ q = [%Trace.call fun {pf} -> - pf "@[locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q] + pf "@[locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q] ; + let locals = Var.Set.of_regs locals in Sh.exists locals q |> [%Trace.retn fun {pf} -> pf "%a" Sh.pp] @@ -136,13 +151,15 @@ let post locals _ q = let retn formals freturn {areturn; subst; frame} q = [%Trace.call fun {pf} -> pf "@[formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]" - (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp + (List.pp ", " Reg.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] ; + let formals = List.map ~f:Var.of_reg formals in + let freturn = Option.map ~f:Var.of_reg freturn in let q = match (areturn, freturn) with - | Some areturn, Some freturn -> exec_move q areturn (Exp.var freturn) - | Some areturn, None -> exec_kill q areturn + | Some areturn, Some freturn -> Exec.move q areturn (Term.var freturn) + | Some areturn, None -> Exec.kill q areturn | _ -> q in let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in @@ -152,8 +169,8 @@ let retn formals freturn {areturn; subst; frame} q = [%Trace.retn fun {pf} -> pf "%a" pp] let resolve_callee lookup ptr q = - match Var.of_exp ptr with - | Some callee -> (lookup (Var.name callee), q) + match Reg.of_exp ptr with + | Some callee -> (lookup (Reg.name callee), q) | None -> ([], q) type summary = {xs: Var.Set.t; foot: t; post: t} @@ -164,16 +181,18 @@ let pp_summary fs {xs; foot; post} = let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = [%Trace.call fun {pf} -> - pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp + pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp post] ; + let locals = Var.Set.of_regs locals in + let formals = Var.Set.of_regs formals in let foot = Sh.exists locals entry in let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in let restore_formals q = Set.fold formals ~init:q ~f:(fun q var -> - let var = Exp.var var in - let renamed_var = Exp.rename subst var in - Sh.and_ (Exp.eq renamed_var var) q ) + let var = Term.var var in + let renamed_var = Term.rename subst var in + Sh.and_ (Term.eq renamed_var var) q ) in (* Add back the original formals name *) let post = Sh.rename subst post in @@ -227,11 +246,11 @@ let%test_module _ = let n_, wrt = Var.fresh "n" ~wrt let b_, wrt = Var.fresh "b" ~wrt let end_, _ = Var.fresh "end" ~wrt - let a = Exp.var a_ - let main = Exp.var main_ - let b = Exp.var b_ - let n = Exp.var n_ - let endV = Exp.var end_ + let a = Term.var a_ + let main = Term.var main_ + let b = Term.var b_ + let n = Term.var n_ + let endV = Term.var end_ let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a} let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV} let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main} diff --git a/sledge/src/symbheap/sh_domain.mli b/sledge/src/symbheap/sh_domain.mli index 3f6e03004..9a7260bbf 100644 --- a/sledge/src/symbheap/sh_domain.mli +++ b/sledge/src/symbheap/sh_domain.mli @@ -10,10 +10,10 @@ include Domain_sig.Dom (* formals should include all the parameters of the summary. That is both - formals and globals.*) + formals and globals. *) val create_summary : - locals:Var.Set.t - -> formals:Var.Set.t + locals:Reg.Set.t + -> formals:Reg.Set.t -> entry:t -> current:t -> summary * t diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml index 3cb8be62d..0e6cab0ca 100644 --- a/sledge/src/symbheap/sh_test.ml +++ b/sledge/src/symbheap/sh_test.ml @@ -13,13 +13,13 @@ let%test_module _ = let pp = Format.printf "@\n%a@." Sh.pp let pp_djn = Format.printf "@\n%a@." Sh.pp_djn let ( ~$ ) = Var.Set.of_list - let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz - let ( = ) = Exp.eq + let ( ! ) i = Term.integer (Z.of_int i) Typ.siz + let ( = ) = Term.eq let wrt = Var.Set.empty let x_, wrt = Var.fresh "x" ~wrt let y_, _ = Var.fresh "y" ~wrt - let x = Exp.var x_ - let y = Exp.var y_ + let x = Term.var x_ + let y = Term.var y_ let%expect_test _ = let p = Sh.(exists ~$[x_] (extend_us ~$[x_] emp)) in diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 68ecaceb3..b1f0c1cda 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -44,15 +44,15 @@ let fresh_var name vs zs ~wrt = let v, wrt = Var.fresh name ~wrt in let vs = Set.add vs v in let zs = Set.add zs v in - let v = Exp.var v in + let v = Term.var v in (v, vs, zs, wrt) type occurrences = Zero | One of Var.t | Many -let single_existential_occurrence xs exp = +let single_existential_occurrence xs term = let exception Multiple_existential_occurrences in try - Exp.fold_vars exp ~init:Zero ~f:(fun seen var -> + Term.fold_vars term ~init:Zero ~f:(fun seen var -> if not (Set.mem xs var) then seen else match seen with @@ -61,32 +61,32 @@ let single_existential_occurrence xs exp = with Multiple_existential_occurrences -> Many let special_cases xs = function - | Exp.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e -> - if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e + | Term.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e -> + if Set.is_subset (Term.fv e) ~of_:xs then Term.bool true else e | e -> e -let excise_exp ({us; min; xs} as goal) pure exp = - let exp' = Equality.normalize min.cong exp in - let exp' = special_cases xs exp' in - [%Trace.info "exp': %a" Exp.pp exp'] ; - if Exp.is_true exp' then Some ({goal with pgs= true}, pure) +let excise_term ({us; min; xs} as goal) pure term = + let term' = Equality.normalize min.cong term in + let term' = special_cases xs term' in + [%Trace.info "term': %a" Term.pp term'] ; + if Term.is_true term' then Some ({goal with pgs= true}, pure) else - match single_existential_occurrence xs exp' with + match single_existential_occurrence xs term' with | Zero -> None | One x -> Some ( { goal with us= Set.add us x - ; min= Sh.and_ exp' min + ; min= Sh.and_ term' min ; xs= Set.remove xs x ; pgs= true } , pure ) - | Many -> Some (goal, exp' :: pure) + | Many -> Some (goal, term' :: pure) let excise_pure ({sub} as goal) = [%Trace.info "@[<2>excise_pure@ %a@]" pp goal] ; - List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) exp -> - excise_exp goal pure exp ) + List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term -> + excise_term goal pure term ) >>| fun (goal, pure) -> {goal with sub= Sh.with_pure pure sub} (* [k; o) @@ -111,8 +111,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg = let com = Sh.star (Sh.seg msg) com in let min = Sh.rem_seg msg min in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a a') (Sh.rem_seg ssg sub))) + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a a') (Sh.rem_seg ssg sub))) in {goal with com; min; sub} @@ -136,24 +136,24 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in - let o_n = Exp.integer o_n Typ.siz in + let o_n = Term.integer o_n Typ.siz in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in let min = Sh.and_ - (Exp.eq - (Exp.memory ~siz:o ~arr:a) - (Exp.concat - [|Exp.memory ~siz:n ~arr:a0; Exp.memory ~siz:o_n ~arr:a1|])) + (Term.eq + (Term.memory ~siz:o ~arr:a) + (Term.concat + [|Term.memory ~siz:n ~arr:a0; Term.memory ~siz:o_n ~arr:a1|])) (Sh.star (Sh.seg - {loc= Exp.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1}) + {loc= Term.add Typ.ptr k n; bas= b; len= m; siz= o_n; arr= a1}) (Sh.rem_seg msg min)) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a0 a') (Sh.rem_seg ssg sub))) + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a0 a') (Sh.rem_seg ssg sub))) in {goal with us; com; min; sub; zs} @@ -178,21 +178,22 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let n_o = Exp.integer n_o Typ.siz in + let n_o = Term.integer n_o Typ.siz in let com = Sh.star (Sh.seg msg) com in let min = Sh.rem_seg msg min in let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Set.union us xs) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ - (Exp.eq - (Exp.concat - [|Exp.memory ~siz:o ~arr:a; Exp.memory ~siz:n_o ~arr:a1'|]) - (Exp.memory ~siz:n ~arr:a')) + (Term.eq + (Term.concat + [| Term.memory ~siz:o ~arr:a + ; Term.memory ~siz:n_o ~arr:a1' |]) + (Term.memory ~siz:n ~arr:a')) (Sh.star (Sh.seg - { loc= Exp.add Typ.ptr l o + { loc= Term.add Typ.ptr l o ; bas= b' ; len= m' ; siz= n_o @@ -221,7 +222,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let l_k = Exp.integer l_k Typ.siz in + let l_k = Term.integer l_k Typ.siz in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in let com = @@ -229,17 +230,17 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Exp.eq - (Exp.memory ~siz:o ~arr:a) - (Exp.concat - [|Exp.memory ~siz:l_k ~arr:a0; Exp.memory ~siz:n ~arr:a1|])) + (Term.eq + (Term.memory ~siz:o ~arr:a) + (Term.concat + [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:n ~arr:a1|])) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.rem_seg msg min)) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a1 a') (Sh.rem_seg ssg sub))) + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub))) in {goal with us; com; min; sub; zs} @@ -264,8 +265,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let l_k = Exp.integer l_k Typ.siz and ko_ln = Exp.integer ko_ln Typ.siz in - let ln = Exp.add Typ.ptr l n in + let l_k = Term.integer l_k Typ.siz + and ko_ln = Term.integer ko_ln Typ.siz in + let ln = Term.add Typ.ptr l n in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in @@ -274,12 +276,12 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Exp.eq - (Exp.memory ~siz:o ~arr:a) - (Exp.concat - [| Exp.memory ~siz:l_k ~arr:a0 - ; Exp.memory ~siz:n ~arr:a1 - ; Exp.memory ~siz:ko_ln ~arr:a2 |])) + (Term.eq + (Term.memory ~siz:o ~arr:a) + (Term.concat + [| Term.memory ~siz:l_k ~arr:a0 + ; Term.memory ~siz:n ~arr:a1 + ; Term.memory ~siz:ko_ln ~arr:a2 |])) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.star @@ -287,8 +289,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k (Sh.rem_seg msg min))) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') (Sh.and_ (Exp.eq a1 a') (Sh.rem_seg ssg sub))) + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub))) in {goal with us; com; min; sub; zs} @@ -313,10 +315,10 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let l_k = Exp.integer l_k Typ.siz in - let ko_l = Exp.integer ko_l Typ.siz in - let ln_ko = Exp.integer ln_ko Typ.siz in - let ko = Exp.add Typ.ptr k o in + let l_k = Term.integer l_k Typ.siz in + let ko_l = Term.integer ko_l Typ.siz in + let ln_ko = Term.integer ln_ko Typ.siz in + let ko = Term.add Typ.ptr k o in let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Set.union us xs) in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in @@ -325,23 +327,23 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k in let min = Sh.and_ - (Exp.eq - (Exp.memory ~siz:o ~arr:a) - (Exp.concat - [|Exp.memory ~siz:l_k ~arr:a0; Exp.memory ~siz:ko_l ~arr:a1|])) + (Term.eq + (Term.memory ~siz:o ~arr:a) + (Term.concat + [|Term.memory ~siz:l_k ~arr:a0; Term.memory ~siz:ko_l ~arr:a1|])) (Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0}) (Sh.rem_seg msg min)) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ - (Exp.eq - (Exp.concat - [| Exp.memory ~siz:ko_l ~arr:a1 - ; Exp.memory ~siz:ln_ko ~arr:a2' |]) - (Exp.memory ~siz:n ~arr:a')) + (Term.eq + (Term.concat + [| Term.memory ~siz:ko_l ~arr:a1 + ; Term.memory ~siz:ln_ko ~arr:a2' |]) + (Term.memory ~siz:n ~arr:a')) (Sh.star (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'}) (Sh.rem_seg ssg sub)))) @@ -369,18 +371,19 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let k_l = Exp.integer k_l Typ.siz in + let k_l = Term.integer k_l Typ.siz in let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let com = Sh.star (Sh.seg msg) com in let min = Sh.rem_seg msg min in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ - (Exp.eq - (Exp.concat - [|Exp.memory ~siz:k_l ~arr:a0'; Exp.memory ~siz:o ~arr:a|]) - (Exp.memory ~siz:n ~arr:a')) + (Term.eq + (Term.concat + [| Term.memory ~siz:k_l ~arr:a0' + ; Term.memory ~siz:o ~arr:a |]) + (Term.memory ~siz:n ~arr:a')) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.rem_seg ssg sub)))) @@ -409,23 +412,23 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let k_l = Exp.integer k_l Typ.siz in - let ln_ko = Exp.integer ln_ko Typ.siz in - let ko = Exp.add Typ.ptr k o in + let k_l = Term.integer k_l Typ.siz in + let ln_ko = Term.integer ln_ko Typ.siz in + let ko = Term.add Typ.ptr k o in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in let com = Sh.star (Sh.seg msg) com in let min = Sh.rem_seg msg min in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ - (Exp.eq - (Exp.concat - [| Exp.memory ~siz:k_l ~arr:a0' - ; Exp.memory ~siz:o ~arr:a - ; Exp.memory ~siz:ln_ko ~arr:a2' |]) - (Exp.memory ~siz:n ~arr:a')) + (Term.eq + (Term.concat + [| Term.memory ~siz:k_l ~arr:a0' + ; Term.memory ~siz:o ~arr:a + ; Term.memory ~siz:ln_ko ~arr:a2' |]) + (Term.memory ~siz:n ~arr:a')) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.star @@ -455,10 +458,10 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in - let k_l = Exp.integer k_l Typ.siz in - let ln_k = Exp.integer ln_k Typ.siz in - let ko_ln = Exp.integer ko_ln Typ.siz in - let ln = Exp.add Typ.ptr l n in + let k_l = Term.integer k_l Typ.siz in + let ln_k = Term.integer ln_k Typ.siz in + let ko_ln = Term.integer ko_ln Typ.siz in + let ln = Term.add Typ.ptr l n in let a0', xs, zs, wrt = fresh_var "a0" xs zs ~wrt:(Set.union us xs) in let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in @@ -467,23 +470,23 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l in let min = Sh.and_ - (Exp.eq - (Exp.memory ~siz:o ~arr:a) - (Exp.concat - [|Exp.memory ~siz:ln_k ~arr:a1; Exp.memory ~siz:ko_ln ~arr:a2|])) + (Term.eq + (Term.memory ~siz:o ~arr:a) + (Term.concat + [|Term.memory ~siz:ln_k ~arr:a1; Term.memory ~siz:ko_ln ~arr:a2|])) (Sh.star (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2}) (Sh.rem_seg msg min)) in let sub = - Sh.and_ (Exp.eq b b') - (Sh.and_ (Exp.eq m m') + Sh.and_ (Term.eq b b') + (Sh.and_ (Term.eq m m') (Sh.and_ - (Exp.eq - (Exp.concat - [| Exp.memory ~siz:k_l ~arr:a0' - ; Exp.memory ~siz:ln_k ~arr:a1 |]) - (Exp.memory ~siz:n ~arr:a')) + (Term.eq + (Term.concat + [| Term.memory ~siz:k_l ~arr:a0' + ; Term.memory ~siz:ln_k ~arr:a1 |]) + (Term.memory ~siz:n ~arr:a')) (Sh.star (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'}) (Sh.rem_seg ssg sub)))) @@ -504,13 +507,14 @@ let excise_seg ({sub} as goal) msg ssg = || not (Equality.entails_eq sub.cong m m') then Some - {goal with sub= Sh.and_ (Exp.eq b b') (Sh.and_ (Exp.eq m m') goal.sub)} + { goal with + sub= Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') goal.sub) } else match[@warning "-p"] Z.sign k_l with (* k-l < 0 so k < l *) | -1 -> ( - let ko = Exp.add Typ.ptr k o in - let ln = Exp.add Typ.ptr l n in + let ko = Term.add Typ.ptr k o in + let ln = Term.add Typ.ptr l n in Equality.difference sub.cong ko ln >>= fun ko_ln -> match[@warning "-p"] Z.sign ko_ln with @@ -535,7 +539,7 @@ let excise_seg ({sub} as goal) msg ssg = (* k-l = 0 so k = l *) | 0 -> ( match Equality.difference sub.cong o n with - | None -> Some {goal with sub= Sh.and_ (Exp.eq o n) goal.sub} + | None -> Some {goal with sub= Sh.and_ (Term.eq o n) goal.sub} | Some o_n -> ( match[@warning "-p"] Z.sign o_n with (* o-n < 0 [k; o) @@ -549,8 +553,8 @@ let excise_seg ({sub} as goal) msg ssg = | 1 -> Some (excise_seg_sub_prefix goal msg ssg o_n) ) ) (* k-l > 0 so k > l *) | 1 -> ( - let ko = Exp.add Typ.ptr k o in - let ln = Exp.add Typ.ptr l n in + let ko = Term.add Typ.ptr k o in + let ln = Term.add Typ.ptr l n in Equality.difference sub.cong ko ln >>= fun ko_ln -> match[@warning "-p"] Z.sign ko_ln with diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index e68c71260..ce488ceef 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -22,10 +22,10 @@ let%test_module _ = Solver.infer_frame p (Var.Set.of_list xs) q |> fun r -> assert (Option.is_some r) - let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz - let ( + ) = Exp.add Typ.ptr - let ( - ) = Exp.sub Typ.siz - let ( * ) = Exp.mul Typ.siz + let ( ! ) i = Term.integer (Z.of_int i) Typ.siz + let ( + ) = Term.add Typ.ptr + let ( - ) = Term.sub Typ.siz + let ( * ) = Term.mul Typ.siz let wrt = Var.Set.empty let a_, wrt = Var.fresh "a" ~wrt let a2_, wrt = Var.fresh "a" ~wrt @@ -36,15 +36,15 @@ let%test_module _ = let l2_, wrt = Var.fresh "l" ~wrt let m_, wrt = Var.fresh "m" ~wrt let n_, _ = Var.fresh "n" ~wrt - let a = Exp.var a_ - let a2 = Exp.var a2_ - let a3 = Exp.var a3_ - let b = Exp.var b_ - let k = Exp.var k_ - let l = Exp.var l_ - let l2 = Exp.var l2_ - let m = Exp.var m_ - let n = Exp.var n_ + let a = Term.var a_ + let a2 = Term.var a2_ + let a3 = Term.var a3_ + let b = Term.var b_ + let k = Term.var k_ + let l = Term.var l_ + let l2 = Term.var l2_ + let m = Term.var m_ + let n = Term.var n_ let%expect_test _ = check_frame Sh.emp [] Sh.emp ; @@ -61,7 +61,7 @@ let%test_module _ = ) infer_frame: false |}] let%expect_test _ = - check_frame Sh.emp [n_; m_] (Sh.and_ (Exp.eq m n) Sh.emp) ; + check_frame Sh.emp [n_; m_] (Sh.and_ (Term.eq m n) Sh.emp) ; [%expect {| ( infer_frame: emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp @@ -93,7 +93,7 @@ let%test_module _ = let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in let minued = Sh.star common seg1 in let subtrahend = - Sh.and_ (Exp.eq m n) + Sh.and_ (Term.eq m n) (Sh.exists (Var.Set.of_list [m_]) (Sh.extend_us (Var.Set.of_list [m_]) common)) @@ -235,7 +235,7 @@ let%test_module _ = let%expect_test _ = check_frame (Sh.and_ - Exp.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) + Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) seg_split_symbolically) [m_; a_] (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; @@ -272,7 +272,7 @@ let%test_module _ = (* Incompleteness: equivalent to above but using ≤ instead of ∨ *) let%expect_test _ = infer_frame - (Sh.and_ (Exp.le n !2) seg_split_symbolically) + (Sh.and_ (Term.le n !2) seg_split_symbolically) [m_; a_] (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ; [%expect diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml new file mode 100644 index 000000000..9a699550e --- /dev/null +++ b/sledge/src/symbheap/term.ml @@ -0,0 +1,1465 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Terms *) + +(** Z wrapped to treat bounded and unsigned operations *) +module Z = struct + include Z + + (** Interpret as a bounded integer with specified signedness and width. *) + let clamp ~signed bits z = + if signed then Z.signed_extract z 0 bits else Z.extract z 0 bits + + let clamp_cmp ~signed bits op x y = + op (clamp ~signed bits x) (clamp ~signed bits y) + + let clamp_bop ~signed bits op x y = + clamp ~signed bits (op (clamp ~signed bits x) (clamp ~signed bits y)) + + let beq ~bits x y = clamp_cmp ~signed:true bits Z.equal x y + let bleq ~bits x y = clamp_cmp ~signed:true bits Z.leq x y + let bgeq ~bits x y = clamp_cmp ~signed:true bits Z.geq x y + let blt ~bits x y = clamp_cmp ~signed:true bits Z.lt x y + let bgt ~bits x y = clamp_cmp ~signed:true bits Z.gt x y + let buleq ~bits x y = clamp_cmp ~signed:false bits Z.leq x y + let bugeq ~bits x y = clamp_cmp ~signed:false bits Z.geq x y + let bult ~bits x y = clamp_cmp ~signed:false bits Z.lt x y + let bugt ~bits x y = clamp_cmp ~signed:false bits Z.gt x y + let bsub ~bits x y = clamp_bop ~signed:true bits Z.sub x y + let bmul ~bits x y = clamp_bop ~signed:true bits Z.mul x y + let bdiv ~bits x y = clamp_bop ~signed:true bits Z.div x y + let brem ~bits x y = clamp_bop ~signed:true bits Z.rem x y + let budiv ~bits x y = clamp_bop ~signed:false bits Z.div x y + let burem ~bits x y = clamp_bop ~signed:false bits Z.rem x y + let blogand ~bits x y = clamp_bop ~signed:true bits Z.logand x y + let blogor ~bits x y = clamp_bop ~signed:true bits Z.logor x y + let blogxor ~bits x y = clamp_bop ~signed:true bits Z.logxor x y + let bshift_left ~bits z i = Z.shift_left (clamp bits ~signed:true z) i + let bshift_right ~bits z i = Z.shift_right (clamp bits ~signed:true z) i + + let bshift_right_trunc ~bits z i = + Z.shift_right_trunc (clamp bits ~signed:true z) i +end + +module rec T : sig + type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] + + type t = + (* nary: arithmetic, numeric and pointer *) + | Add of {args: qset; typ: Typ.t} + | Mul of {args: qset; typ: Typ.t} + (* pointer and memory constants and operations *) + | Splat of {byt: t; siz: t} + | Memory of {siz: t; arr: t} + | Concat of {args: t vector} + (* nullary *) + | Var of {id: int; name: string} + | Nondet of {msg: string} + | Label of {parent: string; name: string} + (* curried application *) + | App of {op: t; arg: t} + (* binary: comparison *) + | Eq + | Dq + | Gt + | Ge + | Lt + | Le + | Ugt + | Uge + | Ult + | Ule + | Ord + | Uno + (* binary: arithmetic, numeric and pointer *) + | Div + | Udiv + | Rem + | Urem + (* binary: boolean / bitwise *) + | And + | Or + | Xor + | Shl + | Lshr + | Ashr + (* ternary: conditional *) + | Conditional + (* array/struct constants and operations *) + | Record + | Select + | Update + | Struct_rec of {elts: t vector} (** NOTE: may be cyclic *) + (* unary: conversion *) + | Convert of {signed: bool; dst: Typ.t; src: Typ.t} + (* numeric constants *) + | Integer of {data: Z.t; typ: Typ.t} + | Float of {data: string} + [@@deriving compare, equal, hash, sexp] + + (* Note: solve (and invariant) requires Qset.min_elt to return a + non-coefficient, so Integer terms must compare higher than any valid + monomial *) + + type comparator_witness + + val comparator : (t, comparator_witness) Comparator.t +end = struct + include T0 include Comparator.Make (T0) +end + +(* auxiliary definition for safe recursive module initialization *) +and T0 : sig + type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] + + type t = + | Add of {args: qset; typ: Typ.t} + | Mul of {args: qset; typ: Typ.t} + | Splat of {byt: t; siz: t} + | Memory of {siz: t; arr: t} + | Concat of {args: t vector} + | Var of {id: int; name: string} + | Nondet of {msg: string} + | Label of {parent: string; name: string} + | App of {op: t; arg: t} + | Eq + | Dq + | Gt + | Ge + | Lt + | Le + | Ugt + | Uge + | Ult + | Ule + | Ord + | Uno + | Div + | Udiv + | Rem + | Urem + | And + | Or + | Xor + | Shl + | Lshr + | Ashr + | Conditional + | Record + | Select + | Update + | Struct_rec of {elts: t vector} + | Convert of {signed: bool; dst: Typ.t; src: Typ.t} + | Integer of {data: Z.t; typ: Typ.t} + | Float of {data: string} + [@@deriving compare, equal, hash, sexp] +end = struct + type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp] + + type t = + | Add of {args: qset; typ: Typ.t} + | Mul of {args: qset; typ: Typ.t} + | Splat of {byt: t; siz: t} + | Memory of {siz: t; arr: t} + | Concat of {args: t vector} + | Var of {id: int; name: string} + | Nondet of {msg: string} + | Label of {parent: string; name: string} + | App of {op: t; arg: t} + | Eq + | Dq + | Gt + | Ge + | Lt + | Le + | Ugt + | Uge + | Ult + | Ule + | Ord + | Uno + | Div + | Udiv + | Rem + | Urem + | And + | Or + | Xor + | Shl + | Lshr + | Ashr + | Conditional + | Record + | Select + | Update + | Struct_rec of {elts: t vector} + | Convert of {signed: bool; dst: Typ.t; src: Typ.t} + | Integer of {data: Z.t; typ: Typ.t} + | Float of {data: string} + [@@deriving compare, equal, hash, sexp] +end + +(* suppress spurious "Warning 60: unused module T0." *) +type _t = T0.t + +include T + +let empty_map = Map.empty (module T) +let empty_qset = Qset.empty (module T) + +let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a = + let rec fix_f seen e = + match e with + | Struct_rec _ -> + if List.mem ~equal:( == ) seen e then f bot e + else f (fix_f (e :: seen)) e + | _ -> f (fix_f seen) e + in + let rec fix_f_seen_nil e = + match e with Struct_rec _ -> f (fix_f [e]) e | _ -> f fix_f_seen_nil e + in + fix_f_seen_nil e + +let fix_flip (f : ('z -> t -> 'a as 'f) -> 'f) (bot : 'f) (z : 'z) (e : t) = + fix (fun f' e z -> f (fun z e -> f' e z) z e) (fun e z -> bot z e) e z + +let uncurry = + let rec uncurry_ acc_args = function + | App {op; arg} -> uncurry_ (arg :: acc_args) op + | op -> (op, acc_args) + in + uncurry_ [] + +let rec pp ?is_x fs term = + let get_var_style var = + match is_x with + | None -> `None + | Some is_x -> if not (is_x var) then `Bold else `Cyan + in + let pp_ pp fs term = + let pf fmt = + Format.pp_open_box fs 2 ; + Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt + in + match term with + | Var {name; id= 0} as var -> + Trace.pp_styled (get_var_style var) "%%%s" fs name + | Var {name; id} as var -> + Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id + | Nondet {msg} -> pf "nondet \"%s\"" msg + | Label {name} -> pf "%s" name + | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null" + | Splat {byt; siz} -> pf "%a^%a" pp byt pp siz + | Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr + | Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args + | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data + | Float {data} -> pf "%s" data + | Eq -> pf "=" + | Dq -> pf "@<1>≠" + | Gt -> pf ">" + | Ge -> pf "@<1>≥" + | Lt -> pf "<" + | Le -> pf "@<1>≤" + | Ugt -> pf "u>" + | Uge -> pf "@<2>u≥" + | Ult -> pf "u<" + | Ule -> pf "@<2>u≤" + | Ord -> pf "ord" + | Uno -> pf "uno" + | Add {args} -> + let pp_poly_term fs (monomial, coefficient) = + match monomial with + | Integer {data} when Z.equal Z.one data -> Q.pp fs coefficient + | _ when Q.equal Q.one coefficient -> pp fs monomial + | _ -> + Format.fprintf fs "%a @<1>× %a" Q.pp coefficient pp monomial + in + pf "(%a)" (Qset.pp "@ + " pp_poly_term) args + | Mul {args} -> + let pp_mono_term fs (factor, exponent) = + if Q.equal Q.one exponent then pp fs factor + else Format.fprintf fs "%a^%a" pp factor Q.pp exponent + in + pf "(%a)" (Qset.pp "@ @<2>× " pp_mono_term) args + | Div -> pf "/" + | Udiv -> pf "udiv" + | Rem -> pf "rem" + | Urem -> pf "urem" + | And -> pf "&&" + | Or -> pf "||" + | Xor -> pf "xor" + | App + {op= App {op= Xor; arg}; arg= Integer {data; typ= Integer {bits= 1}}} + when Z.is_true data -> + pf "¬%a" pp arg + | App + {op= App {op= Xor; arg= Integer {data; typ= Integer {bits= 1}}}; arg} + when Z.is_true data -> + pf "¬%a" pp arg + | Shl -> pf "shl" + | Lshr -> pf "lshr" + | Ashr -> pf "ashr" + | Conditional -> pf "(_?_:_)" + | App {op= Conditional; arg= cnd} -> pf "(%a@ ? _:_)" pp cnd + | App {op= App {op= Conditional; arg= cnd}; arg= thn} -> + pf "(%a@ ? %a@ : _)" pp cnd pp thn + | App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els} + -> + pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els + | Select -> pf "_[_]" + | App {op= Select; arg= rcd} -> pf "%a[_]" pp rcd + | App {op= App {op= Select; arg= rcd}; arg= idx} -> + pf "%a[%a]" pp rcd pp idx + | Update -> pf "[_|_→_]" + | App {op= Update; arg= rcd} -> pf "[%a@ @[| _→_@]]" pp rcd + | App {op= App {op= Update; arg= rcd}; arg= elt} -> + pf "[%a@ @[| _→ %a@]]" pp rcd pp elt + | App {op= App {op= App {op= Update; arg= rcd}; arg= elt}; arg= idx} -> + pf "[%a@ @[| %a → %a@]]" pp rcd pp idx pp elt + | Record -> pf "{_}" + | App {op; arg} -> ( + match uncurry term with + | Record, elts -> pf "{%a}" pp_record elts + | op, [x; y] -> pf "(%a@ %a %a)" pp x pp op pp y + | _ -> pf "(%a@ %a)" pp op pp arg ) + | Struct_rec {elts} -> pf "{|%a|}" (Vector.pp ",@ " pp) elts + | Convert {dst; src} -> pf "(%a)(%a)" Typ.pp dst Typ.pp src + in + fix_flip pp_ (fun _ _ -> ()) fs term + +and pp_record fs elts = + [%Trace.fprintf + fs "%a" + (fun fs elts -> + let elta = Array.of_list elts in + match + String.init (Array.length elta) ~f:(fun i -> + match elta.(i) with + | Integer {data} -> Char.of_int_exn (Z.to_int data) + | _ -> raise (Invalid_argument "not a string") ) + with + | s -> Format.fprintf fs "@[%s@]" (String.escaped s) + | exception _ -> + Format.fprintf fs "@[%a@]" (List.pp ",@ " pp) elts ) + elts] + +type term = t + +let pp_t = pp ?is_x:None +let pp_full = pp +let pp = pp_t + +(** Invariant *) + +let rec typ_of = function + | Add {typ} | Mul {typ} | Integer {typ} | App {op= Convert {dst= typ}} -> + Some typ + | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule}} + -> + Some Typ.bool + | App + { op= + App + { op= + Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr + ; arg= x } + ; arg= y } -> ( + match typ_of x with Some _ as t -> t | None -> typ_of y ) + | App {op= App {op= App {op= Conditional}; arg= thn}; arg= els} -> ( + match typ_of thn with Some _ as t -> t | None -> typ_of els ) + | _ -> None + +let typ = typ_of + +let type_check e typ = + assert ( + Option.for_all ~f:(Typ.castable typ) (typ_of e) + || fail "%a@ : %a not <:@ %a" pp e Typ.pp + (Option.value_exn (typ_of e)) + Typ.pp typ ) + +let type_check2 e f typ = type_check e typ ; type_check f typ + +(* an indeterminate (factor of a monomial) is any non-Add/Mul/Integer term *) +let rec assert_indeterminate = function + | App {op} -> assert_indeterminate op + | Integer _ | Add _ | Mul _ -> assert false + | _ -> assert true + +(* a monomial is a power product of factors, e.g. + * ∏ᵢ xᵢ^nᵢ + * for (non-constant) indeterminants xᵢ and positive integer exponents nᵢ + *) +let assert_monomial add_typ mono = + match mono with + | Mul {typ; args} -> + assert (Typ.castable add_typ typ) ; + assert (Option.is_some (Typ.prim_bit_size_of typ)) ; + Qset.iter args ~f:(fun factor exponent -> + assert (Q.sign exponent > 0) ; + assert_indeterminate factor |> Fn.id ) + | _ -> assert_indeterminate mono |> Fn.id + +(* a polynomial term is a monomial multiplied by a non-zero coefficient + * c × ∏ᵢ xᵢ + *) +let assert_poly_term add_typ mono coeff = + assert (not (Q.equal Q.zero coeff)) ; + match mono with + | Integer {data} -> assert (Z.equal Z.one data) + | Mul {args} -> + ( match Qset.min_elt args with + | None | Some (Integer _, _) -> assert false + | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n)) + ) ; + assert_monomial add_typ mono |> Fn.id + | _ -> assert_monomial add_typ mono |> Fn.id + +(* a polynomial is a linear combination of monomials, e.g. + * ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ + * for non-zero constant coefficients cᵢ + * and monomials ∏ⱼ xᵢⱼ, one of which may be the empty product 1 + *) +let assert_polynomial poly = + match poly with + | Add {typ; args} -> + ( match Qset.min_elt args with + | None -> assert false + | Some (Integer _, _) -> assert false + | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k)) + ) ; + Qset.iter args ~f:(fun m c -> assert_poly_term typ m c |> Fn.id) + | _ -> assert false + +let invariant ?(partial = false) e = + Invariant.invariant [%here] e [%sexp_of: t] + @@ fun () -> + let op, args = uncurry e in + let assert_arity arity = + let nargs = List.length args in + assert (nargs = arity || (partial && nargs < arity)) + in + match op with + | App _ -> fail "uncurry cannot return App" () + | Integer {data; typ= (Integer _ | Pointer _) as typ} -> ( + match Typ.prim_bit_size_of typ with + | None -> assert false + | Some bits -> + assert_arity 0 ; + assert (Z.numbits data <= bits) ) + | Integer _ -> assert false + | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0 + | Convert {dst; src} -> + ( match args with + | [Integer {typ= Integer _ as typ}] -> assert (Typ.equal src typ) + | [arg] -> + assert (Option.for_all ~f:(Typ.convertible src) (typ_of arg)) + | _ -> assert_arity 1 ) ; + assert (Typ.convertible src dst) + | Add _ -> assert_polynomial e |> Fn.id + | Mul {typ} -> assert_monomial typ e |> Fn.id + | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Div | Udiv | Rem + |Urem | And | Or | Xor | Shl | Lshr | Ashr -> ( + match args with + | [x; y] -> ( + match (typ_of x, typ_of y) with + | Some typ, Some typ' -> assert (Typ.castable typ typ') + | _ -> assert true ) + | _ -> assert_arity 2 ) + | Concat {args} -> assert (Vector.length args <> 1) + | Splat {byt; siz} -> ( + assert (Option.exists ~f:(Typ.convertible Typ.byt) (typ_of byt)) ; + assert (Option.exists ~f:(Typ.convertible Typ.siz) (typ_of siz)) ; + match siz with + | Integer {data} -> assert (not (Z.equal Z.zero data)) + | _ -> () ) + | Memory {siz} -> + assert (Option.for_all ~f:(Typ.convertible Typ.siz) (typ_of siz)) + | Ord | Uno | Select -> assert_arity 2 + | Conditional | Update -> assert_arity 3 + | Record -> assert (partial || not (List.is_empty args)) + | Struct_rec {elts} -> + assert (not (Vector.is_empty elts)) ; + assert_arity 0 + +let bits_of_int term = + match term with + | Integer {typ} -> ( + match Typ.prim_bit_size_of typ with + | Some bits -> bits + | None -> violates invariant term ) + | _ -> fail "bits_of_int" () + +(** Variables are the terms constructed by [Var] *) +module Var = struct + include T + + let pp = pp + + type var = t + + let of_reg (r : Reg.t) = + match (r :> Exp.t) with + | Reg {id; name} -> Var {id; name} + | _ -> violates Reg.invariant r + + module Set = struct + include ( + Set : + module type of Set with type ('elt, 'cmp) t := ('elt, 'cmp) Set.t ) + + type t = Set.M(T).t [@@deriving compare, equal, sexp] + + let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs + let pp = pp_full ?is_x:None + let empty = Set.empty (module T) + let of_option = Option.fold ~f:Set.add ~init:empty + let of_list = Set.of_list (module T) + let of_vector = Set.of_vector (module T) + let of_regs = Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) + end + + module Map = struct + include ( + Map : + module type of Map + with type ('key, 'value, 'cmp) t := ('key, 'value, 'cmp) Map.t ) + + type 'v t = 'v Map.M(T).t [@@deriving compare, equal, sexp] + + let empty = Map.empty (module T) + end + + let demangle = + let open Ctypes in + let cxa_demangle = + (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *) + Foreign.foreign "__cxa_demangle" + ( string @-> ptr char @-> ptr size_t @-> ptr int + @-> returning string_opt ) + in + let null_ptr_char = from_voidp char null in + let null_ptr_size_t = from_voidp size_t null in + let status = allocate int 0 in + fun mangled -> + let demangled = + cxa_demangle mangled null_ptr_char null_ptr_size_t status + in + if !@status = 0 then demangled else None + + let pp_demangled fs = function + | Var {name} -> ( + match demangle name with + | Some demangled when not (String.equal name demangled) -> + Format.fprintf fs "“%s”" demangled + | _ -> () ) + | _ -> () + + let invariant x = + Invariant.invariant [%here] x [%sexp_of: t] + @@ fun () -> match x with Var _ -> invariant x | _ -> assert false + + let id = function Var {id} -> id | x -> violates invariant x + let name = function Var {name} -> name | x -> violates invariant x + + let of_term = function + | Var _ as v -> Some (v |> check invariant) + | _ -> None + + let program name = Var {id= 0; name} |> check invariant + + let fresh name ~(wrt : Set.t) = + let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in + let x' = Var {name; id= max + 1} in + (x', Set.add wrt x') + + (** Variable renaming substitutions *) + module Subst = struct + type t = T.t Map.M(T).t [@@deriving compare, equal, sexp] + + let invariant s = + Invariant.invariant [%here] s [%sexp_of: t] + @@ fun () -> + let domain, range = + Map.fold s ~init:(Set.empty, Set.empty) + ~f:(fun ~key ~data (domain, range) -> + assert (not (Set.mem range data)) ; + (Set.add domain key, Set.add range data) ) + in + assert (Set.disjoint domain range) + + let pp fs s = + Format.fprintf fs "@[<1>[%a]@]" + (List.pp ",@ " (fun fs (k, v) -> + Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v )) + (Map.to_alist s) + + let empty = empty_map + let is_empty = Map.is_empty + + let freshen vs ~wrt = + let xs = Set.inter wrt vs in + let wrt = Set.union wrt vs in + Set.fold xs ~init:(empty, wrt) ~f:(fun (sub, wrt) x -> + let x', wrt = fresh (name x) ~wrt in + let sub = Map.add_exn sub ~key:x ~data:x' in + (sub, wrt) ) + |> fst |> check invariant + + let extend sub ~replace ~with_ = + ( match Map.add sub ~key:replace ~data:with_ with + | `Duplicate -> sub + | `Ok sub -> + Map.map_preserving_phys_equal sub ~f:(fun v -> + if T.equal v replace then with_ else v ) ) + |> check invariant + + let invert sub = + Map.fold sub ~init:empty ~f:(fun ~key ~data sub' -> + Map.add_exn sub' ~key:data ~data:key ) + |> check invariant + + let exclude sub vs = + Set.fold vs ~init:sub ~f:Map.remove |> check invariant + + let restrict sub vs = + Map.filter_keys ~f:(Set.mem vs) sub |> check invariant + + let domain sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain -> + Set.add domain key ) + + let range sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> + Set.add range data ) + + let apply sub v = try Map.find_exn sub v with Caml.Not_found -> v + + let apply_set sub vs = + Map.fold sub ~init:vs ~f:(fun ~key ~data vs -> + let vs' = Set.remove vs key in + if Set.to_tree vs' == Set.to_tree vs then vs + else ( + assert (not (Set.equal vs' vs)) ; + Set.add vs' data ) ) + + let close_set sub vs = + Map.fold sub ~init:vs ~f:(fun ~key:_ ~data vs -> Set.add vs data) + end +end + +let fold_terms e ~init ~f = + let fold_terms_ fold_terms_ e z = + let z = + match e with + | App {op= x; arg= y} + |Splat {byt= x; siz= y} + |Memory {siz= x; arr= y} -> + fold_terms_ y (fold_terms_ x z) + | Add {args} | Mul {args} -> + Qset.fold args ~init:z ~f:(fun arg _ z -> fold_terms_ arg z) + | Concat {args} | Struct_rec {elts= args} -> + Vector.fold args ~init:z ~f:(fun z elt -> fold_terms_ elt z) + | _ -> z + in + f z e + in + fix fold_terms_ (fun _ z -> z) e init + +let iter_terms e ~f = fold_terms e ~init:() ~f:(fun () e -> f e) + +let fold_vars e ~init ~f = + fold_terms e ~init ~f:(fun z -> function + | Var _ as v -> f z (v :> Var.t) | _ -> z ) + +let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty + +(** Construct *) + +let var x = x +let nondet msg = Nondet {msg} |> check invariant +let label ~parent ~name = Label {parent; name} |> check invariant +let integer data typ = Integer {data; typ} |> check invariant +let null = integer Z.zero Typ.ptr +let bool b = integer (Z.of_bool b) Typ.bool +let float data = Float {data} |> check invariant + +let zero (typ : Typ.t) = + match typ with Float _ -> float "0" | _ -> integer Z.zero typ + +let one (typ : Typ.t) = + match typ with Float _ -> float "1" | _ -> integer Z.one typ + +let minus_one (typ : Typ.t) = + match typ with Float _ -> float "-1" | _ -> integer Z.minus_one typ + +let simp_convert signed (dst : Typ.t) src arg = + match (dst, arg) with + | _ when Typ.castable dst src -> arg + | Integer {bits= m}, Integer {data; typ= Integer {bits= n}} -> + integer (Z.clamp ~signed (min m n) data) dst + | _ -> App {op= Convert {signed; dst; src}; arg} + +let simp_gt x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bgt ~bits i j) + | _ -> App {op= App {op= Gt; arg= x}; arg= y} + +let simp_ugt x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bugt ~bits i j) + | _ -> App {op= App {op= Ugt; arg= x}; arg= y} + +let simp_ge x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bgeq ~bits i j) + | _ -> App {op= App {op= Ge; arg= x}; arg= y} + +let simp_uge x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bugeq ~bits i j) + | _ -> App {op= App {op= Uge; arg= x}; arg= y} + +let simp_lt x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.blt ~bits i j) + | _ -> App {op= App {op= Lt; arg= x}; arg= y} + +let simp_ult x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bult ~bits i j) + | _ -> App {op= App {op= Ult; arg= x}; arg= y} + +let simp_le x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.bleq ~bits i j) + | _ -> App {op= App {op= Le; arg= x}; arg= y} + +let simp_ule x y = + match (x, y) with + | Integer {data= i}, Integer {data= j; typ= Integer {bits}} -> + bool (Z.buleq ~bits i j) + | _ -> App {op= App {op= Ule; arg= x}; arg= y} + +let simp_ord x y = App {op= App {op= Ord; arg= x}; arg= y} +let simp_uno x y = App {op= App {op= Uno; arg= x}; arg= y} + +let sum_mul_const const sum = + assert (not (Q.equal Q.zero const)) ; + if Q.equal Q.one const then sum + else Qset.map_counts ~f:(fun _ -> Q.mul const) sum + +let rec sum_to_term typ sum = + match Qset.length sum with + | 0 -> zero typ + | 1 -> ( + match Qset.min_elt sum with + | Some (Integer _, q) -> rational q typ + | Some (arg, q) when Q.equal Q.one q -> arg + | _ -> Add {typ; args= sum} ) + | _ -> Add {typ; args= sum} + +and rational Q.{num; den} typ = + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + simp_div + (integer (Z.clamp ~signed:true bits num) typ) + (integer (Z.clamp ~signed:true bits den) typ) + +and simp_div x y = + match (x, y) with + (* i / j *) + | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.bdiv ~bits i j) typ + (* e / 1 ==> e *) + | e, Integer {data} when Z.equal Z.one data -> e + (* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *) + | Add {typ; args}, Integer {data} -> + sum_to_term typ (sum_mul_const Q.(inv (of_z data)) args) + | _ -> App {op= App {op= Div; arg= x}; arg= y} + +let simp_udiv x y = + match (x, y) with + (* i u/ j *) + | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.budiv ~bits i j) typ + (* e u/ 1 ==> e *) + | e, Integer {data} when Z.equal Z.one data -> e + | _ -> App {op= App {op= Udiv; arg= x}; arg= y} + +let simp_rem x y = + match (x, y) with + (* i % j *) + | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.brem ~bits i j) typ + (* e % 1 ==> 0 *) + | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ + | _ -> App {op= App {op= Rem; arg= x}; arg= y} + +let simp_urem x y = + match (x, y) with + (* i u% j *) + | Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.burem ~bits i j) typ + (* e u% 1 ==> 0 *) + | _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ + | _ -> App {op= App {op= Urem; arg= x}; arg= y} + +(* Sums of polynomial terms represented by multisets. A sum ∑ᵢ cᵢ × Xᵢ of + monomials Xᵢ with coefficients cᵢ is represented by a multiset where the + elements are Xᵢ with multiplicities cᵢ. A constant is treated as the + coefficient of the empty monomial, which is the unit of multiplication 1. *) +module Sum = struct + let empty = empty_qset + + let add coeff term sum = + assert (not (Q.equal Q.zero coeff)) ; + match term with + | Integer {data} when Z.equal Z.zero data -> sum + | Integer {data; typ} -> + Qset.add sum (integer Z.one typ) Q.(coeff * of_z data) + | _ -> Qset.add sum term coeff + + let singleton ?(coeff = Q.one) term = add coeff term empty + + let map sum ~f = + Qset.fold sum ~init:empty ~f:(fun e c sum -> add c (f e) sum) + + let mul_const = sum_mul_const + let to_term = sum_to_term +end + +let rec simp_add_ typ es poly = + (* (coeff × term) + poly *) + let f term coeff poly = + match (term, poly) with + (* (0 × e) + s ==> 0 (optim) *) + | _ when Q.equal Q.zero coeff -> poly + (* (c × 0) + s ==> s (optim) *) + | Integer {data}, _ when Z.equal Z.zero data -> poly + (* (c × cᵢ) + cⱼ ==> c×cᵢ+cⱼ *) + | Integer {data= i}, Integer {data= j} -> + rational Q.((coeff * of_z i) + of_z j) typ + (* (c × ∑ᵢ cᵢ × Xᵢ) + s ==> (∑ᵢ (c × cᵢ) × Xᵢ) + s *) + | Add {args}, _ -> simp_add_ typ (Sum.mul_const coeff args) poly + (* (c₀ × X₀) + (∑ᵢ₌₁ⁿ cᵢ × Xᵢ) ==> ∑ᵢ₌₀ⁿ cᵢ × Xᵢ *) + | _, Add {args} -> Sum.to_term typ (Sum.add coeff term args) + (* (c₁ × X₁) + X₂ ==> ∑ᵢ₌₁² cᵢ × Xᵢ for c₂ = 1 *) + | _ -> Sum.to_term typ (Sum.add coeff term (Sum.singleton poly)) + in + Qset.fold ~f es ~init:poly + +let simp_add typ es = simp_add_ typ es (zero typ) +let simp_add2 typ e f = simp_add_ typ (Sum.singleton e) f + +(* Products of indeterminants represented by multisets. A product ∏ᵢ xᵢ^nᵢ + of indeterminates xᵢ is represented by a multiset where the elements are + xᵢ and the multiplicities are the exponents nᵢ. *) +module Prod = struct + let empty = empty_qset + + let add term prod = + assert (match term with Integer _ -> false | _ -> true) ; + Qset.add prod term Q.one + + let singleton term = add term empty + let union = Qset.union +end + +let rec simp_mul2 typ e f = + match (e, f) with + (* c₁ × c₂ ==> c₁×c₂ *) + | Integer {data= i}, Integer {data= j} -> + integer (Z.bmul ~bits:(bits_of_int e) i j) typ + (* 0 × f ==> 0 *) + | Integer {data}, _ when Z.equal Z.zero data -> e + (* e × 0 ==> 0 *) + | _, Integer {data} when Z.equal Z.zero data -> f + (* c × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ c × cᵤ × ∏ⱼ yᵤⱼ *) + | Integer {data}, Add {args} | Add {args}, Integer {data} -> + Sum.to_term typ (Sum.mul_const (Q.of_z data) args) + (* c₁ × x₁ ==> ∑ᵢ₌₁ cᵢ × xᵢ *) + | Integer {data= c}, x | x, Integer {data= c} -> + Sum.to_term typ (Sum.singleton ~coeff:(Q.of_z c) x) + (* (∏ᵤ₌₀ⁱ xᵤ) × (∏ᵥ₌ᵢ₊₁ⁿ xᵥ) ==> ∏ⱼ₌₀ⁿ xⱼ *) + | Mul {args= xs1}, Mul {args= xs2} -> Mul {typ; args= Prod.union xs1 xs2} + (* (∏ᵢ xᵢ) × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ cᵤ × ∏ᵢ xᵢ × ∏ⱼ yᵤⱼ *) + | (Mul {args= prod} as m), Add {args= sum} + |Add {args= sum}, (Mul {args= prod} as m) -> + Sum.to_term typ + (Sum.map sum ~f:(function + | Mul {args} -> Mul {typ; args= Prod.union prod args} + | Integer _ as c -> simp_mul2 typ c m + | mono -> Mul {typ; args= Prod.add mono prod} )) + (* x₀ × (∏ᵢ₌₁ⁿ xᵢ) ==> ∏ᵢ₌₀ⁿ xᵢ *) + | Mul {args= xs1}, x | x, Mul {args= xs1} -> + Mul {typ; args= Prod.add x xs1} + (* e × (∑ᵤ cᵤ × ∏ⱼ yᵤⱼ) ==> ∑ᵤ e × cᵤ × ∏ⱼ yᵤⱼ *) + | Add {args}, e | e, Add {args} -> + simp_add typ (Sum.map ~f:(fun m -> simp_mul2 typ e m) args) + (* x₁ × x₂ ==> ∏ᵢ₌₁² xᵢ *) + | _ -> Mul {args= Prod.add e (Prod.singleton f); typ} + +let simp_mul typ es = + (* (bas ^ pwr) × term *) + let rec mul_pwr bas pwr term = + if Q.equal Q.zero pwr then term + else mul_pwr bas Q.(pwr - one) (simp_mul2 typ bas term) + in + let one = one typ in + Qset.fold es ~init:one ~f:(fun bas pwr term -> + if Q.sign pwr >= 0 then mul_pwr bas pwr term + else simp_div term (mul_pwr bas (Q.neg pwr) one) ) + +let simp_negate typ x = simp_mul2 typ (minus_one typ) x + +let simp_sub typ x y = + match (x, y) with + (* i - j *) + | Integer {data= i}, Integer {data= j} -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.bsub ~bits i j) typ + (* x - y ==> x + (-1 * y) *) + | _ -> simp_add2 typ x (simp_negate typ y) + +let simp_cond cnd thn els = + match cnd with + (* ¬(true ? t : e) ==> t *) + | Integer {data; typ= Integer {bits= 1}} when Z.is_true data -> thn + (* ¬(false ? t : e) ==> e *) + | Integer {data; typ= Integer {bits= 1}} when Z.is_false data -> els + | _ -> + App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els} + +let rec simp_and x y = + match (x, y) with + (* i && j *) + | Integer {data= i; typ}, Integer {data= j} -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.blogand ~bits i j) typ + (* e && true ==> e *) + | Integer {data; typ= Integer {bits= 1}}, e + |e, Integer {data; typ= Integer {bits= 1}} + when Z.is_true data -> + e + (* e && false ==> 0 *) + | (Integer {data; typ= Integer {bits= 1}} as f), _ + |_, (Integer {data; typ= Integer {bits= 1}} as f) + when Z.is_false data -> + f + (* e && (c ? t : f) ==> (c ? e && t : e && f) *) + | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f} + |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e -> + simp_cond c (simp_and e t) (simp_and e f) + (* e && e ==> e *) + | _ when equal x y -> x + | _ -> App {op= App {op= And; arg= x}; arg= y} + +let rec simp_or x y = + match (x, y) with + (* i || j *) + | Integer {data= i; typ}, Integer {data= j} -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.blogor ~bits i j) typ + (* e || true ==> true *) + | (Integer {data; typ= Integer {bits= 1}} as t), _ + |_, (Integer {data; typ= Integer {bits= 1}} as t) + when Z.is_true data -> + t + (* e || false ==> e *) + | Integer {data; typ= Integer {bits= 1}}, e + |e, Integer {data; typ= Integer {bits= 1}} + when Z.is_false data -> + e + (* e || (c ? t : f) ==> (c ? e || t : e || f) *) + | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f} + |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e -> + simp_cond c (simp_or e t) (simp_or e f) + (* e || e ==> e *) + | _ when equal x y -> x + | _ -> App {op= App {op= Or; arg= x}; arg= y} + +let rec simp_not (typ : Typ.t) term = + match (term, typ) with + (* ¬(x = y) ==> x ≠ y *) + | App {op= App {op= Eq; arg= x}; arg= y}, _ -> simp_dq x y + (* ¬(x ≠ y) ==> x = y *) + | App {op= App {op= Dq; arg= x}; arg= y}, _ -> simp_eq x y + (* ¬(x > y) ==> x <= y *) + | App {op= App {op= Gt; arg= x}; arg= y}, _ -> simp_le x y + (* ¬(x >= y) ==> x < y *) + | App {op= App {op= Ge; arg= x}; arg= y}, _ -> simp_lt x y + (* ¬(x < y) ==> x >= y *) + | App {op= App {op= Lt; arg= x}; arg= y}, _ -> simp_ge x y + (* ¬(x <= y) ==> x > y *) + | App {op= App {op= Le; arg= x}; arg= y}, _ -> simp_gt x y + (* ¬(x u> y) ==> x u<= y *) + | App {op= App {op= Ugt; arg= x}; arg= y}, _ -> simp_ule x y + (* ¬(x u>= y) ==> x u< y *) + | App {op= App {op= Uge; arg= x}; arg= y}, _ -> simp_ult x y + (* ¬(x u< y) ==> x u>= y *) + | App {op= App {op= Ult; arg= x}; arg= y}, _ -> simp_uge x y + (* ¬(x u<= y) ==> x u> y *) + | App {op= App {op= Ule; arg= x}; arg= y}, _ -> simp_ugt x y + (* ¬(x ≠ nan ∧ y ≠ nan) ==> x = nan ∨ y = nan *) + | App {op= App {op= Ord; arg= x}; arg= y}, _ -> simp_uno x y + (* ¬(x = nan ∨ y = nan) ==> x ≠ nan ∧ y ≠ nan *) + | App {op= App {op= Uno; arg= x}; arg= y}, _ -> simp_ord x y + (* ¬(a ∧ b) ==> ¬a ∨ ¬b *) + | App {op= App {op= And; arg= x}; arg= y}, Integer {bits= 1} -> + simp_or (simp_not typ x) (simp_not typ y) + (* ¬(a ∨ b) ==> ¬a ∧ ¬b *) + | App {op= App {op= Or; arg= x}; arg= y}, Integer {bits= 1} -> + simp_and (simp_not typ x) (simp_not typ y) + (* ¬(c ? t : e) ==> c ? ¬t : ¬e *) + | ( App {op= App {op= App {op= Conditional; arg= cnd}; arg= thn}; arg= els} + , Integer {bits= 1} ) -> + simp_cond cnd (simp_not typ thn) (simp_not typ els) + (* ¬false ==> true ¬true ==> false *) + | Integer {data}, Integer {bits= 1} -> bool (Z.is_false data) + (* ¬b ==> false = b *) + | b, Integer {bits= 1} -> App {op= App {op= Eq; arg= bool false}; arg= b} + (* ¬e ==> true xor e *) + | e, _ -> + App {op= App {op= Xor; arg= integer (Z.of_bool true) typ}; arg= e} + +and simp_eq x y = + match (x, y) with + | Integer {data= i; typ}, Integer {data= j} -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + (* i = j *) + bool (Z.beq ~bits i j) + | b, Integer {data; typ= Integer {bits= 1}} + |Integer {data; typ= Integer {bits= 1}}, b -> + if Z.is_false data then (* b = false ==> ¬b *) + simp_not Typ.bool b + else (* b = true ==> b *) + b + (* e = (c ? t : f) ==> (c ? e = t : e = f) *) + | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f} + |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e -> + simp_cond c (simp_eq e t) (simp_eq e f) + (* e = e ==> true *) + | x, y when equal x y -> bool true + | x, y -> App {op= App {op= Eq; arg= x}; arg= y} + +and simp_dq x y = + match (x, y) with + (* e ≠ (c ? t : f) ==> (c ? e ≠ t : e ≠ f) *) + | e, App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f} + |App {op= App {op= App {op= Conditional; arg= c}; arg= t}; arg= f}, e -> + simp_cond c (simp_dq e t) (simp_dq e f) + | _ -> ( + match simp_eq x y with + | App {op= App {op= Eq; arg= x}; arg= y} -> + App {op= App {op= Dq; arg= x}; arg= y} + | b -> simp_not Typ.bool b ) + +let simp_xor x y = + match (x, y) with + (* i xor j *) + | Integer {data= i; typ}, Integer {data= j} -> + let bits = Option.value_exn (Typ.prim_bit_size_of typ) in + integer (Z.blogxor ~bits i j) typ + (* true xor b ==> ¬b *) + | Integer {data; typ= Integer {bits= 1}}, b + |b, Integer {data; typ= Integer {bits= 1}} + when Z.is_true data -> + simp_not Typ.bool b + | _ -> App {op= App {op= Xor; arg= x}; arg= y} + +let simp_shl x y = + match (x, y) with + (* i shl j *) + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> + integer (Z.bshift_left ~bits i (Z.to_int j)) typ + (* e shl 0 ==> e *) + | e, Integer {data} when Z.equal Z.zero data -> e + | _ -> App {op= App {op= Shl; arg= x}; arg= y} + +let simp_lshr x y = + match (x, y) with + (* i lshr j *) + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> + integer (Z.bshift_right_trunc ~bits i (Z.to_int j)) typ + (* e lshr 0 ==> e *) + | e, Integer {data} when Z.equal Z.zero data -> e + | _ -> App {op= App {op= Lshr; arg= x}; arg= y} + +let simp_ashr x y = + match (x, y) with + (* i ashr j *) + | Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j} + when Z.sign j >= 0 && Z.lt j (Z.of_int bits) -> + integer (Z.bshift_right ~bits i (Z.to_int j)) typ + (* e ashr 0 ==> e *) + | e, Integer {data} when Z.equal Z.zero data -> e + | _ -> App {op= App {op= Ashr; arg= x}; arg= y} + +(** Access *) + +let iter e ~f = + match e with + | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y} + -> + f x ; f y + | Add {args} | Mul {args} -> Qset.iter ~f:(fun arg _ -> f arg) args + | Concat {args} | Struct_rec {elts= args} -> Vector.iter ~f args + | _ -> () + +let fold e ~init:s ~f = + match e with + | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y} + -> + f y (f x s) + | Add {args} | Mul {args} -> + Qset.fold ~f:(fun e _ s -> f e s) args ~init:s + | Concat {args} | Struct_rec {elts= args} -> + Vector.fold ~f:(fun s e -> f e s) args ~init:s + | _ -> s + +let is_subterm ~sub ~sup = + With_return.with_return + @@ fun {return} -> + iter_terms sup ~f:(fun e -> if equal sub e then return true) ; + false + +let app1 ?(partial = false) op arg = + ( match (op, arg) with + | App {op= Eq; arg= x}, y -> simp_eq x y + | App {op= Dq; arg= x}, y -> simp_dq x y + | App {op= Gt; arg= x}, y -> simp_gt x y + | App {op= Ge; arg= x}, y -> simp_ge x y + | App {op= Lt; arg= x}, y -> simp_lt x y + | App {op= Le; arg= x}, y -> simp_le x y + | App {op= Ugt; arg= x}, y -> simp_ugt x y + | App {op= Uge; arg= x}, y -> simp_uge x y + | App {op= Ult; arg= x}, y -> simp_ult x y + | App {op= Ule; arg= x}, y -> simp_ule x y + | App {op= Ord; arg= x}, y -> simp_ord x y + | App {op= Uno; arg= x}, y -> simp_uno x y + | App {op= Div; arg= x}, y -> simp_div x y + | App {op= Udiv; arg= x}, y -> simp_udiv x y + | App {op= Rem; arg= x}, y -> simp_rem x y + | App {op= Urem; arg= x}, y -> simp_urem x y + | App {op= And; arg= x}, y -> simp_and x y + | App {op= Or; arg= x}, y -> simp_or x y + | App {op= Xor; arg= x}, y -> simp_xor x y + | App {op= Shl; arg= x}, y -> simp_shl x y + | App {op= Lshr; arg= x}, y -> simp_lshr x y + | App {op= Ashr; arg= x}, y -> simp_ashr x y + | App {op= App {op= Conditional; arg= x}; arg= y}, z -> simp_cond x y z + | Convert {signed; dst; src}, x -> simp_convert signed dst src x + | _ -> App {op; arg} ) + |> check (invariant ~partial) + |> check (fun e -> + (* every App subterm of output appears in input *) + match op with + | App {op= Eq | Dq | Xor} -> () + | _ -> ( + match e with + | App {op= App {op= App {op= Conditional}}} -> () + | _ -> + iter e ~f:(function + | App {op= Eq | Dq} -> () + | App _ as a -> + assert ( + is_subterm ~sub:a ~sup:op + || is_subterm ~sub:a ~sup:arg + || Trace.fail + "simplifying %a %a@ yields %a@ with new \ + subterm %a" + pp op pp arg pp e pp a ) + | _ -> () ) ) ) + +let app2 op x y = app1 (app1 ~partial:true op x) y +let app3 op x y z = app1 (app1 ~partial:true (app1 ~partial:true op x) y) z +let addN typ args = simp_add typ args |> check invariant +let mulN typ args = simp_mul typ args |> check invariant + +let check1 op typ x = + type_check x typ ; + op typ x |> check invariant + +let check2 op typ x y = + type_check2 x y typ ; + op typ x y |> check invariant + +let simp_memory siz arr = Memory {siz; arr} + +let memory ~siz ~arr = + type_check siz Typ.siz ; + simp_memory siz arr |> check invariant + +let simp_concat xs = + if Vector.length xs = 1 then Vector.get xs 0 + else + let args = + if Vector.for_all xs ~f:(function Concat _ -> false | _ -> true) + then xs + else + Vector.concat + (Vector.fold_right xs ~init:[] ~f:(fun x s -> + match x with + | Concat {args} -> args :: s + | x -> Vector.of_array [|x|] :: s )) + in + Concat {args} + +let concat xs = simp_concat (Vector.of_array xs) |> check invariant + +let simp_splat byt siz = + match siz with + | Integer {data} when Z.equal Z.zero data -> concat [||] + | _ -> Splat {byt; siz} + +let splat ~byt ~siz = + type_check byt Typ.byt ; + type_check siz Typ.siz ; + simp_splat byt siz |> check invariant + +let eq = app2 Eq +let dq = app2 Dq +let gt = app2 Gt +let ge = app2 Ge +let lt = app2 Lt +let le = app2 Le +let ugt = app2 Ugt +let uge = app2 Uge +let ult = app2 Ult +let ule = app2 Ule +let ord = app2 Ord +let uno = app2 Uno +let neg = check1 simp_negate +let add = check2 simp_add2 +let sub = check2 simp_sub +let mul = check2 simp_mul2 +let div = app2 Div +let udiv = app2 Udiv +let rem = app2 Rem +let urem = app2 Urem +let and_ = app2 And +let or_ = app2 Or +let xor = app2 Xor +let not_ = check1 simp_not +let shl = app2 Shl +let lshr = app2 Lshr +let ashr = app2 Ashr +let conditional ~cnd ~thn ~els = app3 Conditional cnd thn els +let record elts = List.fold ~f:app1 ~init:Record elts +let select ~rcd ~idx = app2 Select rcd idx +let update ~rcd ~elt ~idx = app3 Update rcd elt idx + +let struct_rec key = + let memo_id = Hashtbl.create key in + let dummy = null in + Staged.stage + @@ fun ~id elt_thks -> + match Hashtbl.find memo_id id with + | None -> + (* Add placeholder to prevent computing [elts] in calls to + [struct_rec] from [elt_thks] for recursive occurrences of [id]. *) + let elta = Array.create ~len:(Vector.length elt_thks) dummy in + let elts = Vector.of_array elta in + Hashtbl.set memo_id ~key:id ~data:elts ; + Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ; + Struct_rec {elts} |> check invariant + | Some elts -> + (* Do not check invariant as invariant will be checked above after the + thunks are forced, before which invariant-checking may spuriously + fail. Note that it is important that the value constructed here + shares the array in the memo table, so that the update after + forcing the recursive thunks also updates this value. *) + Struct_rec {elts} + +let convert ?(signed = false) ~dst ~src term = + app1 (Convert {signed; dst; src}) term + +let rec of_exp (e : Exp.t) = + let of_exps exps = + Qset.fold exps ~init:empty_qset ~f:(fun e q ts -> + Qset.add ts (of_exp e) q ) + in + match e with + | Add {args; typ} -> Add {args= of_exps args; typ} + | Mul {args; typ} -> Mul {args= of_exps args; typ} + | Splat {byt; siz} -> Splat {byt= of_exp byt; siz= of_exp siz} + | Memory {siz; arr} -> Memory {siz= of_exp siz; arr= of_exp arr} + | Concat {args} -> Concat {args= Vector.map ~f:of_exp args} + | Reg {id; name} -> Var {id; name} + | Nondet {msg} -> Nondet {msg} + | Label {parent; name} -> Label {parent; name} + | App {op; arg} -> App {op= of_exp op; arg= of_exp arg} + | Eq -> Eq + | Dq -> Dq + | Gt -> Gt + | Ge -> Ge + | Lt -> Lt + | Le -> Le + | Ugt -> Ugt + | Uge -> Uge + | Ult -> Ult + | Ule -> Ule + | Ord -> Ord + | Uno -> Uno + | Div -> Div + | Udiv -> Udiv + | Rem -> Rem + | Urem -> Urem + | And -> And + | Or -> Or + | Xor -> Xor + | Shl -> Shl + | Lshr -> Lshr + | Ashr -> Ashr + | Conditional -> Conditional + | Record -> Record + | Select -> Select + | Update -> Update + | Struct_rec {elts} -> + Staged.unstage + (struct_rec (module Exp)) + ~id:e + (Vector.map elts ~f:(fun e -> lazy (of_exp e))) + | Convert {signed; dst; src} -> Convert {signed; dst; src} + | Integer {data; typ} -> Integer {data; typ} + | Float {data} -> Float {data} + +let size_of t = + Option.bind (Typ.prim_bit_size_of t) ~f:(fun n -> + if n % 8 = 0 then Some (integer (Z.of_int (n / 8)) Typ.siz) else None + ) + +(** Transform *) + +let map e ~f = + let map_ : (t -> t) -> t -> t = + fun map_ e -> + let map_bin mk ~f x y = + let x' = f x in + let y' = f y in + if x' == x && y' == y then e else mk x' y' + in + let map_vector mk ~f args = + let args' = Vector.map_preserving_phys_equal ~f args in + if args' == args then e else mk args' + in + let map_qset mk typ ~f args = + let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in + if args' == args then e else mk typ args' + in + match e with + | App {op; arg} -> map_bin (app1 ~partial:true) ~f op arg + | Add {args; typ} -> map_qset addN typ ~f args + | Mul {args; typ} -> map_qset mulN typ ~f args + | Splat {byt; siz} -> map_bin simp_splat ~f byt siz + | Memory {siz; arr} -> map_bin simp_memory ~f siz arr + | Concat {args} -> map_vector simp_concat ~f args + | Struct_rec {elts= args} -> Struct_rec {elts= Vector.map args ~f:map_} + | _ -> e + in + fix map_ (fun e -> e) e + +let rename sub e = + let rec rename_ sub e = + match e with + | Var _ -> Var.Subst.apply sub e + | _ -> map ~f:(rename_ sub) e + in + rename_ sub e |> check (invariant ~partial:true) + +(** Query *) + +let is_true = function + | Integer {data; typ= Integer {bits= 1}} -> Z.is_true data + | _ -> false + +let is_false = function + | Integer {data; typ= Integer {bits= 1}} -> Z.is_false data + | _ -> false + +let rec is_constant e = + let is_constant_bin x y = is_constant x && is_constant y in + match e with + | Var _ | Nondet _ -> false + | App {op= x; arg= y} | Splat {byt= x; siz= y} | Memory {siz= x; arr= y} + -> + is_constant_bin x y + | Add {args} | Mul {args} -> + Qset.for_all ~f:(fun arg _ -> is_constant arg) args + | Concat {args} | Struct_rec {elts= args} -> + Vector.for_all ~f:is_constant args + | _ -> true + +let classify = function + | Add _ | Mul _ -> `Interpreted + | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Simplified + | App _ -> `Uninterpreted + | _ -> `Atomic + +let solve e f = + [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f] + ; + let rec solve_ e f s = + let solve_uninterp e f = + let ord = compare e f in + match (is_constant e, is_constant f) with + | true, true when ord <> 0 -> None + (* orient equation to discretionarily prefer term that is constant or + compares smaller as class representative *) + | true, false -> Some (Map.add_exn s ~key:f ~data:e) + | false, true -> Some (Map.add_exn s ~key:e ~data:f) + | _ -> + let key, data = if ord > 0 then (e, f) else (f, e) in + Some (Map.add_exn s ~key ~data) + in + let concat_size args = + Vector.fold_until args ~init:(integer Z.zero Typ.siz) + ~f:(fun sum -> function + | Memory {siz} -> Continue (add Typ.siz siz sum) | _ -> Stop None + ) + ~finish:(fun _ -> None) + in + match (e, f) with + | (Add {typ} | Mul {typ} | Integer {typ}), _ + |_, (Add {typ} | Mul {typ} | Integer {typ}) -> ( + match sub typ e f with + | Add {args} -> + let c, q = Qset.min_elt_exn args in + let n = Sum.to_term typ (Qset.remove args c) in + let d = rational (Q.neg q) typ in + let r = div n d in + Some (Map.add_exn s ~key:c ~data:r) + | e_f -> solve_uninterp e_f (zero typ) ) + | Concat {args= ms}, Concat {args= ns} -> ( + match (concat_size ms, concat_size ns) with + | Some p, Some q -> solve_uninterp e f >>= solve_ p q + | _ -> solve_uninterp e f ) + | Memory {siz= m}, Concat {args= ns} | Concat {args= ns}, Memory {siz= m} + -> ( + match concat_size ns with + | Some p -> solve_uninterp e f >>= solve_ p m + | _ -> solve_uninterp e f ) + | _ -> solve_uninterp e f + in + solve_ e f empty_map + |> + [%Trace.retn fun {pf} -> + function Some s -> pf "%a" Var.Subst.pp s | None -> pf "false"] diff --git a/sledge/src/symbheap/term.mli b/sledge/src/symbheap/term.mli new file mode 100644 index 000000000..e7dddf643 --- /dev/null +++ b/sledge/src/symbheap/term.mli @@ -0,0 +1,219 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Terms + + Pure (heap-independent) terms are complex arithmetic, bitwise-logical, + etc. operations over literal values and variables. + + Terms for operations that are uninterpreted in the analyzer are + represented in curried form, where [App] is an application of a function + symbol to an argument. This is done to simplify the definition of + 'subterm' and make it explicit. The specific constructor functions + indicate and check the expected arity of the function symbols. *) + +type comparator_witness + +type qset = (t, comparator_witness) Qset.t + +and t = private + | Add of {args: qset; typ: Typ.t} (** Addition *) + | Mul of {args: qset; typ: Typ.t} (** Multiplication *) + | Splat of {byt: t; siz: t} + (** Iterated concatenation of a single byte *) + | Memory of {siz: t; arr: t} (** Size-tagged byte-array *) + | Concat of {args: t vector} (** Byte-array concatenation *) + | Var of {id: int; name: string} (** Local variable / virtual register *) + | Nondet of {msg: string} + (** Anonymous local variable with arbitrary value, representing + non-deterministic approximation of value described by [msg] *) + | Label of {parent: string; name: string} + (** Address of named code block within parent function *) + | App of {op: t; arg: t} + (** Application of function symbol to argument, curried *) + | Eq (** Equal test *) + | Dq (** Disequal test *) + | Gt (** Greater-than test *) + | Ge (** Greater-than-or-equal test *) + | Lt (** Less-than test *) + | Le (** Less-than-or-equal test *) + | Ugt (** Unsigned greater-than test *) + | Uge (** Unsigned greater-than-or-equal test *) + | Ult (** Unsigned less-than test *) + | Ule (** Unsigned less-than-or-equal test *) + | Ord (** Ordered test (neither arg is nan) *) + | Uno (** Unordered test (some arg is nan) *) + | Div (** Division *) + | Udiv (** Unsigned division *) + | Rem (** Remainder of division *) + | Urem (** Remainder of unsigned division *) + | And (** Conjunction, boolean or bitwise *) + | Or (** Disjunction, boolean or bitwise *) + | Xor (** Exclusive-or, bitwise *) + | Shl (** Shift left, bitwise *) + | Lshr (** Logical shift right, bitwise *) + | Ashr (** Arithmetic shift right, bitwise *) + | Conditional (** If-then-else *) + | Record (** Record (array / struct) constant *) + | Select (** Select an index from a record *) + | Update (** Constant record with updated index *) + | Struct_rec of {elts: t vector} + (** Struct constant that may recursively refer to itself + (transitively) from [elts]. NOTE: represented by cyclic values. *) + | Convert of {signed: bool; dst: Typ.t; src: Typ.t} + (** Convert between specified types, possibly with loss of information *) + | Integer of {data: Z.t; typ: Typ.t} + (** Integer constant, or if [typ] is a [Pointer], null pointer value + that never refers to an object *) + | Float of {data: string} (** Floating-point constant *) +[@@deriving compare, equal, hash, sexp] + +val comparator : (t, comparator_witness) Comparator.t + +type term = t + +val pp_full : ?is_x:(term -> bool) -> t pp +val pp : t pp +val invariant : ?partial:bool -> t -> unit + +(** Term.Var is re-exported as Var *) +module Var : sig + type t = private term [@@deriving compare, equal, hash, sexp] + type var = t + + include Comparator.S with type t := t + + module Set : sig + type t = (var, comparator_witness) Set.t + [@@deriving compare, equal, sexp] + + val pp_full : ?is_x:(term -> bool) -> t pp + val pp : t pp + val empty : t + val of_option : var option -> t + val of_list : var list -> t + val of_vector : var vector -> t + val of_regs : Reg.Set.t -> t + end + + module Map : sig + type 'a t = (var, 'a, comparator_witness) Map.t + [@@deriving compare, equal, sexp] + + val empty : 'a t + end + + val pp : t pp + val pp_demangled : t pp + + include Invariant.S with type t := t + + val of_reg : Reg.t -> t + val of_term : term -> t option + val program : string -> t + val fresh : string -> wrt:Set.t -> t * Set.t + val id : t -> int + val name : t -> string + + module Subst : sig + type t [@@deriving compare, equal, sexp] + + val pp : t pp + val empty : t + val freshen : Set.t -> wrt:Set.t -> t + val extend : t -> replace:var -> with_:var -> t + val invert : t -> t + val exclude : t -> Set.t -> t + val restrict : t -> Set.t -> t + val is_empty : t -> bool + val domain : t -> Set.t + val range : t -> Set.t + val apply_set : t -> Set.t -> Set.t + val close_set : t -> Set.t -> Set.t + end +end + +(** Construct *) + +val of_exp : Exp.t -> t +val var : Var.t -> t +val nondet : string -> t +val label : parent:string -> name:string -> t +val null : t +val splat : byt:t -> siz:t -> t +val memory : siz:t -> arr:t -> t +val concat : t array -> t +val bool : bool -> t +val integer : Z.t -> Typ.t -> t +val rational : Q.t -> Typ.t -> t +val float : string -> t +val eq : t -> t -> t +val dq : t -> t -> t +val gt : t -> t -> t +val ge : t -> t -> t +val lt : t -> t -> t +val le : t -> t -> t +val ugt : t -> t -> t +val uge : t -> t -> t +val ult : t -> t -> t +val ule : t -> t -> t +val ord : t -> t -> t +val uno : t -> t -> t +val neg : Typ.t -> t -> t +val add : Typ.t -> t -> t -> t +val sub : Typ.t -> t -> t -> t +val mul : Typ.t -> t -> t -> t +val div : t -> t -> t +val udiv : t -> t -> t +val rem : t -> t -> t +val urem : t -> t -> t +val and_ : t -> t -> t +val or_ : t -> t -> t +val xor : t -> t -> t +val not_ : Typ.t -> t -> t +val shl : t -> t -> t +val lshr : t -> t -> t +val ashr : t -> t -> t +val conditional : cnd:t -> thn:t -> els:t -> t +val record : t list -> t +val select : rcd:t -> idx:t -> t +val update : rcd:t -> elt:t -> idx:t -> t + +val struct_rec : + (module Hashtbl.Key with type t = 'id) + -> (id:'id -> t lazy_t vector -> t) Staged.t +(** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct] + value. Cycles are detected using [Id]. The caller of [struct_rec Id] + must ensure that a single unstaging of [struct_rec Id] is used for each + complete cyclic value. Also, the caller must ensure that recursive calls + to [struct_rec Id] provide [id] values that uniquely identify at least + one point on each cycle. Failure to obey these requirements will lead to + stack overflow. *) + +val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t +val size_of : Typ.t -> t option + +(** Access *) + +val iter : t -> f:(t -> unit) -> unit +val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a +val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a +val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a + +(** Transform *) + +val map : t -> f:(t -> t) -> t +val rename : Var.Subst.t -> t -> t + +(** Query *) + +val fv : t -> Var.Set.t +val is_true : t -> bool +val is_false : t -> bool +val typ : t -> Typ.t option +val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted] +val solve : t -> t -> (t, t, comparator_witness) Map.t option diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/symbheap/term_test.ml similarity index 81% rename from sledge/src/llair/exp_test.ml rename to sledge/src/symbheap/term_test.ml index 6cc5b954a..6f23d2670 100644 --- a/sledge/src/llair/exp_test.ml +++ b/sledge/src/symbheap/term_test.ml @@ -9,48 +9,50 @@ let%test_module _ = ( module struct (* let () = Trace.init ~margin:68 ~config:all () *) let () = Trace.init ~margin:68 ~config:none () - let pp = Format.printf "@\n%a@." Exp.pp + let pp = Format.printf "@\n%a@." Term.pp let char = Typ.integer ~bits:8 - let ( ! ) i = Exp.integer (Z.of_int i) char - let ( + ) = Exp.add char - let ( - ) = Exp.sub char - let ( * ) = Exp.mul char - let ( = ) = Exp.eq - let ( != ) = Exp.dq - let ( > ) = Exp.gt - let ( >= ) = Exp.ge - let ( < ) = Exp.lt - let ( <= ) = Exp.le - let ( && ) = Exp.and_ - let ( || ) = Exp.or_ - let ( ~~ ) = Exp.not_ Typ.bool + let ( ! ) i = Term.integer (Z.of_int i) char + let ( + ) = Term.add char + let ( - ) = Term.sub char + let ( * ) = Term.mul char + let ( = ) = Term.eq + let ( != ) = Term.dq + let ( > ) = Term.gt + let ( >= ) = Term.ge + let ( < ) = Term.lt + let ( <= ) = Term.le + let ( && ) = Term.and_ + let ( || ) = Term.or_ + let ( ~~ ) = Term.not_ Typ.bool let wrt = Var.Set.empty let y_, wrt = Var.fresh "y" ~wrt let z_, _ = Var.fresh "z" ~wrt - let y = Exp.var y_ - let z = Exp.var z_ + let y = Term.var y_ + let z = Term.var z_ let%test "booleans distinct" = - Exp.is_false - (Exp.eq - (Exp.integer Z.minus_one Typ.bool) - (Exp.integer Z.zero Typ.bool)) + Term.is_false + (Term.eq + (Term.integer Z.minus_one Typ.bool) + (Term.integer Z.zero Typ.bool)) let%test "unsigned booleans distinct" = - Exp.is_false - (Exp.eq (Exp.integer Z.one Typ.bool) (Exp.integer Z.zero Typ.bool)) + Term.is_false + (Term.eq + (Term.integer Z.one Typ.bool) + (Term.integer Z.zero Typ.bool)) let%test "boolean overflow" = - Exp.is_true - (Exp.eq - (Exp.integer Z.minus_one Typ.bool) - (Exp.integer Z.one Typ.bool)) + Term.is_true + (Term.eq + (Term.integer Z.minus_one Typ.bool) + (Term.integer Z.one Typ.bool)) let%test "unsigned boolean overflow" = - Exp.is_true - (Exp.uge - (Exp.integer Z.minus_one Typ.bool) - (Exp.integer Z.one Typ.bool)) + Term.is_true + (Term.uge + (Term.integer Z.minus_one Typ.bool) + (Term.integer Z.one Typ.bool)) let%expect_test _ = pp (!42 + !13) ; @@ -176,19 +178,19 @@ let%test_module _ = [%expect {| 0 |}] let%expect_test _ = - pp (!3 * y = z = Exp.bool true) ; + pp (!3 * y = z = Term.bool true) ; [%expect {| ((3 × %y_1) = %z_2) |}] let%expect_test _ = - pp (Exp.bool true = (!3 * y = z)) ; + pp (Term.bool true = (!3 * y = z)) ; [%expect {| ((3 × %y_1) = %z_2) |}] let%expect_test _ = - pp (!3 * y = z = Exp.bool false) ; + pp (!3 * y = z = Term.bool false) ; [%expect {| ((3 × %y_1) ≠ %z_2) |}] let%expect_test _ = - pp (Exp.bool false = (!3 * y = z)) ; + pp (Term.bool false = (!3 * y = z)) ; [%expect {| ((3 × %y_1) ≠ %z_2) |}] let%expect_test _ = @@ -208,11 +210,11 @@ let%test_module _ = [%expect {| ((-3 × %y_1 + 4) = %y_1) |}] let%expect_test _ = - pp (Exp.sub Typ.bool (Exp.bool true) (z = !4)) ; + pp (Term.sub Typ.bool (Term.bool true) (z = !4)) ; [%expect {| (-1 × (%z_2 = 4) + -1) |}] let%expect_test _ = - pp (Exp.add Typ.bool (Exp.bool true) (z = !4) = (z = !4)) ; + pp (Term.add Typ.bool (Term.bool true) (z = !4) = (z = !4)) ; [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}] let%expect_test _ = @@ -244,9 +246,9 @@ let%test_module _ = [%expect {| ((%y_1 < 2) && (%z_2 ≥ 3)) |}] let%expect_test _ = - pp Exp.(eq z null) ; - pp Exp.(eq null z) ; - pp Exp.(dq (eq null z) (bool false)) ; + pp Term.(eq z null) ; + pp Term.(eq null z) ; + pp Term.(dq (eq null z) (bool false)) ; [%expect {| (%z_2 = null) diff --git a/sledge/src/llair/exp_test.mli b/sledge/src/symbheap/term_test.mli similarity index 100% rename from sledge/src/llair/exp_test.mli rename to sledge/src/symbheap/term_test.mli diff --git a/sledge/src/llair/var.ml b/sledge/src/symbheap/var.ml similarity index 92% rename from sledge/src/llair/var.ml rename to sledge/src/symbheap/var.ml index bcc0b0865..0b93a52e0 100644 --- a/sledge/src/llair/var.ml +++ b/sledge/src/symbheap/var.ml @@ -7,4 +7,4 @@ (** Variables *) -include Exp.Var +include Term.Var diff --git a/sledge/src/llair/var.mli b/sledge/src/symbheap/var.mli similarity index 86% rename from sledge/src/llair/var.mli rename to sledge/src/symbheap/var.mli index 64bdc2169..d4d909555 100644 --- a/sledge/src/llair/var.mli +++ b/sledge/src/symbheap/var.mli @@ -7,4 +7,4 @@ (** Variables *) -include module type of Exp.Var +include module type of Term.Var