Summary: Pausing the experiment in favour of new PulseFormula. Can be resurrected later. Reviewed By: skcho Differential Revision: D22576274 fbshipit-source-id: 76529d767master
Jules Villard
4 years ago
committed by
Facebook GitHub Bot
parent
5a39c158c5
commit
f1e9e28f73
@ -1,13 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
module Pudge = ( val if Config.pudge then (module PulseSledge) else (module PulseDummySledge)
|
||||
: Pudge_intf.S )
|
||||
|
||||
include Pudge
|
||||
@ -1,10 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
include Pudge_intf.S
|
||||
@ -1,73 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module F = Format
|
||||
module AbstractValue = PulseAbstractValue
|
||||
|
||||
module type S = sig
|
||||
type t
|
||||
|
||||
val pp : F.formatter -> t -> unit
|
||||
|
||||
val true_ : t
|
||||
|
||||
module Var : sig
|
||||
type t
|
||||
|
||||
val of_absval : AbstractValue.t -> t
|
||||
|
||||
val to_absval : t -> AbstractValue.t
|
||||
(** use with caution: will crash the program if the given variable wasn't generated from an
|
||||
[AbstractValue.t] using [Var.of_absval] *)
|
||||
end
|
||||
|
||||
module Term : sig
|
||||
type t
|
||||
|
||||
val zero : t
|
||||
|
||||
val of_intlit : IntLit.t -> t
|
||||
|
||||
val of_absval : AbstractValue.t -> t
|
||||
|
||||
val of_unop : Unop.t -> t -> t option
|
||||
|
||||
val of_binop : Binop.t -> t -> t -> t option
|
||||
end
|
||||
|
||||
module Formula : sig
|
||||
type t
|
||||
|
||||
val eq : Term.t -> Term.t -> t
|
||||
|
||||
val lt : Term.t -> Term.t -> t
|
||||
|
||||
val not_ : t -> t
|
||||
|
||||
val term_binop : Binop.t -> Term.t -> Term.t -> t option
|
||||
end
|
||||
|
||||
val and_formula : Formula.t -> t -> t
|
||||
|
||||
val and_ : t -> t -> t
|
||||
|
||||
(** queries *)
|
||||
|
||||
val is_unsat : t -> bool
|
||||
|
||||
val is_known_zero : Term.t -> t -> bool
|
||||
(** [is_known_zero phi t] returns [true] if [phi |- t = 0], [false] if we don't know for sure *)
|
||||
|
||||
(** operations *)
|
||||
|
||||
val fold_map_variables : t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
|
||||
|
||||
val simplify : keep:AbstractValue.Set.t -> t -> t
|
||||
(** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
|
||||
possible *)
|
||||
end
|
||||
@ -1,65 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module F = Format
|
||||
|
||||
module Var = struct
|
||||
type t = unit
|
||||
|
||||
let of_absval _ = ()
|
||||
|
||||
let to_absval () = assert false
|
||||
end
|
||||
|
||||
module Term = struct
|
||||
type t = unit
|
||||
|
||||
let zero = ()
|
||||
|
||||
let of_intlit _ = ()
|
||||
|
||||
let of_absval _ = ()
|
||||
|
||||
let of_unop _ () = None
|
||||
|
||||
let of_binop _ () () = None
|
||||
end
|
||||
|
||||
module Formula = struct
|
||||
type t = unit
|
||||
|
||||
let eq () () = ()
|
||||
|
||||
let lt () () = ()
|
||||
|
||||
let not_ () = ()
|
||||
|
||||
let term_binop _ () () = None
|
||||
end
|
||||
|
||||
(* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
|
||||
type t = {eqs: Ses.Equality.t lazy_t; non_eqs: Ses.Term.t lazy_t}
|
||||
|
||||
(* still print to make sure the formula never changes in debug *)
|
||||
let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
|
||||
F.fprintf fmt "%a∧%a" Ses.Equality.pp eqs Ses.Term.pp non_eqs
|
||||
|
||||
|
||||
let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
|
||||
|
||||
let and_formula () phi = phi
|
||||
|
||||
let and_ phi1 _ = phi1
|
||||
|
||||
let is_known_zero () _ = false
|
||||
|
||||
let is_unsat _ = false
|
||||
|
||||
let fold_map_variables phi ~init ~f:_ = (init, phi)
|
||||
|
||||
let simplify ~keep:_ phi = phi
|
||||
@ -1,10 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
include Pudge_intf.S
|
||||
@ -1,157 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
module L = Logging
|
||||
module AbstractValue = PulseAbstractValue
|
||||
|
||||
[@@@warning "+9"]
|
||||
|
||||
module Var = struct
|
||||
module Var = Sledge.Fol.Var
|
||||
|
||||
let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
|
||||
|
||||
let to_absval v =
|
||||
assert (String.equal (Var.name v) "v") ;
|
||||
Var.id v |> AbstractValue.of_id
|
||||
|
||||
|
||||
include Var
|
||||
end
|
||||
|
||||
module Term = struct
|
||||
module Term = Sledge.Fol.Term
|
||||
|
||||
let of_intlit i = Term.integer (IntLit.to_big_int i)
|
||||
|
||||
let of_absval v = Term.var (Var.of_absval v)
|
||||
|
||||
let of_unop (unop : Unop.t) t = match unop with Neg -> Some (Term.neg t) | BNot | LNot -> None
|
||||
|
||||
let of_binop (binop : Binop.t) t1 t2 =
|
||||
let open Term in
|
||||
match binop with
|
||||
| PlusA _ | PlusPI ->
|
||||
Some (add t1 t2)
|
||||
| MinusA _ | MinusPI | MinusPP ->
|
||||
Some (sub t1 t2)
|
||||
| Mult _ ->
|
||||
Some (mul t1 t2)
|
||||
| Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | LAnd | BOr | LOr | BXor
|
||||
->
|
||||
None
|
||||
|
||||
|
||||
include Term
|
||||
end
|
||||
|
||||
module Formula = struct
|
||||
module Formula = Sledge.Fol.Formula
|
||||
|
||||
let term_binop (binop : Binop.t) t1 t2 =
|
||||
match binop with
|
||||
| BAnd
|
||||
| BOr
|
||||
| BXor
|
||||
| PlusA _
|
||||
| PlusPI
|
||||
| MinusA _
|
||||
| MinusPI
|
||||
| MinusPP
|
||||
| Mult _
|
||||
| Div
|
||||
| Mod
|
||||
| Shiftlt
|
||||
| Shiftrt ->
|
||||
Term.of_binop binop t1 t2 |> Option.map ~f:(fun t -> Formula.dq t Term.zero)
|
||||
| Lt ->
|
||||
Some (Formula.lt t1 t2)
|
||||
| Gt ->
|
||||
Some (Formula.lt t2 t1)
|
||||
| Le ->
|
||||
Some (Formula.le t1 t2)
|
||||
| Ge ->
|
||||
Some (Formula.le t2 t1)
|
||||
| Eq ->
|
||||
Some (Formula.eq t1 t2)
|
||||
| Ne ->
|
||||
Some (Formula.dq t1 t2)
|
||||
| LAnd ->
|
||||
Option.both (Formula.project t1) (Formula.project t2)
|
||||
|> Option.map ~f:(fun (f1, f2) -> Formula.and_ f1 f2)
|
||||
| LOr ->
|
||||
Option.both (Formula.project t1) (Formula.project t2)
|
||||
|> Option.map ~f:(fun (f1, f2) -> Formula.or_ f1 f2)
|
||||
|
||||
|
||||
include Formula
|
||||
end
|
||||
|
||||
module Context = struct
|
||||
include Sledge.Fol.Context
|
||||
|
||||
let assert_no_new_vars api new_vars =
|
||||
if not (Var.Set.is_empty new_vars) then
|
||||
L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
|
||||
|
||||
|
||||
let and_formula phi r =
|
||||
let new_vars, r' = Sledge.Fol.Context.and_formula Var.Set.empty phi r in
|
||||
assert_no_new_vars "Context.and_formula" new_vars ;
|
||||
r'
|
||||
|
||||
|
||||
let and_ r1 r2 =
|
||||
let new_vars, r' = Sledge.Fol.Context.and_ Var.Set.empty r1 r2 in
|
||||
assert_no_new_vars "Context.and_" new_vars ;
|
||||
r'
|
||||
|
||||
|
||||
let apply_subst subst r =
|
||||
let new_vars, r' = Sledge.Fol.Context.apply_subst Var.Set.empty subst r in
|
||||
assert_no_new_vars "Context.apply_subst" new_vars ;
|
||||
r'
|
||||
end
|
||||
|
||||
type t = Context.t lazy_t
|
||||
|
||||
let pp fmt (lazy phi) = Context.pp fmt phi
|
||||
|
||||
let true_ = Lazy.from_val Context.true_
|
||||
|
||||
let and_formula f phi = lazy (Context.and_formula f (Lazy.force phi))
|
||||
|
||||
let and_ phi1 phi2 = lazy (Context.and_ (Lazy.force phi1) (Lazy.force phi2))
|
||||
|
||||
let is_known_zero t phi = Context.entails_eq (Lazy.force phi) t Term.zero
|
||||
|
||||
let is_unsat phi = Context.is_false (Lazy.force phi)
|
||||
|
||||
let fv (lazy phi) = Context.fv phi
|
||||
|
||||
let fold_map_variables phi ~init ~f =
|
||||
let acc, phi' =
|
||||
Context.classes (Lazy.force phi)
|
||||
|> Term.Map.fold ~init:(init, Context.true_) ~f:(fun ~key:t ~data:equal_ts (acc, phi') ->
|
||||
let acc, t' = Term.fold_map_vars ~init:acc ~f t in
|
||||
List.fold equal_ts ~init:(acc, phi') ~f:(fun (acc, phi') equal_t ->
|
||||
let acc, t_mapped = Term.fold_map_vars ~init:acc ~f equal_t in
|
||||
(acc, Context.and_formula (Formula.eq t' t_mapped) phi') ) )
|
||||
in
|
||||
(acc, Lazy.from_val phi')
|
||||
|
||||
|
||||
let simplify ~keep phi =
|
||||
let all_vs = fv phi in
|
||||
let keep_vs =
|
||||
AbstractValue.Set.fold
|
||||
(fun v keep_vs -> Var.Set.add keep_vs (Var.of_absval v))
|
||||
keep Var.Set.empty
|
||||
in
|
||||
let simpl_subst = Context.solve_for_vars [keep_vs; all_vs] (Lazy.force phi) in
|
||||
Lazy.from_val (Context.apply_subst simpl_subst (Lazy.force phi))
|
||||
@ -1,10 +0,0 @@
|
||||
(*
|
||||
* 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.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
include Pudge_intf.S
|
||||
@ -1,5 +0,0 @@
|
||||
; 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.
|
||||
(vendored_dirs *)
|
||||
@ -1 +0,0 @@
|
||||
../../../sledge
|
||||
Loading…
Reference in new issue