From 1643bf1c505829444d81ae8720947621e6ec6c9d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 27 Oct 2020 12:16:38 -0700 Subject: [PATCH] [sledge] Factor core Fol modules into separate modules Summary: The Fol.Term and Fol.Formula provide an interface which supports if-then-else terms and formulas, while the underlying representation in Trm does not and Fml only supports if-then-else over formulas, not terms. The implementation of the rest of the first-order solver needs to use the underlying, normalized, representation. This diff exports Trm and Fml to separate modules for this purpose. Later, they will be packed into a library for the first-order solver, and only used from within. Reviewed By: ngorogiannis Differential Revision: D24532351 fbshipit-source-id: 7310827da --- sledge/src/arithmetic_intf.ml | 2 +- sledge/src/fml.ml | 84 ++++++ sledge/src/fml.mli | 22 ++ sledge/src/fol.ml | 474 +--------------------------------- sledge/src/fol.mli | 9 +- sledge/src/propositional.ml | 3 +- sledge/src/solver.mli | 2 - sledge/src/trm.ml | 392 ++++++++++++++++++++++++++++ sledge/src/trm.mli | 65 +++++ sledge/src/var.ml | 10 + sledge/src/var.mli | 10 + 11 files changed, 594 insertions(+), 479 deletions(-) create mode 100644 sledge/src/fml.ml create mode 100644 sledge/src/fml.mli create mode 100644 sledge/src/trm.ml create mode 100644 sledge/src/trm.mli create mode 100644 sledge/src/var.ml create mode 100644 sledge/src/var.mli diff --git a/sledge/src/arithmetic_intf.ml b/sledge/src/arithmetic_intf.ml index 5f9759ec7..c306102c4 100644 --- a/sledge/src/arithmetic_intf.ml +++ b/sledge/src/arithmetic_intf.ml @@ -7,7 +7,7 @@ (** Arithmetic terms *) -open Ses +module Var = Ses.Var module type S = sig type var diff --git a/sledge/src/fml.ml b/sledge/src/fml.ml new file mode 100644 index 000000000..d1a82800d --- /dev/null +++ b/sledge/src/fml.ml @@ -0,0 +1,84 @@ +(* + * 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. + *) + +(** Formulas *) + +module Prop = Propositional.Make (Trm) +module Fmls = Prop.Fmls + +type fmls = Fmls.t + +include Prop.Fml + +let tt = mk_Tt () +let ff = _Not tt +let bool b = if b then tt else ff + +let _Eq0 x = + match (x : Trm.trm) with + | Z z -> bool (Z.equal Z.zero z) + | Q q -> bool (Q.equal Q.zero q) + | x -> _Eq0 x + +let _Pos x = + match (x : Trm.trm) with + | Z z -> bool (Z.gt z Z.zero) + | Q q -> bool (Q.gt q Q.zero) + | x -> _Pos x + +let _Eq x y = + if x == Trm.zero then _Eq0 y + else if y == Trm.zero then _Eq0 x + else + let sort_eq x y = + match Sign.of_int (Trm.compare_trm x y) with + | Neg -> _Eq x y + | Zero -> tt + | Pos -> _Eq y x + in + match (x, y) with + (* x = y ==> 0 = x - y when x = y is an arithmetic equality *) + | (Z _ | Q _ | Arith _), _ | _, (Z _ | Q _ | Arith _) -> + _Eq0 (Trm.sub x y) + (* α^β^δ = α^γ^δ ==> β = γ *) + | Concat a, Concat b -> + let m = Array.length a in + let n = Array.length b in + let l = min m n in + let length_common_prefix = + let rec find_lcp i = + if i < l && Trm.equal_trm a.(i) b.(i) then find_lcp (i + 1) + else i + in + find_lcp 0 + in + if length_common_prefix = l then tt + else + let length_common_suffix = + let rec find_lcs i = + if Trm.equal_trm a.(m - 1 - i) b.(n - 1 - i) then + find_lcs (i + 1) + else i + in + find_lcs 0 + in + let length_common = length_common_prefix + length_common_suffix in + if length_common = 0 then sort_eq x y + else + let pos = length_common_prefix in + let a = Array.sub ~pos ~len:(m - length_common) a in + let b = Array.sub ~pos ~len:(n - length_common) b in + _Eq (Trm._Concat a) (Trm._Concat b) + | (Sized _ | Extract _ | Concat _), (Sized _ | Extract _ | Concat _) -> + sort_eq x y + (* x = α ==> ⟨x,|α|⟩ = α *) + | x, ((Sized _ | Extract _ | Concat _) as a) + |((Sized _ | Extract _ | Concat _) as a), x -> + _Eq (Trm._Sized x (Trm.seq_size_exn a)) a + | _ -> sort_eq x y + +let vars p = Iter.flat_map ~f:Trm.vars (trms p) diff --git a/sledge/src/fml.mli b/sledge/src/fml.mli new file mode 100644 index 000000000..e413888ce --- /dev/null +++ b/sledge/src/fml.mli @@ -0,0 +1,22 @@ +(* + * 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. + *) + +(** Formulas *) + +open Propositional_intf +include FORMULA with type trm := Trm.trm +module Fmls : FORMULA_SET with type elt := fml with type t = fmls + +type trm := Trm.trm + +val tt : fml +val ff : fml +val bool : bool -> fml +val _Eq0 : trm -> fml +val _Pos : trm -> fml +val _Eq : trm -> trm -> fml +val vars : fml -> Trm.Var.t iter diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 7b974f39e..48d280816 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -5,475 +5,11 @@ * LICENSE file in the root directory of this source tree. *) -open Ses - -let pp_boxed fs fmt = - Format.pp_open_box fs 2 ; - Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt - -(* - * Terms - *) - -(** Variable terms, represented as a subtype of general terms *) -module rec Var : sig - include Var_intf.VAR with type t = private Trm.trm - - val of_ : Trm.trm -> t -end = struct - module T = struct - type t = Trm.trm [@@deriving compare, equal, sexp] - - let invariant x = - let@ () = Invariant.invariant [%here] x [%sexp_of: t] in - match x with - | Var _ -> () - | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) () - - let make ~id ~name = Trm._Var id name |> check invariant - let id = function Trm.Var v -> v.id | x -> violates invariant x - let name = function Trm.Var v -> v.name | x -> violates invariant x - end - - include Var0.Make (T) - - let of_ v = v |> check T.invariant -end - -and Arith0 : - (Arithmetic.REPRESENTATION - with type var := Var.t - with type trm := Trm.trm) = - Arithmetic.Representation (Trm) - -and Arith : - (Arithmetic.S - with type var := Var.t - with type trm := Trm.trm - with type t = Arith0.t) = struct - include Arith0 - - include Make (struct - let get_arith (e : Trm.trm) = - match e with - | Z z -> Some (Arith.const (Q.of_z z)) - | Q q -> Some (Arith.const q) - | Arith a -> Some a - | _ -> None - end) -end - -(** Terms, built from variables and applications of function symbols from - various theories. Denote functions from structures to values. *) -and Trm : sig - type var = Var.t - - type trm = private - (* variables *) - | Var of {id: int; name: string} - (* arithmetic *) - | Z of Z.t - | Q of Q.t - | Arith of Arith.t - (* sequences (of flexible size) *) - | Splat of trm - | Sized of {seq: trm; siz: trm} - | Extract of {seq: trm; off: trm; len: trm} - | Concat of trm array - (* records (with fixed indices) *) - | Select of {idx: int; rcd: trm} - | Update of {idx: int; rcd: trm; elt: trm} - | Record of trm array - | Ancestor of int - (* uninterpreted *) - | Apply of Funsym.t * trm array - [@@deriving compare, equal, sexp] - - val ppx : Var.t Var.strength -> trm pp - val _Var : int -> string -> trm - val _Z : Z.t -> trm - val _Q : Q.t -> trm - val _Arith : Arith.t -> trm - val _Splat : trm -> trm - val _Sized : trm -> trm -> trm - val _Extract : trm -> trm -> trm -> trm - val _Concat : trm array -> trm - val _Select : int -> trm -> trm - val _Update : int -> trm -> trm -> trm - val _Record : trm array -> trm - val _Ancestor : int -> trm - val _Apply : Funsym.t -> trm array -> trm - val add : trm -> trm -> trm - val sub : trm -> trm -> trm - val seq_size_exn : trm -> trm - val vars : trm -> Var.t iter -end = struct - type var = Var.t - - type trm = - | Var of {id: int; name: string} - | Z of Z.t - | Q of Q.t - | Arith of Arith.t - | Splat of trm - | Sized of {seq: trm; siz: trm} - | Extract of {seq: trm; off: trm; len: trm} - | Concat of trm array - | Select of {idx: int; rcd: trm} - | Update of {idx: int; rcd: trm; elt: trm} - | Record of trm array - | Ancestor of int - | Apply of Funsym.t * trm array - [@@deriving compare, equal, sexp] - - let compare_trm x y = - if x == y then 0 - else - match (x, y) with - | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> - Int.compare i j - | _ -> compare_trm x y - - let equal_trm x y = - x == y - || - match (x, y) with - | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> - Int.equal i j - | _ -> equal_trm x y - - let rec ppx strength fs trm = - let rec pp fs trm = - let pf fmt = pp_boxed fs fmt in - match trm with - | Var _ as v -> Var.ppx strength fs (Var.of_ v) - | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z - | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q - | Arith a -> Arith.ppx strength fs a - | Splat x -> pf "%a^" pp x - | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq - | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len - | Concat [||] -> pf "@<2>⟨⟩" - | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs - | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx - | Update {idx; rcd; elt} -> - pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt - | Record xs -> pf "{%a}" (ppx_record strength) xs - | Ancestor i -> pf "(ancestor %i)" i - | Apply (f, [||]) -> pf "%a" Funsym.pp f - | Apply - ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr) - as f ) - , [|x; y|] ) -> - pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y - | Apply (f, es) -> - pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx strength)) es - in - pp fs trm - - and ppx_record strength fs elts = - [%Trace.fprintf - fs "%a" - (fun fs elts -> - let exception Not_a_string in - match - String.init (Array.length elts) ~f:(fun i -> - match elts.(i) with - | Z c -> Char.of_int_exn (Z.to_int c) - | _ -> raise Not_a_string ) - with - | s -> Format.fprintf fs "%S" s - | exception (Not_a_string | Z.Overflow | Failure _) -> - Format.fprintf fs "@[%a@]" - (Array.pp ",@ " (ppx strength)) - elts ) - elts] - - let pp = ppx (fun _ -> None) - - let invariant e = - let@ () = Invariant.invariant [%here] e [%sexp_of: trm] in - match e with - | Q q -> assert (not (Z.equal Z.one (Q.den q))) - | Arith a -> ( - match Arith.classify a with - | Compound -> () - | Trm _ | Const _ -> assert false ) - | _ -> () - - (* destructors *) - - let get_z = function Z z -> Some z | _ -> None - let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None - - (* constructors *) - - let _Var id name = Var {id; name} |> check invariant - - (* statically allocated since they are tested with == *) - let zero = Z Z.zero |> check invariant - let one = Z Z.one |> check invariant - - let _Z z = - (if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z) - |> check invariant - - let _Q q = - (if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q) - |> check invariant - - let _Arith a = - ( match Arith.classify a with - | Trm e -> e - | Const q -> _Q q - | Compound -> Arith a ) - |> check invariant - - let add x y = _Arith Arith.(add (trm x) (trm y)) - let sub x y = _Arith Arith.(sub (trm x) (trm y)) - let _Splat x = Splat x |> check invariant - - let seq_size_exn = - let invalid = Invalid_argument "seq_size_exn" in - let rec seq_size_exn = function - | Sized {siz= n} | Extract {len= n} -> n - | Concat a0U -> - Array.fold ~f:(fun aJ a0I -> add a0I (seq_size_exn aJ)) a0U zero - | _ -> raise invalid - in - seq_size_exn - - let seq_size e = - try Some (seq_size_exn e) with Invalid_argument _ -> None - - let _Sized seq siz = - ( match seq_size seq with - (* ⟨n,α⟩ ==> α when n ≡ |α| *) - | Some n when equal_trm siz n -> seq - | _ -> Sized {seq; siz} ) - |> check invariant - - let partial_compare x y = - match sub x y with - | Z z -> Some (Int.sign (Z.sign z)) - | Q q -> Some (Int.sign (Q.sign q)) - | _ -> None - - let partial_ge x y = - match partial_compare x y with Some (Pos | Zero) -> true | _ -> false - - let empty_seq = Concat [||] - - let rec _Extract seq off len = - [%trace] - ~call:(fun {pf} -> pf "%a" pp (Extract {seq; off; len})) - ~retn:(fun {pf} -> pf "%a" pp) - @@ fun () -> - (* _[_,0) ==> ⟨⟩ *) - ( if equal_trm len zero then empty_seq - else - let o_l = add off len in - match seq with - (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *) - | Extract {seq= a; off= m; len= k} when partial_ge k o_l -> - _Extract a (add m off) len - (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *) - | Sized {siz= n; seq= Splat _ as e} when partial_ge n o_l -> - _Sized e len - (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *) - | Sized {siz= n} when equal_trm off zero && equal_trm n len -> seq - (* For (α₀^α₁)[o,l) there are 3 cases: - * - * ⟨...⟩^⟨...⟩ - * [,) - * o < o+l ≤ |α₀| : (α₀^α₁)[o,l) ==> α₀[o,l) ^ α₁[0,0) - * - * ⟨...⟩^⟨...⟩ - * [ , ) - * o ≤ |α₀| < o+l : (α₀^α₁)[o,l) ==> α₀[o,|α₀|-o) ^ α₁[0,l-(|α₀|-o)) - * - * ⟨...⟩^⟨...⟩ - * [,) - * |α₀| ≤ o : (α₀^α₁)[o,l) ==> α₀[o,0) ^ α₁[o-|α₀|,l) - * - * So in general: - * - * (α₀^α₁)[o,l) ==> α₀[o,l₀) ^ α₁[o₁,l-l₀) - * where l₀ = max 0 (min l |α₀|-o) - * o₁ = max 0 o-|α₀| - *) - | Concat na1N -> ( - match len with - | Z l -> - Array.fold_map_until na1N (l, off) - ~f:(fun naI (l, oI) -> - if Z.equal Z.zero l then - `Continue (_Extract naI oI zero, (l, oI)) - else - let nI = seq_size_exn naI in - let oI_nI = sub oI nI in - match oI_nI with - | Z z -> - let oJ = if Z.sign z <= 0 then zero else oI_nI in - let lI = Z.(max zero (min l (neg z))) in - let l = Z.(l - lI) in - `Continue (_Extract naI oI (_Z lI), (l, oJ)) - | _ -> `Stop (Extract {seq; off; len}) ) - ~finish:(fun (e1N, _) -> _Concat e1N) - | _ -> Extract {seq; off; len} ) - (* α[o,l) *) - | _ -> Extract {seq; off; len} ) - |> check invariant - - and _Concat xs = - [%trace] - ~call:(fun {pf} -> pf "%a" pp (Concat xs)) - ~retn:(fun {pf} -> pf "%a" pp) - @@ fun () -> - (* (α^(β^γ)^δ) ==> (α^β^γ^δ) *) - let flatten xs = - if Array.exists ~f:(function Concat _ -> true | _ -> false) xs then - Array.flat_map ~f:(function Concat s -> s | e -> [|e|]) xs - else xs - in - let simp_adjacent e f = - match (e, f) with - (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *) - | ( Extract {seq= Sized {siz= n} as na; off= o; len= k} - , Extract {seq= na'; off= o_k; len= l} ) - when equal_trm na na' - && equal_trm o_k (add o k) - && partial_ge n (add o_k l) -> - Some (_Extract na o (add k l)) - (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *) - | Sized {siz= m; seq= Splat _ as a}, Sized {siz= n; seq= a'} - when equal_trm a a' -> - Some (_Sized a (add m n)) - | _ -> None - in - let xs = flatten xs in - let xs = Array.reduce_adjacent ~f:simp_adjacent xs in - (if Array.length xs = 1 then xs.(0) else Concat xs) |> check invariant - - let _Select idx rcd = Select {idx; rcd} |> check invariant - let _Update idx rcd elt = Update {idx; rcd; elt} |> check invariant - let _Record es = Record es |> check invariant - let _Ancestor i = Ancestor i |> check invariant - - let _Apply f es = - ( match - Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es - with - | Some c -> c - | None -> Apply (f, es) ) - |> check invariant - - let rec iter_vars e ~f = - match e with - | Var _ as v -> f (Var.of_ v) - | Z _ | Q _ | Ancestor _ -> () - | Splat x | Select {rcd= x} -> iter_vars ~f x - | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} -> - iter_vars ~f x ; - iter_vars ~f y - | Extract {seq= x; off= y; len= z} -> - iter_vars ~f x ; - iter_vars ~f y ; - iter_vars ~f z - | Concat xs | Record xs | Apply (_, xs) -> - Array.iter ~f:(iter_vars ~f) xs - | Arith a -> Iter.iter ~f:(iter_vars ~f) (Arith.iter a) - - let vars e = Iter.from_labelled_iter (iter_vars e) -end - open Trm - -let zero = _Z Z.zero -let one = _Z Z.one - -(* - * Formulas - *) - -module Prop = Propositional.Make (Trm) - -module Fml = struct - include Prop.Fml - - let tt = mk_Tt () - let ff = _Not tt - let bool b = if b then tt else ff - - let _Eq0 = function - | Z z -> bool (Z.equal Z.zero z) - | Q q -> bool (Q.equal Q.zero q) - | x -> _Eq0 x - - let _Pos = function - | Z z -> bool (Z.gt z Z.zero) - | Q q -> bool (Q.gt q Q.zero) - | x -> _Pos x - - let _Eq x y = - if x == zero then _Eq0 y - else if y == zero then _Eq0 x - else - let sort_eq x y = - match Sign.of_int (compare_trm x y) with - | Neg -> _Eq x y - | Zero -> tt - | Pos -> _Eq y x - in - match (x, y) with - (* x = y ==> 0 = x - y when x = y is an arithmetic equality *) - | (Z _ | Q _ | Arith _), _ | _, (Z _ | Q _ | Arith _) -> - _Eq0 (sub x y) - (* α^β^δ = α^γ^δ ==> β = γ *) - | Concat a, Concat b -> - let m = Array.length a in - let n = Array.length b in - let l = min m n in - let length_common_prefix = - let rec find_lcp i = - if i < l && equal_trm a.(i) b.(i) then find_lcp (i + 1) else i - in - find_lcp 0 - in - if length_common_prefix = l then tt - else - let length_common_suffix = - let rec find_lcs i = - if equal_trm a.(m - 1 - i) b.(n - 1 - i) then - find_lcs (i + 1) - else i - in - find_lcs 0 - in - let length_common = - length_common_prefix + length_common_suffix - in - if length_common = 0 then sort_eq x y - else - let pos = length_common_prefix in - let a = Array.sub ~pos ~len:(m - length_common) a in - let b = Array.sub ~pos ~len:(n - length_common) b in - _Eq (_Concat a) (_Concat b) - | (Sized _ | Extract _ | Concat _), (Sized _ | Extract _ | Concat _) - -> - sort_eq x y - (* x = α ==> ⟨x,|α|⟩ = α *) - | x, ((Sized _ | Extract _ | Concat _) as a) - |((Sized _ | Extract _ | Concat _) as a), x -> - _Eq (_Sized x (seq_size_exn a)) a - | _ -> sort_eq x y - - let vars p = Iter.flat_map ~f:Trm.vars (trms p) -end - -module Fmls = Prop.Fmls open Fml +type var = Var.t + (* * Conditional terms *) @@ -498,6 +34,10 @@ type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp] (** pp *) +let pp_boxed fs fmt = + Format.pp_open_box fs 2 ; + Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt + let ppx_f strength fs fml = let pp_t = Trm.ppx strength in let rec pp fs fml = @@ -529,7 +69,7 @@ let ppx_f strength fs fml = | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y | Cond {cnd; pos; neg} -> pf "@[(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg - | Lit (p, xs) -> pf "%a(%a)" Predsym.pp p (Array.pp ",@ " pp_t) xs + | Lit (p, xs) -> pf "%a(%a)" Ses.Predsym.pp p (Array.pp ",@ " pp_t) xs in pp fs fml diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index b927123b6..3ac8dee92 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -5,11 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -open Ses - -(** Variables *) -module Var : Var_intf.VAR - (** Terms *) module rec Term : sig type t [@@deriving compare, equal, sexp] @@ -51,7 +46,7 @@ module rec Term : sig val ancestor : int -> t (* uninterpreted *) - val apply : Funsym.t -> t array -> t + val apply : Ses.Funsym.t -> t array -> t (* if-then-else *) val ite : cnd:Formula.t -> thn:t -> els:t -> t @@ -116,7 +111,7 @@ and Formula : sig val le : Term.t -> Term.t -> t (* uninterpreted *) - val lit : Predsym.t -> Term.t array -> t + val lit : Ses.Predsym.t -> Term.t array -> t (* connectives *) val not_ : t -> t diff --git a/sledge/src/propositional.ml b/sledge/src/propositional.ml index b712582f2..08c8f0d54 100644 --- a/sledge/src/propositional.ml +++ b/sledge/src/propositional.ml @@ -8,7 +8,6 @@ (** Propositional formulas *) include Propositional_intf -open Ses module Make (Trm : TERM) = struct open Trm @@ -38,7 +37,7 @@ module Make (Trm : TERM) = struct | Or of {pos: Fmls.t; neg: Fmls.t} | Iff of fml * fml | Cond of {cnd: fml; pos: fml; neg: fml} - | Lit of Predsym.t * trm array + | Lit of Ses.Predsym.t * trm array [@@deriving compare, equal, sexp] let invariant f = diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli index ae6ae86ca..3a84142aa 100644 --- a/sledge/src/solver.mli +++ b/sledge/src/solver.mli @@ -7,8 +7,6 @@ (** Frame Inference Solver over Symbolic Heaps *) -open Fol - val infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option (** If [infer_frame p xs q] is [Some r], then [p ⊢ ∃xs. q * r]. The vocabulary of [r] is the vocabulary of [q] union [xs]. A goal is for [r] diff --git a/sledge/src/trm.ml b/sledge/src/trm.ml new file mode 100644 index 000000000..0cfad1fd3 --- /dev/null +++ b/sledge/src/trm.ml @@ -0,0 +1,392 @@ +(* + * 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 *) + +module Funsym = Ses.Funsym + +let pp_boxed fs fmt = + Format.pp_open_box fs 2 ; + Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt + +(** Variable terms, represented as a subtype of general terms *) +module rec Var : sig + include Ses.Var_intf.VAR with type t = private Trm.trm + + val of_ : Trm.trm -> t +end = struct + module T = struct + type t = Trm.trm [@@deriving compare, equal, sexp] + + let invariant x = + let@ () = Invariant.invariant [%here] x [%sexp_of: t] in + match x with + | Var _ -> () + | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) () + + let make ~id ~name = Trm._Var id name |> check invariant + let id = function Trm.Var v -> v.id | x -> violates invariant x + let name = function Trm.Var v -> v.name | x -> violates invariant x + end + + include Ses.Var0.Make (T) + + let of_ v = v |> check T.invariant +end + +and Arith0 : + (Arithmetic.REPRESENTATION + with type var := Var.t + with type trm := Trm.trm) = + Arithmetic.Representation (Trm) + +and Arith : + (Arithmetic.S + with type var := Var.t + with type trm := Trm.trm + with type t = Arith0.t) = struct + include Arith0 + + include Make (struct + let get_arith (e : Trm.trm) = + match e with + | Z z -> Some (Arith.const (Q.of_z z)) + | Q q -> Some (Arith.const q) + | Arith a -> Some a + | _ -> None + end) +end + +(** Terms, built from variables and applications of function symbols from + various theories. Denote functions from structures to values. *) +and Trm : sig + type var = Var.t + + type trm = private + (* variables *) + | Var of {id: int; name: string} + (* arithmetic *) + | Z of Z.t + | Q of Q.t + | Arith of Arith.t + (* sequences (of flexible size) *) + | Splat of trm + | Sized of {seq: trm; siz: trm} + | Extract of {seq: trm; off: trm; len: trm} + | Concat of trm array + (* records (with fixed indices) *) + | Select of {idx: int; rcd: trm} + | Update of {idx: int; rcd: trm; elt: trm} + | Record of trm array + | Ancestor of int + (* uninterpreted *) + | Apply of Funsym.t * trm array + [@@deriving compare, equal, sexp] + + val ppx : Var.t Var.strength -> trm pp + val _Var : int -> string -> trm + val _Z : Z.t -> trm + val _Q : Q.t -> trm + val _Arith : Arith.t -> trm + val _Splat : trm -> trm + val _Sized : trm -> trm -> trm + val _Extract : trm -> trm -> trm -> trm + val _Concat : trm array -> trm + val _Select : int -> trm -> trm + val _Update : int -> trm -> trm -> trm + val _Record : trm array -> trm + val _Ancestor : int -> trm + val _Apply : Funsym.t -> trm array -> trm + val add : trm -> trm -> trm + val sub : trm -> trm -> trm + val seq_size_exn : trm -> trm + val seq_size : trm -> trm option +end = struct + type var = Var.t + + type trm = + | Var of {id: int; name: string} + | Z of Z.t + | Q of Q.t + | Arith of Arith.t + | Splat of trm + | Sized of {seq: trm; siz: trm} + | Extract of {seq: trm; off: trm; len: trm} + | Concat of trm array + | Select of {idx: int; rcd: trm} + | Update of {idx: int; rcd: trm; elt: trm} + | Record of trm array + | Ancestor of int + | Apply of Funsym.t * trm array + [@@deriving compare, equal, sexp] + + let compare_trm x y = + if x == y then 0 + else + match (x, y) with + | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> + Int.compare i j + | _ -> compare_trm x y + + let equal_trm x y = + x == y + || + match (x, y) with + | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 -> + Int.equal i j + | _ -> equal_trm x y + + let rec ppx strength fs trm = + let rec pp fs trm = + let pf fmt = pp_boxed fs fmt in + match trm with + | Var _ as v -> Var.ppx strength fs (Var.of_ v) + | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z + | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q + | Arith a -> Arith.ppx strength fs a + | Splat x -> pf "%a^" pp x + | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq + | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len + | Concat [||] -> pf "@<2>⟨⟩" + | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs + | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx + | Update {idx; rcd; elt} -> + pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt + | Record xs -> pf "{%a}" (ppx_record strength) xs + | Ancestor i -> pf "(ancestor %i)" i + | Apply (f, [||]) -> pf "%a" Funsym.pp f + | Apply + ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr) + as f ) + , [|x; y|] ) -> + pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y + | Apply (f, es) -> + pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx strength)) es + in + pp fs trm + + and ppx_record strength fs elts = + [%Trace.fprintf + fs "%a" + (fun fs elts -> + let exception Not_a_string in + match + String.init (Array.length elts) ~f:(fun i -> + match elts.(i) with + | Z c -> Char.of_int_exn (Z.to_int c) + | _ -> raise Not_a_string ) + with + | s -> Format.fprintf fs "%S" s + | exception (Not_a_string | Z.Overflow | Failure _) -> + Format.fprintf fs "@[%a@]" + (Array.pp ",@ " (ppx strength)) + elts ) + elts] + + let pp = ppx (fun _ -> None) + + let invariant e = + let@ () = Invariant.invariant [%here] e [%sexp_of: trm] in + match e with + | Q q -> assert (not (Z.equal Z.one (Q.den q))) + | Arith a -> ( + match Arith.classify a with + | Compound -> () + | Trm _ | Const _ -> assert false ) + | _ -> () + + (* destructors *) + + let get_z = function Z z -> Some z | _ -> None + let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None + + (* constructors *) + + let _Var id name = Var {id; name} |> check invariant + + (* statically allocated since they are tested with == *) + let zero = Z Z.zero |> check invariant + let one = Z Z.one |> check invariant + + let _Z z = + (if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z) + |> check invariant + + let _Q q = + (if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q) + |> check invariant + + let _Arith a = + ( match Arith.classify a with + | Trm e -> e + | Const q -> _Q q + | Compound -> Arith a ) + |> check invariant + + let add x y = _Arith Arith.(add (trm x) (trm y)) + let sub x y = _Arith Arith.(sub (trm x) (trm y)) + let _Splat x = Splat x |> check invariant + + let seq_size_exn = + let invalid = Invalid_argument "seq_size_exn" in + let rec seq_size_exn = function + | Sized {siz= n} | Extract {len= n} -> n + | Concat a0U -> + Array.fold ~f:(fun aJ a0I -> add a0I (seq_size_exn aJ)) a0U zero + | _ -> raise invalid + in + seq_size_exn + + let seq_size e = + try Some (seq_size_exn e) with Invalid_argument _ -> None + + let _Sized seq siz = + ( match seq_size seq with + (* ⟨n,α⟩ ==> α when n ≡ |α| *) + | Some n when equal_trm siz n -> seq + | _ -> Sized {seq; siz} ) + |> check invariant + + let partial_compare x y = + match sub x y with + | Z z -> Some (Int.sign (Z.sign z)) + | Q q -> Some (Int.sign (Q.sign q)) + | _ -> None + + let partial_ge x y = + match partial_compare x y with Some (Pos | Zero) -> true | _ -> false + + let empty_seq = Concat [||] + + let rec _Extract seq off len = + [%trace] + ~call:(fun {pf} -> pf "%a" pp (Extract {seq; off; len})) + ~retn:(fun {pf} -> pf "%a" pp) + @@ fun () -> + (* _[_,0) ==> ⟨⟩ *) + ( if equal_trm len zero then empty_seq + else + let o_l = add off len in + match seq with + (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *) + | Extract {seq= a; off= m; len= k} when partial_ge k o_l -> + _Extract a (add m off) len + (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *) + | Sized {siz= n; seq= Splat _ as e} when partial_ge n o_l -> + _Sized e len + (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *) + | Sized {siz= n} when equal_trm off zero && equal_trm n len -> seq + (* For (α₀^α₁)[o,l) there are 3 cases: + * + * ⟨...⟩^⟨...⟩ + * [,) + * o < o+l ≤ |α₀| : (α₀^α₁)[o,l) ==> α₀[o,l) ^ α₁[0,0) + * + * ⟨...⟩^⟨...⟩ + * [ , ) + * o ≤ |α₀| < o+l : (α₀^α₁)[o,l) ==> α₀[o,|α₀|-o) ^ α₁[0,l-(|α₀|-o)) + * + * ⟨...⟩^⟨...⟩ + * [,) + * |α₀| ≤ o : (α₀^α₁)[o,l) ==> α₀[o,0) ^ α₁[o-|α₀|,l) + * + * So in general: + * + * (α₀^α₁)[o,l) ==> α₀[o,l₀) ^ α₁[o₁,l-l₀) + * where l₀ = max 0 (min l |α₀|-o) + * o₁ = max 0 o-|α₀| + *) + | Concat na1N -> ( + match len with + | Z l -> + Array.fold_map_until na1N (l, off) + ~f:(fun naI (l, oI) -> + if Z.equal Z.zero l then + `Continue (_Extract naI oI zero, (l, oI)) + else + let nI = seq_size_exn naI in + let oI_nI = sub oI nI in + match oI_nI with + | Z z -> + let oJ = if Z.sign z <= 0 then zero else oI_nI in + let lI = Z.(max zero (min l (neg z))) in + let l = Z.(l - lI) in + `Continue (_Extract naI oI (_Z lI), (l, oJ)) + | _ -> `Stop (Extract {seq; off; len}) ) + ~finish:(fun (e1N, _) -> _Concat e1N) + | _ -> Extract {seq; off; len} ) + (* α[o,l) *) + | _ -> Extract {seq; off; len} ) + |> check invariant + + and _Concat xs = + [%trace] + ~call:(fun {pf} -> pf "%a" pp (Concat xs)) + ~retn:(fun {pf} -> pf "%a" pp) + @@ fun () -> + (* (α^(β^γ)^δ) ==> (α^β^γ^δ) *) + let flatten xs = + if Array.exists ~f:(function Concat _ -> true | _ -> false) xs then + Array.flat_map ~f:(function Concat s -> s | e -> [|e|]) xs + else xs + in + let simp_adjacent e f = + match (e, f) with + (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *) + | ( Extract {seq= Sized {siz= n} as na; off= o; len= k} + , Extract {seq= na'; off= o_k; len= l} ) + when equal_trm na na' + && equal_trm o_k (add o k) + && partial_ge n (add o_k l) -> + Some (_Extract na o (add k l)) + (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *) + | Sized {siz= m; seq= Splat _ as a}, Sized {siz= n; seq= a'} + when equal_trm a a' -> + Some (_Sized a (add m n)) + | _ -> None + in + let xs = flatten xs in + let xs = Array.reduce_adjacent ~f:simp_adjacent xs in + (if Array.length xs = 1 then xs.(0) else Concat xs) |> check invariant + + let _Select idx rcd = Select {idx; rcd} |> check invariant + let _Update idx rcd elt = Update {idx; rcd; elt} |> check invariant + let _Record es = Record es |> check invariant + let _Ancestor i = Ancestor i |> check invariant + + let _Apply f es = + ( match + Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es + with + | Some c -> c + | None -> Apply (f, es) ) + |> check invariant +end + +type arith = Arith.t + +include Trm + +let zero = _Z Z.zero +let one = _Z Z.one + +let rec iter_vars e ~f = + match e with + | Var _ as v -> f (Var.of_ v) + | Z _ | Q _ | Ancestor _ -> () + | Splat x | Select {rcd= x} -> iter_vars ~f x + | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} -> + iter_vars ~f x ; + iter_vars ~f y + | Extract {seq= x; off= y; len= z} -> + iter_vars ~f x ; + iter_vars ~f y ; + iter_vars ~f z + | Concat xs | Record xs | Apply (_, xs) -> Array.iter ~f:(iter_vars ~f) xs + | Arith a -> Iter.iter ~f:(iter_vars ~f) (Arith.iter a) + +let vars e = Iter.from_labelled_iter (iter_vars e) diff --git a/sledge/src/trm.mli b/sledge/src/trm.mli new file mode 100644 index 000000000..b5f11c838 --- /dev/null +++ b/sledge/src/trm.mli @@ -0,0 +1,65 @@ +(* + * 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 *) + +type arith + +type trm = private + (* variables *) + | Var of {id: int; name: string} + (* arithmetic *) + | Z of Z.t + | Q of Q.t + | Arith of arith + (* sequences (of flexible size) *) + | Splat of trm + | Sized of {seq: trm; siz: trm} + | Extract of {seq: trm; off: trm; len: trm} + | Concat of trm array + (* records (with fixed indices) *) + | Select of {idx: int; rcd: trm} + | Update of {idx: int; rcd: trm; elt: trm} + | Record of trm array + | Ancestor of int + (* uninterpreted *) + | Apply of Ses.Funsym.t * trm array +[@@deriving compare, equal, sexp] + +module Var : sig + include Ses.Var_intf.VAR with type t = private trm + + val of_ : trm -> t +end + +module Arith : + Arithmetic.S + with type var := Var.t + with type trm := trm + with type t = arith + +val ppx : Var.t Var.strength -> trm pp +val _Var : int -> string -> trm +val _Z : Z.t -> trm +val _Q : Q.t -> trm +val _Arith : Arith.t -> trm +val _Splat : trm -> trm +val _Sized : trm -> trm -> trm +val _Extract : trm -> trm -> trm -> trm +val _Concat : trm array -> trm +val _Select : int -> trm -> trm +val _Update : int -> trm -> trm -> trm +val _Record : trm array -> trm +val _Ancestor : int -> trm +val _Apply : Ses.Funsym.t -> trm array -> trm +val add : trm -> trm -> trm +val sub : trm -> trm -> trm +val seq_size_exn : trm -> trm +val seq_size : trm -> trm option +val vars : trm -> Var.t iter +val zero : trm +val one : trm diff --git a/sledge/src/var.ml b/sledge/src/var.ml new file mode 100644 index 000000000..ba2c62c94 --- /dev/null +++ b/sledge/src/var.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 Trm.Var diff --git a/sledge/src/var.mli b/sledge/src/var.mli new file mode 100644 index 000000000..155099a0b --- /dev/null +++ b/sledge/src/var.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 Trm.Var