From 3d1fbf3840028f306b901cdb58ca23f69e312c1c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:43:38 -0700 Subject: [PATCH] [sledge] Refactor: Expand sig of Fol submodules Reviewed By: ngorogiannis Differential Revision: D22170515 fbshipit-source-id: 3bfe11125 --- sledge/src/fol.ml | 2 +- sledge/src/fol.mli | 395 ++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 393 insertions(+), 4 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 87d2e9fb3..837f35e00 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -5,6 +5,6 @@ * LICENSE file in the root directory of this source tree. *) -module Var = Ses.Var +module Var = Ses.Term.Var module Term = Ses.Term module Context = Ses.Equality diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index 87d2e9fb3..0beeb201a 100644 --- a/sledge/src/fol.mli +++ b/sledge/src/fol.mli @@ -5,6 +5,395 @@ * LICENSE file in the root directory of this source tree. *) -module Var = Ses.Var -module Term = Ses.Term -module Context = Ses.Equality +(** Terms *) +module Term : sig + type op1 = + | Signed of {bits: int} + (** [Ap1 (Signed {bits= n}, arg)] is [arg] interpreted as an [n]-bit + signed integer. That is, it two's-complement--decodes the low + [n] bits of the infinite two's-complement encoding of [arg]. *) + | Unsigned of {bits: int} + (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an + [n]-bit unsigned integer. That is, it unsigned-binary--decodes + the low [n] bits of the infinite two's-complement encoding of + [arg]. *) + | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t} + (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type + [src] to type [dst], possibly with loss of information. The + [src] and [dst] types must be [Typ.convertible] and must not + both be [Integer] types. *) + | Splat (** Iterated concatenation of a single byte *) + | Select of int (** Select an index from a record *) + [@@deriving compare, equal, hash, sexp] + + type op2 = + | Eq (** Equal test *) + | Dq (** Disequal test *) + | Lt (** Less-than test *) + | Le (** Less-than-or-equal test *) + | Ord (** Ordered test (neither arg is nan) *) + | Uno (** Unordered test (some arg is nan) *) + | Div (** Division, for integers result is truncated toward zero *) + | Rem + (** Remainder of division, satisfies [a = b * div a b + rem a b] and + for integers [rem a b] has same sign as [a], and + [|rem a b| < |b|] *) + | Xor (** Exclusive-or, bitwise *) + | Shl (** Shift left, bitwise *) + | Lshr (** Logical shift right, bitwise *) + | Ashr (** Arithmetic shift right, bitwise *) + | Sized (** Size-tagged sequence *) + | Update of int (** Constant record with updated index *) + [@@deriving compare, equal, hash, sexp] + + type op3 = + | Conditional (** If-then-else *) + | Extract (** Extract a slice of an sequence value *) + [@@deriving compare, equal, hash, sexp] + + type opN = + | Concat (** Byte-array concatenation *) + | Record (** Record (array / struct) constant *) + [@@deriving compare, equal, hash, sexp] + + module rec Set : sig + include NS.Set.S with type elt := T.t + + val hash_fold_t : t Hash.folder + val t_of_sexp : Sexp.t -> t + end + + and Qset : sig + include NS.Qset.S with type elt := T.t + + val hash_fold_t : t Hash.folder + val t_of_sexp : Sexp.t -> t + end + + and T : sig + type set = Set.t [@@deriving compare, equal, hash, sexp] + + type qset = Qset.t [@@deriving compare, equal, hash, sexp] + + and t = private + | Var of {id: int; name: string} + (** Local variable / virtual register *) + | Ap1 of op1 * t (** Unary application *) + | Ap2 of op2 * t * t (** Binary application *) + | Ap3 of op3 * t * t * t (** Ternary application *) + | ApN of opN * t iarray (** N-ary application *) + | And of set (** Conjunction, boolean or bitwise *) + | Or of set (** Disjunction, boolean or bitwise *) + | Add of qset (** Sum of terms with rational coefficients *) + | Mul of qset (** Product of terms with rational exponents *) + | Label of {parent: string; name: string} + (** Address of named code block within parent function *) + | Float of {data: string} (** Floating-point constant *) + | Integer of {data: Z.t} (** Integer constant *) + | Rational of {data: Q.t} (** Rational constant *) + | RecRecord of int (** Reference to ancestor recursive record *) + [@@deriving compare, equal, hash, sexp] + end + + include module type of T with type t = T.t + + module Var : sig + type term := t + type t = private term [@@deriving compare, equal, hash, sexp] + type strength = t -> [`Universal | `Existential | `Anonymous] option + + module Map : Map.S with type key := t + + module Set : sig + include NS.Set.S with type elt := t + + val hash_fold_t : t Hash.folder + val sexp_of_t : t -> Sexp.t + val t_of_sexp : Sexp.t -> t + val ppx : strength -> t pp + val pp : t pp + val pp_xs : t pp + val of_regs : Llair.Reg.Set.t -> t + end + + val pp : t pp + + include Invariant.S with type t := t + + val name : t -> string + val id : t -> int + val of_ : term -> t + val of_term : term -> t option + val of_reg : Llair.Reg.t -> t + val fresh : string -> wrt:Set.t -> t * Set.t + + val identified : name:string -> id:int -> t + (** Variable with the given [id]. Variables are compared by [id] alone, + [name] is used only for printing. The only way to ensure + [identified] variables do not clash with [fresh] variables is to + pass the [identified] variables to [fresh] in [wrt]: + [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *) + + module Subst : sig + type var := t + type t [@@deriving compare, equal, sexp] + type x = {sub: t; dom: Set.t; rng: Set.t} + + val pp : t pp + val empty : t + val freshen : Set.t -> wrt:Set.t -> x * Set.t + val invert : t -> t + val restrict : t -> Set.t -> x + val is_empty : t -> bool + val domain : t -> Set.t + val range : t -> Set.t + val apply : t -> var -> var + val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a + end + end + + module Map : sig + include Map.S with type key := t + + val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t + end + + val ppx : Var.strength -> t pp + val pp : t pp + val pp_diff : (t * t) pp + val invariant : t -> unit + + (** Construct *) + + (* variables *) + val var : Var.t -> t + + (* constants *) + val label : parent:string -> name:string -> t + val bool : bool -> t + val true_ : t + val false_ : t + val integer : Z.t -> t + val zero : t + val one : t + val minus_one : t + val rational : Q.t -> t + val float : string -> t + + (* type conversions *) + val signed : int -> t -> t + val unsigned : int -> t -> t + val convert : Llair.Typ.t -> to_:Llair.Typ.t -> t -> t + + (* comparisons *) + val eq : t -> t -> t + val dq : t -> t -> t + val lt : t -> t -> t + val le : t -> t -> t + val ord : t -> t -> t + val uno : t -> t -> t + + (* arithmetic *) + val neg : t -> t + val add : t -> t -> t + val sub : t -> t -> t + val mulq : Q.t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val rem : t -> t -> t + + (* boolean / bitwise *) + val and_ : t -> t -> t + val or_ : t -> t -> t + val not_ : t -> t + + (* bitwise *) + val xor : t -> t -> t + val shl : t -> t -> t + val lshr : t -> t -> t + val ashr : t -> t -> t + + (* if-then-else *) + val conditional : cnd:t -> thn:t -> els:t -> t + + (* sequence sizes *) + val seq_size_exn : t -> t + val seq_size : t -> t option + + (* sequences *) + val splat : t -> t + val sized : seq:t -> siz:t -> t + val extract : seq:t -> off:t -> len:t -> t + val concat : t array -> t + + (* records (struct / array values) *) + val record : t iarray -> t + val select : rcd:t -> idx:int -> t + val update : rcd:t -> idx:int -> elt:t -> t + val rec_record : int -> t + + (* convert *) + val of_exp : Llair.Exp.t -> t + + (** Destruct *) + + val d_int : t -> Z.t option + + (** Access *) + + val const_of : t -> Q.t option + + (** Transform *) + + val map : t -> f:(t -> t) -> t + + val map_rec_pre : t -> f:(t -> t option) -> t + (** Pre-order transformation. Each subterm [x] from root to leaves is + presented to [f]. If [f x = Some x'] then the subterms of [x] are not + traversed and [x] is transformed to [x']. Otherwise traversal proceeds + to the subterms of [x], followed by rebuilding the term structure on + the transformed subterms. *) + + val fold_map : t -> init:'a -> f:('a -> t -> 'a * t) -> 'a * t + + val fold_map_rec_pre : + t -> init:'a -> f:('a -> t -> ('a * t) option) -> 'a * t + + val disjuncts : t -> t list + val rename : Var.Subst.t -> t -> t + + (** Traverse *) + + val iter : t -> f:(t -> unit) -> unit + val exists : t -> f:(t -> bool) -> bool + val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a + val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a + val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a + + (** Query *) + + val fv : t -> Var.Set.t + val is_true : t -> bool + val is_false : t -> bool + + val is_constant : t -> bool + (** Test if a term's semantics is independent of the values of variables. *) + + val height : t -> int + + (** Solve *) + + val solve_zero_eq : ?for_:t -> t -> (t * t) option + (** [solve_zero_eq d] is [Some (e, f)] if [d = 0] can be equivalently + expressed as [e = f] for some monomial subterm [e] of [d]. If [for_] + is passed, then the subterm [e] must be [for_]. *) +end + +module Var = Term.Var + +(** Inference System *) +module Context : sig + type t [@@deriving compare, equal, sexp] + type classes = Term.t list Term.Map.t + + val classes : t -> classes + (** [classes r] maps each equivalence class representative to the other + terms [r] proves equal to it. *) + + val diff_classes : t -> t -> classes + (** [diff_classes r s] is the equality classes of [r] omitting equalities + in [s]. *) + + val pp : t pp + val pp_classes : t pp + val ppx_classes : Var.strength -> classes pp + + include Invariant.S with type t := t + + val true_ : t + (** The diagonal relation, which only equates each term with itself. *) + + val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> Var.Set.t * t + (** Conjoin an equation to a relation. *) + + val and_term : Var.Set.t -> Term.t -> t -> Var.Set.t * t + (** Conjoin a (Boolean) term to a relation. *) + + val and_ : Var.Set.t -> t -> t -> Var.Set.t * t + (** Conjunction. *) + + val or_ : Var.Set.t -> t -> t -> Var.Set.t * t + (** Disjunction. *) + + val orN : Var.Set.t -> t list -> Var.Set.t * t + (** Nary disjunction. *) + + 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 terms of the relation. *) + + val is_true : t -> bool + (** Test if the relation is diagonal. *) + + val is_false : t -> bool + (** Test if the relation is empty / inconsistent. *) + + val entails_eq : t -> Term.t -> Term.t -> bool + (** Test if an equation is entailed by a 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 -> 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 -> 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_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a + + (** Solution Substitutions *) + module Subst : sig + type t [@@deriving compare, equal, sexp] + + val pp : t pp + val is_empty : t -> bool + + val fold : + t -> init:'a -> f:(key:Term.t -> data:Term.t -> 'a -> 'a) -> 'a + + val subst : t -> Term.t -> Term.t + (** Apply a substitution recursively to subterms. *) + + val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t + (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks + and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks + and ks ∩ fv(τ) = ∅. *) + end + + val apply_subst : Var.Set.t -> Subst.t -> t -> Var.Set.t * t + (** Relation induced by applying a substitution to a set of equations + generating the argument relation. *) + + val solve_for_vars : Var.Set.t list -> t -> Subst.t + (** [solve_for_vars vss r] is a solution substitution that is entailed by + [r] and consists of oriented equalities [x ↦ e] that map terms [x] + with free variables contained in (the union of) a prefix [uss] of + [vss] to terms [e] with free variables contained in as short a prefix + of [uss] as possible. *) + + val elim : Var.Set.t -> t -> t + (** Weaken relation by removing oriented equations [k ↦ _] for [k] in + [ks]. *) + + (* Replay debugging *) + + val replay : string -> unit +end