diff --git a/Gillian-C/lib/gilgen.ml b/Gillian-C/lib/gilgen.ml index 0fd2c4cd..1f053e66 100644 --- a/Gillian-C/lib/gilgen.ml +++ b/Gillian-C/lib/gilgen.ml @@ -1061,6 +1061,8 @@ let trans_program imports = []; lemmas = Hashtbl.create 1; preds = Hashtbl.create 1; + funcs = Hashtbl.create 1; + datatypes = Hashtbl.create 1; only_specs = Hashtbl.create 1; macros = Hashtbl.create 1; bi_specs = make_hashtbl (fun p -> p.BiSpec.bispec_name) bi_specs; diff --git a/Gillian-JS/lib/Compiler/JSIL2GIL.ml b/Gillian-JS/lib/Compiler/JSIL2GIL.ml index 6e06a4b7..9bbb3b28 100644 --- a/Gillian-JS/lib/Compiler/JSIL2GIL.ml +++ b/Gillian-JS/lib/Compiler/JSIL2GIL.ml @@ -502,6 +502,9 @@ let jsil2core_prog (prog : EProg.t) : ('a, string) GProg.t = ~procs:new_procs ~macros:(translate_tbl prog.macros jsil2gil_macro) ~bi_specs:(translate_tbl prog.bi_specs jsil2gil_bispec) - ~proc_names:prog.proc_names ~predecessors:(Hashtbl.create 1) () + ~proc_names:prog.proc_names ~predecessors:(Hashtbl.create 1) + ~datatypes:(Hashtbl.create 1) + ~funcs:(Hashtbl.create 1) (* TODO *) + () in result diff --git a/GillianCore/GIL_Syntax/Constructor.ml b/GillianCore/GIL_Syntax/Constructor.ml new file mode 100644 index 00000000..3f34ab7f --- /dev/null +++ b/GillianCore/GIL_Syntax/Constructor.ml @@ -0,0 +1,9 @@ +type t = TypeDef__.constructor = { + constructor_name : string; + constructor_source_path : string option; + constructor_loc : Location.t option; + constructor_num_fields : int; + constructor_fields : Type.t option list; + constructor_datatype : string; +} +[@@deriving yojson] diff --git a/GillianCore/GIL_Syntax/Datatype.ml b/GillianCore/GIL_Syntax/Datatype.ml new file mode 100644 index 00000000..09e9b05e --- /dev/null +++ b/GillianCore/GIL_Syntax/Datatype.ml @@ -0,0 +1,7 @@ +type t = TypeDef__.datatype = { + datatype_name : string; + datatype_source_path : string option; + datatype_loc : Location.t option; + datatype_constructors : Constructor.t list; +} +[@@deriving yojson] diff --git a/GillianCore/GIL_Syntax/Expr.ml b/GillianCore/GIL_Syntax/Expr.ml index 650e2b70..78ff7b78 100644 --- a/GillianCore/GIL_Syntax/Expr.ml +++ b/GillianCore/GIL_Syntax/Expr.ml @@ -16,6 +16,9 @@ type t = TypeDef__.expr = (** Existential quantification. *) | ForAll of (string * Type.t option) list * t (** Universal quantification. *) + | ConstructorApp of string * t list (** Datatype constructor *) + | FuncApp of string * t list (** Function application *) + | Cases of t * (string * string list * t) list [@@deriving eq, ord] let to_yojson = TypeDef__.expr_to_yojson @@ -377,6 +380,18 @@ let rec map_opt match map_e e with | Some e' -> Some (ForAll (bt, e')) | _ -> None) + | ConstructorApp (n, les) -> + aux les (fun les -> ConstructorApp (n, les)) + | FuncApp (n, les) -> aux les (fun les -> FuncApp (n, les)) + | Cases (e, cs) -> + let cs = + List_utils.flaky_map + (fun (c, bs, e) -> + let e = map_e e in + Option.map (fun e -> (c, bs, e)) e) + cs + in + Option.map (fun cs -> Cases (e, cs)) cs in Option.map f_after mapped_expr @@ -414,6 +429,25 @@ let rec pp fmt e = Fmt.pf fmt "(forall %a . %a)" (Fmt.list ~sep:Fmt.comma pp_var_with_type) bt pp e + | ConstructorApp (n, ll) -> + Fmt.pf fmt "'%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll + | FuncApp (n, ll) -> Fmt.pf fmt "%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll + | Cases (scrutinee, branches) -> + Fmt.pf fmt "@[case %a {@," pp scrutinee; + List.iteri + (fun i (constructor, binders, expr) -> + Fmt.pf fmt " %s" constructor; + (match binders with + | [] -> () + | _ -> + Fmt.pf fmt "("; + Fmt.pf fmt "%a" (Fmt.list ~sep:(Fmt.any ", ") Fmt.string) binders; + Fmt.pf fmt ")"); + Fmt.pf fmt " -> %a" pp expr; + if i < List.length branches - 1 then Fmt.pf fmt ";@," + else Fmt.pf fmt "@,") + branches; + Fmt.pf fmt "}@]" let rec full_pp fmt e = match e with @@ -476,6 +510,7 @@ let rec is_concrete (le : t) : bool = | BinOp (e1, _, e2) -> loop [ e1; e2 ] | LstSub (e1, e2, e3) -> loop [ e1; e2; e3 ] | NOp (_, les) | EList les | ESet les -> loop les + | ConstructorApp (_, _) | FuncApp _ | Cases _ -> false let is_concrete_zero_i : t -> bool = function | Lit (Int z) -> Z.equal Z.zero z diff --git a/GillianCore/GIL_Syntax/Func.ml b/GillianCore/GIL_Syntax/Func.ml new file mode 100644 index 00000000..70db2b3e --- /dev/null +++ b/GillianCore/GIL_Syntax/Func.ml @@ -0,0 +1,8 @@ +type t = TypeDef__.func = { + func_name : string; + func_source_path : string option; + func_loc : Location.t option; + func_num_params : int; + func_params : (string * Type.t option) list; + func_definition : Expr.t; +} diff --git a/GillianCore/GIL_Syntax/Gil_syntax.ml b/GillianCore/GIL_Syntax/Gil_syntax.ml index ad6d2375..06d8ece8 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.ml +++ b/GillianCore/GIL_Syntax/Gil_syntax.ml @@ -6,7 +6,10 @@ module BiSpec = BiSpec module Branch_case = Branch_case module Cmd = Cmd module Constant = Constant +module Constructor = Constructor +module Datatype = Datatype module Expr = Expr +module Func = Func module Flag = Flag module LCmd = LCmd module Lemma = Lemma diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index e1829a0b..6dbc944f 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.mli +++ b/GillianCore/GIL_Syntax/Gil_syntax.mli @@ -48,7 +48,7 @@ end module Type : sig (** GIL Types *) - type t = + type t = TypeDef__.typ = | UndefinedType (** Type of Undefined *) | NullType (** Type of Null *) | EmptyType (** Type of Empty *) @@ -61,6 +61,7 @@ module Type : sig | ListType (** Type of lists *) | TypeType (** Type of types *) | SetType (** Type of sets *) + | DatatypeType of string [@@deriving yojson, eq, show] (** Printer *) @@ -250,6 +251,9 @@ module Expr : sig | Exists of (string * Type.t option) list * t (** Existential quantification. *) | ForAll of (string * Type.t option) list * t + | ConstructorApp of string * t list + | FuncApp of string * t list + | Cases of t * (string * string list * t) list [@@deriving yojson] (** {2: Helpers for building expressions} @@ -722,6 +726,39 @@ module Lemma : sig val add_param_bindings : t -> t end +module Datatype : sig + type t = TypeDef__.datatype = { + datatype_name : string; + datatype_source_path : string option; + datatype_loc : Location.t option; + datatype_constructors : Constructor.t list; + } + [@@deriving yojson] +end + +module Func : sig + type t = { + func_name : string; + func_source_path : string option; + func_loc : Location.t option; + func_num_params : int; + func_params : (string * Type.t option) list; + func_definition : Expr.t; + } +end + +module Constructor : sig + type t = TypeDef__.constructor = { + constructor_name : string; + constructor_source_path : string option; + constructor_loc : Location.t option; + constructor_num_fields : int; + constructor_fields : Type.t option list; + constructor_datatype : string; + } + [@@deriving yojson] +end + (** @canonical Gillian.Gil_syntax.Macro *) module Macro : sig (** GIL Macros *) @@ -951,6 +988,8 @@ module Prog : sig (** List of imported GIL files, and whether each has to be verified *) lemmas : (string, Lemma.t) Hashtbl.t; (** Lemmas *) preds : (string, Pred.t) Hashtbl.t; (** Predicates *) + funcs : (string, Func.t) Hashtbl.t; (** Predicates *) + datatypes : (string, Datatype.t) Hashtbl.t; only_specs : (string, Spec.t) Hashtbl.t; (** Specs without function definitions *) procs : (string, ('annot, 'label) Proc.t) Hashtbl.t; (** Proceudes *) @@ -966,6 +1005,8 @@ module Prog : sig imports:(string * bool) list -> lemmas:(string, Lemma.t) Hashtbl.t -> preds:(string, Pred.t) Hashtbl.t -> + funcs:(string, Func.t) Hashtbl.t -> + datatypes:(string, Datatype.t) Hashtbl.t -> only_specs:(string, Spec.t) Hashtbl.t -> procs:(string, ('annot, 'label) Proc.t) Hashtbl.t -> macros:(string, Macro.t) Hashtbl.t -> @@ -981,6 +1022,8 @@ module Prog : sig imports:(string * bool) list -> lemmas:(string, Lemma.t) Hashtbl.t -> preds:(string, Pred.t) Hashtbl.t -> + funcs:(string, Func.t) Hashtbl.t -> + datatypes:(string, Datatype.t) Hashtbl.t -> only_specs:(string, Spec.t) Hashtbl.t -> macros:(string, Macro.t) Hashtbl.t -> bi_specs:(string, BiSpec.t) Hashtbl.t -> @@ -994,6 +1037,8 @@ module Prog : sig predecessors:(string * int * int * int) list -> lemmas:(string, Lemma.t) Hashtbl.t -> preds:(string, Pred.t) Hashtbl.t -> + funcs:(string, Func.t) Hashtbl.t -> + datatypes:(string, Datatype.t) Hashtbl.t -> only_specs:(string, Spec.t) Hashtbl.t -> macros:(string, Macro.t) Hashtbl.t -> bi_specs:(string, BiSpec.t) Hashtbl.t -> @@ -1148,8 +1193,16 @@ module Visitors : sig (string * (string * Expr.t) list) option -> 'f Cmd.t ; visit_Car : 'c -> UnOp.t -> UnOp.t + ; visit_Cases : + 'c -> + Expr.t -> + Expr.t -> + (string * string list * Expr.t) list -> + Expr.t ; visit_Cdr : 'c -> UnOp.t -> UnOp.t ; visit_Constant : 'c -> Literal.t -> Constant.t -> Literal.t + ; visit_ConstructorApp : + 'c -> Expr.t -> string -> Expr.t list -> Expr.t ; visit_ECall : 'c -> 'f Cmd.t -> @@ -1175,6 +1228,7 @@ module Visitors : sig ; visit_FMod : 'c -> BinOp.t -> BinOp.t ; visit_ForAll : 'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t + ; visit_FuncApp : 'c -> Expr.t -> string -> Expr.t list -> Expr.t ; visit_FPlus : 'c -> BinOp.t -> BinOp.t ; visit_FTimes : 'c -> BinOp.t -> BinOp.t ; visit_FUnaryMinus : 'c -> UnOp.t -> UnOp.t @@ -1193,6 +1247,7 @@ module Visitors : sig Expr.t list -> Expr.t list -> Asrt.atom + ; visit_DatatypeType : 'c -> Type.t -> string -> Type.t ; visit_Wand : 'c -> Asrt.atom -> @@ -1344,8 +1399,11 @@ module Visitors : sig ; visit_position : 'c -> Location.position -> Location.position ; visit_location : 'c -> Location.t -> Location.t ; visit_constant : 'c -> Constant.t -> Constant.t + ; visit_constructor : 'c -> Constructor.t -> Constructor.t + ; visit_datatype : 'c -> Datatype.t -> Datatype.t ; visit_expr : 'c -> Expr.t -> Expr.t ; visit_flag : 'c -> Flag.t -> Flag.t + ; visit_func : 'c -> Func.t -> Func.t ; visit_lcmd : 'c -> LCmd.t -> LCmd.t ; visit_lemma : 'c -> Lemma.t -> Lemma.t ; visit_lemma_spec : 'c -> Lemma.spec -> Lemma.spec @@ -1405,9 +1463,16 @@ module Visitors : sig 'f Cmd.t method visit_Car : 'c -> UnOp.t -> UnOp.t + + method visit_Cases : + 'c -> Expr.t -> Expr.t -> (string * string list * Expr.t) list -> Expr.t + method visit_Cdr : 'c -> UnOp.t -> UnOp.t method visit_Constant : 'c -> Literal.t -> Constant.t -> Literal.t + method visit_ConstructorApp : + 'c -> Expr.t -> string -> Expr.t list -> Expr.t + method visit_ECall : 'c -> 'f Cmd.t -> string -> Expr.t -> Expr.t list -> 'f option -> 'f Cmd.t @@ -1428,6 +1493,7 @@ module Visitors : sig method visit_FLessThanEqual : 'c -> BinOp.t -> BinOp.t method visit_FMinus : 'c -> BinOp.t -> BinOp.t method visit_FMod : 'c -> BinOp.t -> BinOp.t + method visit_FuncApp : 'c -> Expr.t -> string -> Expr.t list -> Expr.t method visit_FPlus : 'c -> BinOp.t -> BinOp.t method visit_FTimes : 'c -> BinOp.t -> BinOp.t method visit_FUnaryMinus : 'c -> UnOp.t -> UnOp.t @@ -1447,6 +1513,8 @@ module Visitors : sig method visit_CorePred : 'c -> Asrt.atom -> string -> Expr.t list -> Expr.t list -> Asrt.atom + method visit_DatatypeType : 'c -> Type.t -> string -> Type.t + method visit_Wand : 'c -> Asrt.atom -> @@ -1611,8 +1679,11 @@ module Visitors : sig method visit_position : 'c -> Location.position -> Location.position method visit_location : 'c -> Location.t -> Location.t method visit_constant : 'c -> Constant.t -> Constant.t + method visit_constructor : 'c -> Constructor.t -> Constructor.t + method visit_datatype : 'c -> Datatype.t -> Datatype.t method visit_expr : 'c -> Expr.t -> Expr.t method visit_flag : 'c -> Flag.t -> Flag.t + method visit_func : 'c -> Func.t -> Func.t method private visit_float : 'env. 'env -> float -> float method private visit_int : 'env. 'env -> int -> int method private visit_int32 : 'env. 'env -> int32 -> int32 @@ -1697,8 +1768,11 @@ module Visitors : sig (string * (string * Expr.t) list) option -> 'f ; visit_Car : 'c -> 'f + ; visit_Cases : + 'c -> Expr.t -> (string * string list * Expr.t) list -> 'f ; visit_Cdr : 'c -> 'f ; visit_Constant : 'c -> Constant.t -> 'f + ; visit_ConstructorApp : 'c -> string -> Expr.t list -> 'f ; visit_IDiv : 'c -> 'f ; visit_FDiv : 'c -> 'f ; visit_ECall : @@ -1721,6 +1795,7 @@ module Visitors : sig 'f ; visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> 'f ; visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> 'f + ; visit_DatatypeType : 'c -> string -> 'f ; visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> 'f ; visit_GUnfold : 'c -> string -> 'f ; visit_Goto : 'c -> 'g -> 'f @@ -1813,6 +1888,7 @@ module Visitors : sig ; visit_SignedRightShiftF : 'c -> 'f ; visit_Skip : 'c -> 'f ; visit_FreshSVar : 'c -> string -> 'f + ; visit_FuncApp : 'c -> string -> Expr.t list -> 'f ; visit_StrCat : 'c -> 'f ; visit_StrLen : 'c -> 'f ; visit_StrLess : 'c -> 'f @@ -1862,8 +1938,11 @@ module Visitors : sig ; visit_position : 'c -> Location.position -> 'f ; visit_location : 'c -> Location.t -> 'f ; visit_constant : 'c -> Constant.t -> 'f + ; visit_constructor : 'c -> Constructor.t -> 'f + ; visit_datatype : 'c -> Datatype.t -> 'f ; visit_expr : 'c -> Expr.t -> 'f ; visit_flag : 'c -> Flag.t -> 'f + ; visit_func : 'c -> Func.t -> 'f ; visit_lcmd : 'c -> LCmd.t -> 'f ; visit_lemma : 'c -> Lemma.t -> 'f ; visit_lemma_spec : 'c -> Lemma.spec -> 'f @@ -1918,8 +1997,13 @@ module Visitors : sig 'f method visit_Car : 'c -> 'f + + method visit_Cases : + 'c -> Expr.t -> (string * string list * Expr.t) list -> 'f + method visit_Cdr : 'c -> 'f method visit_Constant : 'c -> Constant.t -> 'f + method visit_ConstructorApp : 'c -> string -> Expr.t list -> 'f method visit_IDiv : 'c -> 'f method visit_FDiv : 'c -> 'f @@ -1946,6 +2030,7 @@ module Visitors : sig method visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> 'f method visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> 'f + method visit_DatatypeType : 'c -> string -> 'f method visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> 'f method visit_GUnfold : 'c -> string -> 'f method visit_Goto : 'c -> 'g -> 'f @@ -2038,6 +2123,7 @@ module Visitors : sig method visit_SignedRightShiftF : 'c -> 'f method visit_Skip : 'c -> 'f method visit_FreshSVar : 'c -> string -> 'f + method visit_FuncApp : 'c -> string -> Expr.t list -> 'f method visit_StrCat : 'c -> 'f method visit_StrLen : 'c -> 'f method visit_StrLess : 'c -> 'f @@ -2085,8 +2171,11 @@ module Visitors : sig method visit_position : 'c -> Location.position -> 'f method visit_location : 'c -> Location.t -> 'f method visit_constant : 'c -> Constant.t -> 'f + method visit_constructor : 'c -> Constructor.t -> 'f + method visit_datatype : 'c -> Datatype.t -> 'f method visit_expr : 'c -> Expr.t -> 'f method visit_flag : 'c -> Flag.t -> 'f + method visit_func : 'c -> Func.t -> 'f method visit_lcmd : 'c -> LCmd.t -> 'f method visit_lemma : 'c -> Lemma.t -> 'f method visit_lemma_spec : 'c -> Lemma.spec -> 'f @@ -2141,8 +2230,11 @@ module Visitors : sig Cmd.logic_bindings_t option -> unit ; visit_Car : 'c -> unit + ; visit_Cases : + 'c -> Expr.t -> (string * string list * Expr.t) list -> unit ; visit_Cdr : 'c -> unit ; visit_Constant : 'c -> Constant.t -> unit + ; visit_ConstructorApp : 'c -> string -> Expr.t list -> unit ; visit_ECall : 'c -> string -> Expr.t -> Expr.t list -> 'f option -> unit ; visit_EList : 'c -> Expr.t list -> unit @@ -2171,6 +2263,7 @@ module Visitors : sig unit ; visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> unit ; visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> unit + ; visit_DatatypeType : 'c -> string -> unit ; visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> unit ; visit_GUnfold : 'c -> string -> unit @@ -2262,6 +2355,7 @@ module Visitors : sig ; visit_SignedRightShiftF : 'c -> unit ; visit_Skip : 'c -> unit ; visit_FreshSVar : 'c -> string -> unit + ; visit_FuncApp : 'c -> string -> Expr.t list -> unit ; visit_StrCat : 'c -> unit ; visit_StrLen : 'c -> unit ; visit_StrLess : 'c -> unit @@ -2306,8 +2400,11 @@ module Visitors : sig ; visit_position : 'c -> Location.position -> unit ; visit_location : 'c -> Location.t -> unit ; visit_constant : 'c -> Constant.t -> unit + ; visit_constructor : 'c -> Constructor.t -> unit + ; visit_datatype : 'c -> Datatype.t -> unit ; visit_expr : 'c -> Expr.t -> unit ; visit_flag : 'c -> Flag.t -> unit + ; visit_func : 'c -> Func.t -> unit ; visit_lcmd : 'c -> LCmd.t -> unit ; visit_lemma : 'c -> Lemma.t -> unit ; visit_lemma_spec : 'c -> Lemma.spec -> unit @@ -2361,8 +2458,13 @@ module Visitors : sig unit method visit_Car : 'c -> unit + + method visit_Cases : + 'c -> Expr.t -> (string * string list * Expr.t) list -> unit + method visit_Cdr : 'c -> unit method visit_Constant : 'c -> Constant.t -> unit + method visit_ConstructorApp : 'c -> string -> Expr.t list -> unit method visit_ECall : 'c -> string -> Expr.t -> Expr.t list -> 'f option -> unit @@ -2395,6 +2497,7 @@ module Visitors : sig method visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> unit method visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> unit + method visit_DatatypeType : 'c -> string -> unit method visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> unit @@ -2488,6 +2591,7 @@ module Visitors : sig method visit_SignedRightShiftF : 'c -> unit method visit_Skip : 'c -> unit method visit_FreshSVar : 'c -> string -> unit + method visit_FuncApp : 'c -> string -> Expr.t list -> unit method visit_StrCat : 'c -> unit method visit_StrLen : 'c -> unit method visit_StrLess : 'c -> unit @@ -2542,8 +2646,11 @@ module Visitors : sig method visit_position : 'c -> Location.position -> unit method visit_location : 'c -> Location.t -> unit method visit_constant : 'c -> Constant.t -> unit + method visit_constructor : 'c -> Constructor.t -> unit + method visit_datatype : 'c -> Datatype.t -> unit method visit_expr : 'c -> Expr.t -> unit method visit_flag : 'c -> Flag.t -> unit + method visit_func : 'c -> Func.t -> unit method private visit_float : 'env. 'env -> float -> unit method private visit_int : 'env. 'env -> int -> unit method private visit_int32 : 'env. 'env -> int32 -> unit diff --git a/GillianCore/GIL_Syntax/Prog.ml b/GillianCore/GIL_Syntax/Prog.ml index f0bd3b94..8362c0ae 100644 --- a/GillianCore/GIL_Syntax/Prog.ml +++ b/GillianCore/GIL_Syntax/Prog.ml @@ -7,6 +7,8 @@ type ('annot, 'label) t = { (* Lemmas *) preds : (string, Pred.t) Hashtbl.t; (* Predicates = Name : String --> Definition *) + funcs : (string, Func.t) Hashtbl.t; + datatypes : (string, Datatype.t) Hashtbl.t; only_specs : (string, Spec.t) Hashtbl.t; (* Specs = Name : String --> Spec *) procs : (string, ('annot, 'label) Proc.t) Hashtbl.t; @@ -23,6 +25,8 @@ let make ~imports ~lemmas ~preds + ~funcs + ~datatypes ~only_specs ~procs ~macros @@ -34,6 +38,8 @@ let make imports; lemmas; preds; + funcs; + datatypes; only_specs; procs; macros; @@ -66,6 +72,8 @@ let create () = make_labeled ~imports:[] ~lemmas:(Hashtbl.create medium_tbl_size) ~preds:(Hashtbl.create big_tbl_size) + ~funcs:(Hashtbl.create medium_tbl_size) + ~datatypes:(Hashtbl.create medium_tbl_size) ~only_specs:(Hashtbl.create medium_tbl_size) ~procs:(Hashtbl.create big_tbl_size) ~macros:(Hashtbl.create small_tbl_size) diff --git a/GillianCore/GIL_Syntax/Type.ml b/GillianCore/GIL_Syntax/Type.ml index f2d11fd0..3b1b2a04 100644 --- a/GillianCore/GIL_Syntax/Type.ml +++ b/GillianCore/GIL_Syntax/Type.ml @@ -15,6 +15,7 @@ type t = TypeDef__.typ = | ListType (** Type of lists *) | TypeType (** Type of types *) | SetType (** Type of sets *) + | DatatypeType of string [@@deriving yojson, eq, ord, show] (** Print *) @@ -32,6 +33,7 @@ let str (x : t) = | ListType -> "List" | TypeType -> "Type" | SetType -> "Set" + | DatatypeType s -> s module Set = Set.Make (struct type nonrec t = t diff --git a/GillianCore/GIL_Syntax/TypeDef__.ml b/GillianCore/GIL_Syntax/TypeDef__.ml index 7f45bcfb..fb3a0b03 100644 --- a/GillianCore/GIL_Syntax/TypeDef__.ml +++ b/GillianCore/GIL_Syntax/TypeDef__.ml @@ -29,6 +29,7 @@ and typ = | ListType | TypeType | SetType + | DatatypeType of string and literal = | Undefined @@ -152,6 +153,9 @@ and expr = | ESet of expr list | Exists of (string * typ option) list * expr | ForAll of (string * typ option) list * expr + | ConstructorApp of string * expr list + | FuncApp of string * expr list + | Cases of expr * (string * string list * expr) list and assertion_atom = | Emp @@ -239,6 +243,31 @@ and lemma = { lemma_existentials : string list; } +and datatype = { + datatype_name : string; + datatype_source_path : string option; + datatype_loc : location option; + datatype_constructors : constructor list; +} + +and func = { + func_name : string; + func_source_path : string option; + func_loc : location option; + func_num_params : int; + func_params : (string * typ option) list; + func_definition : expr; +} + +and constructor = { + constructor_name : string; + constructor_source_path : string option; + constructor_loc : location option; + constructor_num_fields : int; + constructor_fields : typ option list; + constructor_datatype : string; +} + and single_spec = { ss_pre : assertion * location option; ss_posts : (assertion * location option) list; diff --git a/GillianCore/engine/Abstraction/MP.ml b/GillianCore/engine/Abstraction/MP.ml index 8d594c43..c7641ffb 100644 --- a/GillianCore/engine/Abstraction/MP.ml +++ b/GillianCore/engine/Abstraction/MP.ml @@ -101,8 +101,7 @@ let minimise_matchables (kb : KB.t) : KB.t = let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list = let f' = missing_expr in let f = missing_expr kb in - let join (le : Expr.t list) = - let mle = List.map f le in + let join' (mle : KB.t list list) = let cpmle = List_utils.list_product mle in let umle = List.map @@ -111,6 +110,10 @@ let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list = in if umle = [] || List.mem KB.empty umle then [ KB.empty ] else umle in + let join (le : Expr.t list) = + let mle = List.map f le in + join' mle + in if KB.mem e kb then [ KB.empty ] else match e with @@ -140,7 +143,8 @@ let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list = (* The remaining cases proceed recursively *) | UnOp (_, e) -> f e | BinOp (e1, _, e2) -> join [ e1; e2 ] - | NOp (_, le) | EList le | ESet le -> join le + | NOp (_, le) | EList le | ESet le | ConstructorApp (_, le) | FuncApp (_, le) + -> join le | LstSub (e1, e2, e3) -> let result = join [ e1; e2; e3 ] in L.verbose (fun fmt -> @@ -148,6 +152,12 @@ let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list = Fmt.(brackets (list ~sep:semi kb_pp)) result); result + | Cases (le, cs) -> + let kb' bs = + KB.add_seq (List.to_seq bs |> Seq.map (fun x -> Expr.LVar x)) kb + in + let mle = f le :: List.map (fun (_, bs, e) -> f' (kb' bs) e) cs in + join' mle | Exists (bt, e) | ForAll (bt, e) -> let kb' = KB.add_seq (List.to_seq bt |> Seq.map (fun (x, _) -> Expr.LVar x)) kb @@ -287,6 +297,29 @@ let rec learn_expr | BinOp _ -> [] (* Can we learn anything from Exists? *) | Exists _ | ForAll _ -> [] + | ConstructorApp (cname, le) -> + let num_fields = List.length le in + let param_str = Printf.sprintf "param-%d" in + let base_expr_nth_field n = + let case = + (cname, List.init num_fields param_str, Expr.LVar (param_str n)) + in + Expr.Cases (base_expr, [ case ]) + in + let le_with_base_exprs = + List.mapi (fun i e -> (e, base_expr_nth_field i)) le + in + L.( + verbose (fun m -> + m "List of expressions: %a" + Fmt.( + brackets + (list ~sep:semi (parens (pair ~sep:comma Expr.pp Expr.pp)))) + le_with_base_exprs)); + learn_expr_list kb le_with_base_exprs + (* Function application isn't invertible *) + | FuncApp _ -> [] + | Cases _ -> [] and learn_expr_list (kb : KB.t) (le : (Expr.t * Expr.t) list) = (* L.(verbose (fun m -> m "Entering learn_expr_list: \nKB: %a\nList: %a" kb_pp kb Fmt.(brackets (list ~sep:semi (parens (pair ~sep:comma Expr.pp Expr.pp)))) le)); *) @@ -440,7 +473,17 @@ let rec simple_ins_formula (kb : KB.t) (pf : Expr.t) : KB.t list = let ins_pf = f pf in let ins = List.map (fun ins -> KB.diff ins binders) ins_pf in List.map minimise_matchables ins - | Lit _ | PVar _ | LVar _ | ALoc _ | LstSub _ | NOp _ | EList _ | ESet _ -> [] + | Lit _ + | PVar _ + | LVar _ + | ALoc _ + | LstSub _ + | NOp _ + | EList _ + | ESet _ + | ConstructorApp _ + | FuncApp _ + | Cases _ -> [] (** [ins_outs_formula kb pf] returns a list of possible ins-outs pairs for a given formula [pf] under a given knowledge base [kb] *) diff --git a/GillianCore/engine/Abstraction/Normaliser.ml b/GillianCore/engine/Abstraction/Normaliser.ml index 7182ef4f..657e0607 100644 --- a/GillianCore/engine/Abstraction/Normaliser.ml +++ b/GillianCore/engine/Abstraction/Normaliser.ml @@ -173,10 +173,15 @@ module Make (SPState : PState.S) = struct (Exceptions.Impossible "normalise_lexpr: program variable in normalised \ expression") - | BinOp (_, _, _) | UnOp (_, _) -> UnOp (TypeOf, nle1) + | BinOp (_, _, _) | UnOp (_, _) | FuncApp _ | Cases _ -> + UnOp (TypeOf, nle1) | Exists _ | ForAll _ -> Lit (Type BooleanType) | EList _ | LstSub _ | NOp (LstCat, _) -> Lit (Type ListType) - | NOp (_, _) | ESet _ -> Lit (Type SetType)) + | NOp (_, _) | ESet _ -> Lit (Type SetType) + | ConstructorApp (n, _) as c -> ( + match Datatype_env.get_constructor_type n with + | Some t -> Lit (Type t) + | None -> UnOp (TypeOf, c))) | _ -> UnOp (uop, nle1))) | EList le_list -> let n_le_list = List.map f le_list in @@ -226,6 +231,10 @@ module Make (SPState : PState.S) = struct | _, Exists _ -> Exists (bt, ne) | _, ForAll _ -> ForAll (bt, ne) | _, _ -> failwith "Impossible") + | ConstructorApp (n, les) -> ConstructorApp (n, List.map f les) + | FuncApp (n, les) -> FuncApp (n, List.map f les) + | Cases (le, cs) -> + Cases (f le, List.map (fun (c, bs, le) -> (c, bs, f le)) cs) in if not no_types then Typing.infer_types_expr gamma result; diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml index 5bc22548..331dca24 100644 --- a/GillianCore/engine/Abstraction/Verifier.ml +++ b/GillianCore/engine/Abstraction/Verifier.ml @@ -940,6 +940,11 @@ struct L.Phase.with_normal ~title:"Program verification" @@ fun () -> let open ResultsDir in let open ChangeTracker in + (* Prepare datatype env *) + let () = Datatype_env.init prog.datatypes in + let () = Function_env.init prog.funcs in + let () = Smt.init () in + if incremental && prev_results_exist () then ( (* Only verify changed procedures and lemmas *) let cur_source_files = diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index f841f83b..97827d31 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/GillianCore/engine/FOLogic/FOSolver.ml @@ -40,7 +40,7 @@ let simplify_pfs_and_gamma let check_satisfiability_with_model (fs : Expr.t list) (gamma : Type_env.t) : SESubst.t option = let fs, gamma, subst = simplify_pfs_and_gamma fs gamma in - let model = Smt.check_sat fs (Type_env.as_hashtbl gamma) in + let model = Smt.check_sat fs gamma in let lvars = List.fold_left (fun ac vs -> @@ -64,7 +64,7 @@ let check_satisfiability_with_model (fs : Expr.t list) (gamma : Type_env.t) : | None -> None | Some model -> ( try - Smt.lift_model model (Type_env.as_hashtbl gamma) update smt_vars; + Smt.lift_model model gamma update smt_vars; Some subst with e -> let () = @@ -88,7 +88,7 @@ let check_satisfiability if Expr.Set.is_empty fs then true else if Expr.Set.mem Expr.false_ fs then false else - let result = Smt.is_sat fs (Type_env.as_hashtbl gamma) in + let result = Smt.is_sat fs gamma in (* if time <> "" then Utils.Statistics.update_statistics ("FOS: CheckSat: " ^ time) (Sys.time () -. t); *) @@ -198,9 +198,7 @@ let check_entailment let _ = Simplifications.simplify_pfs_and_gamma formulae gamma_left in let model = - Smt.check_sat - (Expr.Set.of_list (PFS.to_list formulae)) - (Type_env.as_hashtbl gamma_left) + Smt.check_sat (Expr.Set.of_list (PFS.to_list formulae)) gamma in let ret = Option.is_none model in L.(verbose (fun m -> m "Entailment returned %b" ret)); diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml index 3bc73242..02fb0cec 100644 --- a/GillianCore/engine/FOLogic/Reduction.ml +++ b/GillianCore/engine/FOLogic/Reduction.ml @@ -136,6 +136,10 @@ let rec normalise_list_expressions (le : Expr.t) : Expr.t = | LstSub (le1, le2, le3) -> LstSub (f le1, f le2, f le3) | Exists (bt, le) -> Exists (bt, f le) | ForAll (bt, le) -> ForAll (bt, f le) + | ConstructorApp (n, les) -> ConstructorApp (n, List.map f les) + | FuncApp (n, les) -> FuncApp (n, List.map f les) + | Cases (le, cs) -> + Cases (f le, List.map (fun (c, bs, le) -> (c, bs, f le)) cs) (* | LstSub(le1, le2, le3) -> (match f le1, f le2, f le3 with @@ -902,6 +906,39 @@ and reduce_lexpr_loop ESet ------------------------- *) | ESet les -> ESet (Expr.Set.elements @@ Expr.Set.of_list @@ List.map f les) + (* ------------------------- + Constructors + ------------------------- *) + | ConstructorApp (n, les) -> ConstructorApp (n, List.map f les) + (* ------------------------- + Function Application + ------------------------- *) + | FuncApp (n, les) -> FuncApp (n, List.map f les) + (* ------------------------- + Cases + ------------------------- *) + | Cases (ConstructorApp (c, les), cs) -> ( + let bles = + List.filter_map + (fun (c', bs, e) -> if c = c' then Some (bs, e) else None) + cs + in + match bles with + | [ (bs, e) ] when List.length bs = List.length les -> + let le = + List.fold_left2 + (fun acc b le -> + Expr.subst_expr_for_expr ~to_subst:(Expr.LVar b) + ~subst_with:le acc) + e bs les + in + f le + | _ -> raise (ReductionException (le, "No case match found"))) + | Cases (le, cs) -> + let le' = f le in + let f' = if not (Expr.equal le le') then f else Fun.id in + let cs' = List.map (fun (c, bs, e) -> (c, bs, f e)) cs in + f' (Cases (le', cs')) (* ------------------------- ForAll + Exists ------------------------- *) @@ -1784,6 +1821,16 @@ and reduce_lexpr_loop when t <> StringType -> Expr.false_ | BinOp (UnOp (TypeOf, BinOp (_, SetMem, _)), Equal, Lit (Type t)) when t <> BooleanType -> Expr.false_ + (* BinOps: Equalities (Constructors) *) + | BinOp (ConstructorApp (ln, lles), Equal, ConstructorApp (rn, rles)) -> + if ln = rn && List.length lles = List.length rles then + Expr.conjunct + (List.map2 (fun le re -> Expr.BinOp (le, Equal, re)) lles rles) + else Expr.false_ + | BinOp (ConstructorApp _, Equal, rle) as le -> ( + match rle with + | LVar _ | ConstructorApp _ | FuncApp _ | Cases _ -> le + | _ -> Expr.false_) (* BinOps: Logic *) | BinOp (Lit (Bool true), And, e) | BinOp (e, And, Lit (Bool true)) diff --git a/GillianCore/smt/smt.ml b/GillianCore/engine/FOLogic/smt.ml similarity index 53% rename from GillianCore/smt/smt.ml rename to GillianCore/engine/FOLogic/smt.ml index a5db04df..de0838fe 100644 --- a/GillianCore/smt/smt.ml +++ b/GillianCore/engine/FOLogic/smt.ml @@ -20,8 +20,8 @@ let () = Sys.(set_signal sigpipe Signal_ignore) exception SMT_unknown let pp_sexp = Sexplib.Sexp.pp_hum -let init_decls : sexp list ref = ref [] let builtin_funcs : sexp list ref = ref [] +let initialised : bool ref = ref false let solver = ref @@ -34,26 +34,6 @@ let solver = let cmd s = ack_command !solver s -let rec init_solver () = - let z3 = new_solver z3 in - let command s = - try z3.command s - with Sys_error s -> - let msg = Fmt.str "Error when calling SMT solver: %s" s in - Logging.normal (fun m -> m "%s" msg); - init_solver (); - raise (Gillian_result.Exc.internal_error msg) - in - let () = solver := { z3 with command } in - (* Config, initial decls *) - let () = - z3_config |> List.iter (fun (k, v) -> cmd (set_option (":" ^ k) v)) - in - let decls = List.rev !init_decls in - let () = decls |> List.iter cmd in - let () = cmd (push 1) in - () - let sanitize_identifier = let pattern = Str.regexp "#" in Str.global_replace pattern "$$" @@ -62,15 +42,11 @@ let is_true = function | Sexplib.Sexp.Atom "true" -> true | _ -> false -type typenv = (string, Type.t) Hashtbl.t [@@deriving to_yojson] - let fs_to_yojson fs = fs |> Expr.Set.to_list |> list_to_yojson Expr.to_yojson let sexps_to_yojson sexps = `List (List.map (fun sexp -> `String (Sexplib.Sexp.to_string_hum sexp)) sexps) -let pp_typenv = Fmt.(Dump.hashtbl string (Fmt.of_to_string Type.str)) - let encoding_cache : (Expr.Set.t, sexp list) Hashtbl.t = Hashtbl.create Config.big_tbl_size @@ -145,6 +121,13 @@ module Variant = struct val access : sexp -> sexp end + module type Nary = sig + include S + + val num_params : int + val construct : sexp list -> sexp + end + let nul ?recognizer name = let recognizer = Option.value recognizer ~default:("is" ^ name) in let module M = struct @@ -167,6 +150,32 @@ module Variant = struct let access x = accessor <| x end in (module M : Unary) + + let n ?recognizer name param_typs = + let module N = (val nul ?recognizer name : Nullary) in + let module M = struct + include N + + let params = + List.mapi + (fun i param_typ -> ("param-" ^ string_of_int i, param_typ)) + param_typs + + let num_params = List.length params + + let construct xs = + let num_params_provided = List.length xs in + if num_params_provided == num_params then atom name $$ xs + else + let msg = + Printf.sprintf + "Invalid number of parameters for the constructor %s. %d \ + parameters were provided, but %d were expected." + name num_params_provided num_params + in + raise (Failure msg) + end in + (module M : Nary) end let declare_recognizer ~name ~constructor ~typ = @@ -175,7 +184,7 @@ let declare_recognizer ~name ~constructor ~typ = t_bool (list [ atom "_"; atom "is"; atom constructor ] <| atom "x") -let mk_datatype name type_params (variants : (module Variant.S) list) = +let mk_datatype' name type_params (variants : (module Variant.S) list) = let constructors, recognizer_defs = variants |> List.map (fun v -> @@ -188,9 +197,28 @@ let mk_datatype name type_params (variants : (module Variant.S) list) = (constructor, recognizer_def)) |> List.split in + let datatype = (name, type_params, constructors) in + (datatype, recognizer_defs) + +let mk_datatype name type_params (variants : (module Variant.S) list) = + let (_, _, constructors), recognizer_defs = + mk_datatype' name type_params variants + in let decl = declare_datatype name type_params constructors in - let () = init_decls := recognizer_defs @ (decl :: !init_decls) in - atom name + decl :: recognizer_defs + +(* Mutually recursive Datatypes *) +let mk_datatypes + (datatypes : (string * string list * (module Variant.S) list) list) = + let datatypes, recognizer_defs = + List.split + (List.map + (fun (name, type_params, variants) -> + mk_datatype' name type_params variants) + datatypes) + in + let decl = declare_datatypes datatypes in + decl :: List.concat recognizer_defs let mk_fun_decl name param_types result_type = let decl = declare_fun name param_types result_type in @@ -211,9 +239,13 @@ module Type_operations = struct module List = (val nul "ListType" : Nullary) module Type = (val nul "TypeType" : Nullary) module Set = (val nul "SetType" : Nullary) + module Datatype = (val un "DatatypeType" "datatype-id" t_int) + + let gil_type_name = "GIL_Type" + let t_gil_type = atom gil_type_name - let t_gil_type = - mk_datatype "GIL_Type" [] + let init_decls = + mk_datatype gil_type_name [] [ (module Undefined : Variant.S); (module Null : Variant.S); @@ -227,6 +259,7 @@ module Type_operations = struct (module List : Variant.S); (module Type : Variant.S); (module Set : Variant.S); + (module Datatype : Variant.S); ] end @@ -237,6 +270,74 @@ module Lit_operations = struct let gil_literal_name = "GIL_Literal" let t_gil_literal = atom gil_literal_name + let t_gil_literal_list = t_seq t_gil_literal + let t_gil_literal_set = t_set t_gil_literal + + let native_sort_of_type = + let open Type in + function + | IntType | StringType | ObjectType -> t_int + | ListType -> t_seq t_gil_literal + | BooleanType -> t_bool + | NumberType -> t_real + | UndefinedType | NoneType | EmptyType | NullType -> t_gil_literal + | SetType -> t_set t_gil_literal + | TypeType -> t_gil_type + | DatatypeType name -> atom name + + let constructor_variants : (string, (module Variant.Nary)) Hashtbl.t ref = + ref (Hashtbl.create 1) + + let datatype_lit_variants : (string, (module Variant.Unary)) Hashtbl.t ref = + ref (Hashtbl.create 1) + + let mk_constructor Constructor.{ constructor_name; constructor_fields; _ } = + let param_typ t = + Option.map native_sort_of_type t |> Option.value ~default:t_gil_literal + in + let param_typs = List.map param_typ constructor_fields in + let module N = (val n constructor_name param_typs : Variant.Nary) in + Hashtbl.add !constructor_variants constructor_name (module N : Variant.Nary); + (module N : Variant.S) + + let mk_user_def_datatype Datatype.{ datatype_name; datatype_constructors; _ } + = + let variants = List.map mk_constructor datatype_constructors in + (datatype_name, [], variants) + + let mk_user_def_datatypes (datatypes : Datatype.t list) = + List.map mk_user_def_datatype datatypes + + let user_def_datatype_lit_variant_name (datatype_name : string) = + "Datatype" ^ datatype_name + + let user_def_datatype_lit_param_name (datatype_name : string) = + datatype_name ^ "Value" + + let mk_user_def_datatype_lit_variant Datatype.{ datatype_name; _ } = + let variant_name = user_def_datatype_lit_variant_name datatype_name in + let t_datatype = atom datatype_name in + let parameter_name = user_def_datatype_lit_param_name datatype_name in + let module N = (val un variant_name parameter_name t_datatype : Unary) in + Hashtbl.add !datatype_lit_variants datatype_name (module N : Unary); + (module N : Variant.S) + + let mk_user_def_datatype_lit_variants datatypes = + List.map mk_user_def_datatype_lit_variant datatypes + + let get_constructor_variant cname = + match Hashtbl.find_opt !constructor_variants cname with + | Some (module N) -> (module N : Nary) + | None -> + let msg = "SMT - Undefined constructor: " ^ cname in + raise (Failure msg) + + let get_datatype_lit_variant dname = + match Hashtbl.find_opt !datatype_lit_variants dname with + | Some (module U) -> (module U : Unary) + | None -> + let msg = "SMT - Undefined datatype: " ^ dname in + raise (Failure msg) module Undefined = (val nul "Undefined" : Nullary) module Null = (val nul "Null" : Nullary) @@ -250,8 +351,11 @@ module Lit_operations = struct module List = (val un "List" "listValue" (t_seq t_gil_literal) : Unary) module None = (val nul "None" : Nullary) - let _ = - mk_datatype gil_literal_name [] + let init_decls user_def_datatypes = + (* Reset variants tables on reinitialisation *) + constructor_variants := Hashtbl.create Config.medium_tbl_size; + datatype_lit_variants := Hashtbl.create Config.medium_tbl_size; + let gil_literal_variants = [ (module Undefined : Variant.S); (module Null : Variant.S); @@ -265,11 +369,22 @@ module Lit_operations = struct (module List : Variant.S); (module None : Variant.S); ] + in + let gil_literal_user_def_variants = + mk_user_def_datatype_lit_variants user_def_datatypes + in + let gil_literal_datatype = + ( gil_literal_name, + [], + gil_literal_variants @ gil_literal_user_def_variants ) + in + mk_datatypes + (gil_literal_datatype :: mk_user_def_datatypes user_def_datatypes) end let t_gil_literal = Lit_operations.t_gil_literal -let t_gil_literal_list = t_seq t_gil_literal -let t_gil_literal_set = t_set t_gil_literal +let t_gil_literal_list = Lit_operations.t_gil_literal_list +let t_gil_literal_set = Lit_operations.t_gil_literal_set let seq_of ~typ = function | [] -> as_type (atom "seq.empty") typ @@ -290,7 +405,10 @@ module Ext_lit_operations = struct module Gil_set = (val un "Set" "setElem" t_gil_literal_set : Unary) - let t_gil_ext_literal = + let gil_ext_literal_name = "Extended_GIL_Literal" + let t_gil_ext_literal = atom gil_ext_literal_name + + let init_decls = mk_datatype "Extended_GIL_Literal" [] [ (module Gil_sing_elem : Variant.S); (module Gil_set : Variant.S) ] end @@ -337,6 +455,8 @@ let encode_type (t : Type.t) = | ListType -> Type_operations.List.construct | TypeType -> Type_operations.Type.construct | SetType -> Type_operations.Set.construct + | DatatypeType name -> + name |> encode_string |> Type_operations.Datatype.construct with _ -> Fmt.failwith "DEATH: encode_type with arg: %a" Type.pp t module Encoding = struct @@ -356,6 +476,7 @@ module Encoding = struct | UndefinedType | NoneType | EmptyType | NullType -> t_gil_literal | SetType -> t_gil_literal_set | TypeType -> t_gil_type + | DatatypeType name -> atom name type t = { consts : (string * sexp) Hashset.t; [@default Hashset.empty ()] @@ -407,24 +528,39 @@ module Encoding = struct in { enc' with consts; extra_asrts } - let get_native ~accessor { expr; kind; _ } = + let get_native + ~accessor + ~recognizer + ~typ + ({ expr; kind; extra_asrts; _ } as enc) : t = (* No additional check is performed on native type, it should be already type checked *) - match kind with - | Native _ -> expr - | Simple_wrapped -> accessor expr - | Extended_wrapped -> - accessor (Ext_lit_operations.Gil_sing_elem.access expr) + let expr, guards = + match kind with + | Native _ -> (expr, []) + | Simple_wrapped -> (accessor expr, [ recognizer expr ]) + | Extended_wrapped -> + let simply_wrapped = Ext_lit_operations.Gil_sing_elem.access expr in + ( accessor simply_wrapped, + [ + recognizer simply_wrapped; + Ext_lit_operations.Gil_sing_elem.recognize expr; + ] ) + in + let extra_asrts = guards @ extra_asrts in + let kind = Native typ in + { enc with expr; extra_asrts; kind } let simply_wrapped = make ~kind:Simple_wrapped + let extended_wrapped = make ~kind:Extended_wrapped (** Takes a value either natively encoded or simply wrapped and returns a value simply wrapped. Careful: do not use wrap with a a set, as they cannot be simply wrapped *) - let simple_wrap { expr; kind; _ } = + let simple_wrap ({ expr; kind; extra_asrts; _ } as enc) = let open Lit_operations in match kind with - | Simple_wrapped -> expr + | Simple_wrapped -> enc | Native typ -> let construct = match typ with @@ -435,35 +571,94 @@ module Encoding = struct | TypeType -> Type.construct | BooleanType -> Bool.construct | ListType -> List.construct + | DatatypeType name -> + let (module U : Variant.Unary) = + Lit_operations.get_datatype_lit_variant name + in + U.construct | UndefinedType | NullType | EmptyType | NoneType | SetType -> Fmt.failwith "Cannot simple-wrap value of type %s" (Gil_syntax.Type.str typ) in - construct expr - | Extended_wrapped -> Ext_lit_operations.Gil_sing_elem.access expr - - let extend_wrap e = - match e.kind with - | Extended_wrapped -> e.expr - | Native SetType -> Ext_lit_operations.Gil_set.construct (simple_wrap e) - | _ -> Ext_lit_operations.Gil_sing_elem.construct (simple_wrap e) - - let get_num = get_native ~accessor:Lit_operations.Num.access - let get_int = get_native ~accessor:Lit_operations.Int.access - let get_bool = get_native ~accessor:Lit_operations.Bool.access - let get_list = get_native ~accessor:Lit_operations.List.access + { enc with expr = construct expr; kind = Simple_wrapped } + | Extended_wrapped -> + let guard = Ext_lit_operations.Gil_sing_elem.recognize expr in + let extra_asrts = guard :: extra_asrts in + let expr = Ext_lit_operations.Gil_sing_elem.access expr in + { enc with extra_asrts; expr; kind = Simple_wrapped } - let get_set { kind; expr; _ } = + let extend_wrap ({ expr; kind; _ } as enc) = + match kind with + | Extended_wrapped -> enc + | Native SetType -> + let expr = Ext_lit_operations.Gil_set.construct expr in + { enc with expr; kind = Extended_wrapped } + | _ -> + let ({ expr; _ } as enc) = simple_wrap enc in + let expr = Ext_lit_operations.Gil_sing_elem.construct expr in + { enc with expr; kind = Extended_wrapped } + + let get_num = + get_native ~accessor:Lit_operations.Num.access + ~recognizer:Lit_operations.Num.recognize ~typ:NumberType + + let get_int = + get_native ~accessor:Lit_operations.Int.access + ~recognizer:Lit_operations.Int.recognize ~typ:IntType + + let get_bool = + get_native ~accessor:Lit_operations.Bool.access + ~recognizer:Lit_operations.Bool.recognize ~typ:BooleanType + + let get_list = + get_native ~accessor:Lit_operations.List.access + ~recognizer:Lit_operations.List.recognize ~typ:ListType + + let get_set ({ kind; expr; extra_asrts; _ } as enc) : t = match kind with - | Native SetType -> expr - | Extended_wrapped -> Ext_lit_operations.Gil_set.access expr + | Native SetType -> enc + | Extended_wrapped -> + let guard = Ext_lit_operations.Gil_set.recognize expr in + let extra_asrts = guard :: extra_asrts in + let expr = Ext_lit_operations.Gil_set.access expr in + let kind = Native SetType in + { enc with extra_asrts; expr; kind } | _ -> failwith "wrong encoding of set" - let get_string = get_native ~accessor:Lit_operations.String.access + let get_string = + get_native ~accessor:Lit_operations.String.access + ~recognizer:Lit_operations.String.recognize ~typ:StringType + + let get_native_of_type ~(typ : Type.t) = + let open Lit_operations in + let accessor, recognizer = + match typ with + | IntType -> (Int.access, Int.recognize) + | NumberType -> (Num.access, Num.recognize) + | StringType -> (String.access, String.recognize) + | ObjectType -> (Loc.access, Loc.recognize) + | TypeType -> (Type.access, Type.recognize) + | BooleanType -> (Bool.access, Bool.recognize) + | ListType -> (List.access, List.recognize) + | DatatypeType name -> + let (module U : Variant.Unary) = get_datatype_lit_variant name in + (U.access, U.recognize) + | UndefinedType | NullType | EmptyType | NoneType | SetType -> + Fmt.failwith "Cannot get native value of type %s" + (Gil_syntax.Type.str typ) + in + get_native ~accessor ~recognizer ~typ end let typeof_simple e = let open Type in + let datatype_guards = + Hashtbl.to_seq !Lit_operations.datatype_lit_variants + |> Seq.map (fun (dname, (module U : Variant.Unary)) -> + (U.recognize, DatatypeType dname)) + |> List.of_seq + in + let guards = Lit_operations. [ @@ -479,6 +674,7 @@ let typeof_simple e = (Type.recognize, TypeType); (List.recognize, ListType); ] + @ datatype_guards in List.fold_left (fun acc (guard, typ) -> ite (guard e) (encode_type typ) acc) @@ -545,7 +741,8 @@ let rec encode_lit (lit : Literal.t) : Encoding.t = | Loc l -> encode_string l >- ObjectType | Type t -> encode_type t >- TypeType | LList lits -> - let args = List.map (fun lit -> simple_wrap (encode_lit lit)) lits in + let>-- args = List.map (fun lit -> simple_wrap (encode_lit lit)) lits in + let args = List.map (fun arg -> arg.expr) args in list args >- ListType | Constant _ -> raise (Exceptions.Unsupported "Z3 encoding: constants") with Failure msg -> @@ -555,23 +752,24 @@ let encode_equality (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = let open Encoding in let>- _ = p1 in let>- _ = p2 in - let res = - match (p1.kind, p2.kind) with - | Native t1, Native t2 when Type.equal t1 t2 -> - if Type.equal t1 BooleanType then - if is_true p1.expr then p2.expr - else if is_true p2.expr then p1.expr - else eq p1.expr p2.expr - else eq p1.expr p2.expr - | Simple_wrapped, Simple_wrapped | Extended_wrapped, Extended_wrapped -> - eq p1.expr p2.expr - | Native _, Native _ -> failwith "incompatible equality, type error!" - | Simple_wrapped, Native _ | Native _, Simple_wrapped -> - eq (simple_wrap p1) (simple_wrap p2) - | Extended_wrapped, _ | _, Extended_wrapped -> - eq (extend_wrap p1) (extend_wrap p2) - in - res >- BooleanType + match (p1.kind, p2.kind) with + | Native t1, Native t2 when Type.equal t1 t2 -> + if Type.equal t1 BooleanType then + if is_true p1.expr then p2.expr >- BooleanType + else if is_true p2.expr then p1.expr >- BooleanType + else eq p1.expr p2.expr >- BooleanType + else eq p1.expr p2.expr >- BooleanType + | Simple_wrapped, Simple_wrapped | Extended_wrapped, Extended_wrapped -> + eq p1.expr p2.expr >- BooleanType + | Native _, Native _ -> failwith "incompatible equality, type error!" + | Simple_wrapped, Native _ | Native _, Simple_wrapped -> + let>- p1 = simple_wrap p1 in + let>- p2 = simple_wrap p2 in + eq p1.expr p2.expr >- BooleanType + | Extended_wrapped, _ | _, Extended_wrapped -> + let>- p1 = extend_wrap p1 in + let>- p2 = extend_wrap p2 in + eq p1.expr p2.expr >- BooleanType let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = @@ -584,37 +782,96 @@ let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t It is expected that values of unknown type are already wrapped into their constructors. *) match op with - | IPlus -> num_add (get_int p1) (get_int p2) >- IntType - | IMinus -> num_sub (get_int p1) (get_int p2) >- IntType - | ITimes -> num_mul (get_int p1) (get_int p2) >- IntType - | IDiv -> num_div (get_int p1) (get_int p2) >- IntType - | IMod -> num_mod (get_int p1) (get_int p2) >- IntType - | ILessThan -> num_lt (get_int p1) (get_int p2) >- BooleanType - | ILessThanEqual -> num_leq (get_int p1) (get_int p2) >- BooleanType - | FPlus -> num_add (get_num p1) (get_num p2) >- NumberType - | FMinus -> num_sub (get_num p1) (get_num p2) >- NumberType - | FTimes -> num_mul (get_num p1) (get_num p2) >- NumberType - | FDiv -> num_div (get_num p1) (get_num p2) >- NumberType - | FLessThan -> num_lt (get_num p1) (get_num p2) >- BooleanType - | FLessThanEqual -> num_leq (get_num p1) (get_num p2) >- BooleanType + | IPlus -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_add p1.expr p2.expr >- IntType + | IMinus -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_sub p1.expr p2.expr >- IntType + | ITimes -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_mul p1.expr p2.expr >- IntType + | IDiv -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_div p1.expr p2.expr >- IntType + | IMod -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_mod p1.expr p2.expr >- IntType + | ILessThan -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_lt p1.expr p2.expr >- IntType + | ILessThanEqual -> + let>- p1 = get_int p1 in + let>- p2 = get_int p2 in + num_leq p1.expr p2.expr >- IntType + | FPlus -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_add p1.expr p2.expr >- NumberType + | FMinus -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_sub p1.expr p2.expr >- NumberType + | FTimes -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_mul p1.expr p2.expr >- NumberType + | FDiv -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_div p1.expr p2.expr >- NumberType + | FLessThan -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_lt p1.expr p2.expr >- NumberType + | FLessThanEqual -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + num_leq p1.expr p2.expr >- NumberType | Equal -> encode_equality p1 p2 - | Or -> bool_or (get_bool p1) (get_bool p2) >- BooleanType - | Impl -> bool_implies (get_bool p1) (get_bool p2) >- BooleanType - | And -> bool_and (get_bool p1) (get_bool p2) >- BooleanType + | Or -> + let>- p1 = get_bool p1 in + let>- p2 = get_bool p2 in + bool_or p1.expr p2.expr >- BooleanType + | Impl -> + let>- p1 = get_bool p1 in + let>- p2 = get_bool p2 in + bool_implies p1.expr p2.expr >- BooleanType + | And -> + let>- p1 = get_bool p1 in + let>- p2 = get_bool p2 in + bool_and p1.expr p2.expr >- BooleanType | SetMem -> (* p2 has to be already wrapped *) - set_member Z3 (simple_wrap p1) (get_set p2) >- BooleanType - | SetDiff -> set_difference Z3 (get_set p1) (get_set p2) >- SetType - | SetSub -> set_subset Z3 (get_set p1) (get_set p2) >- BooleanType - | LstNth -> seq_nth (get_list p1) (get_int p2) |> simply_wrapped + let>- p1 = simple_wrap p1 in + let>- p2 = get_set p2 in + set_member Z3 p1.expr p2.expr >- BooleanType + | SetDiff -> + let>- p1 = get_set p1 in + let>- p2 = get_set p2 in + set_difference Z3 p1.expr p2.expr >- SetType + | SetSub -> + let>- p1 = get_set p1 in + let>- p2 = get_set p2 in + set_subset Z3 p1.expr p2.expr >- BooleanType + | LstNth -> + let>- p1 = get_list p1 in + let>- p2 = get_list p2 in + seq_nth p1.expr p2.expr |> simply_wrapped | LstRepeat -> - let x = simple_wrap p1 in - let n = get_int p2 in - RepeatCache.get x n + let>- x = simple_wrap p1 in + let>- n = get_int p2 in + RepeatCache.get x.expr n.expr | StrNth -> - let str' = get_string p1 in - let index' = get_num p2 in - let res = Axiomatised_operations.snth $$ [ str'; index' ] in + let>- str' = get_string p1 in + let>- index' = get_num p2 in + let res = Axiomatised_operations.snth $$ [ str'.expr; index'.expr ] in res >- StringType | FMod | StrLess @@ -647,31 +904,58 @@ let encode_unop ~llen_lvars ~e (op : UnOp.t) le = let open Axiomatised_operations in let>- _ = le in match op with - | IUnaryMinus -> num_neg (get_int le) >- IntType - | FUnaryMinus -> num_neg (get_num le) >- NumberType + | IUnaryMinus -> + let>- le = get_int le in + num_neg le.expr >- IntType + | FUnaryMinus -> + let>- le = get_num le in + num_neg le.expr >- NumberType | LstLen -> (* If we only use an LVar as an argument to llen, then encode it as an uninterpreted function. *) + let>- le = get_list le in let enc = match e with - | Expr.LVar l when SS.mem l llen_lvars -> llen <| get_list le - | _ -> seq_len (get_list le) + | Expr.LVar l when SS.mem l llen_lvars -> llen <| le.expr + | _ -> seq_len le.expr in enc >- IntType - | StrLen -> slen <| get_string le >- NumberType - | ToStringOp -> Axiomatised_operations.num2str <| get_num le >- StringType - | ToNumberOp -> Axiomatised_operations.str2num <| get_string le >- NumberType - | ToIntOp -> Axiomatised_operations.num2int <| get_num le >- NumberType - | Not -> bool_not (get_bool le) >- BooleanType + | StrLen -> + let>- le = get_string le in + slen <| le.expr >- NumberType + | ToStringOp -> + let>- le = get_num le in + Axiomatised_operations.num2str <| le.expr >- StringType + | ToNumberOp -> + let>- le = get_string le in + Axiomatised_operations.str2num <| le.expr >- NumberType + | ToIntOp -> + let>- le = get_num le in + Axiomatised_operations.num2int <| le.expr >- NumberType + | Not -> + let>- le = get_bool le in + bool_not le.expr >- BooleanType | Cdr -> - let list = get_list le in - seq_extract list (int_k 1) (seq_len list) >- ListType - | Car -> seq_nth (get_list le) (int_k 0) |> simply_wrapped + let>- list = get_list le in + seq_extract list.expr (int_k 1) (seq_len list.expr) >- ListType + | Car -> + let>- list = get_list le in + seq_nth list.expr (int_k 0) |> simply_wrapped | TypeOf -> typeof_expression le >- TypeType - | ToUint32Op -> get_num le |> real_to_int |> int_to_real >- NumberType - | LstRev -> Axiomatised_operations.lrev <| get_list le >- ListType - | NumToInt -> get_num le |> real_to_int >- IntType - | IntToNum -> get_int le |> int_to_real >- NumberType - | IsInt -> num_divisible (get_num le) 1 >- BooleanType + | ToUint32Op -> + let>- le = get_num le in + le.expr |> real_to_int |> int_to_real >- NumberType + | LstRev -> + let>- list = get_list le in + Axiomatised_operations.lrev <| list.expr >- ListType + | NumToInt -> + let>- le = get_num le in + le.expr |> real_to_int >- IntType + | IntToNum -> + let>- le = get_int le in + le.expr |> int_to_real >- NumberType + | IsInt -> + let>- le = get_num le in + num_divisible le.expr 1 >- BooleanType | BitwiseNot | M_isNaN | M_abs @@ -698,46 +982,48 @@ let encode_unop ~llen_lvars ~e (op : UnOp.t) le = let () = L.print_to_all msg in raise (Failure msg) -let encode_quantified_expr +let encode_bound_expr ~(encode_expr : - gamma:typenv -> + gamma:Type_env.t -> llen_lvars:SS.t -> list_elem_vars:SS.t -> 'a -> Encoding.t) - ~mk_quant ~gamma ~llen_lvars ~list_elem_vars - quantified_vars - (assertion : 'a) : Encoding.t = + bound_vars + (expr : 'a) = let open Encoding in - let- () = - match quantified_vars with - | [] -> - (* A quantified assertion with no quantified variables is just the assertion *) - Some (encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion) - | _ -> None - in (* Start by updating gamma with the information provided by quantifier types. There's very few foralls, so it's ok to copy the gamma entirely *) - let gamma = Hashtbl.copy gamma in + let gamma = Type_env.copy gamma in let () = - quantified_vars + bound_vars |> List.iter (fun (x, typ) -> match typ with - | None -> Hashtbl.remove gamma x - | Some typ -> Hashtbl.replace gamma x typ) + | None -> Type_env.remove gamma x + | Some typ -> Type_env.update gamma x typ) in (* Not the same gamma now!*) - let encoded_assertion, consts, extra_asrts = - match encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion with - | { kind = Native BooleanType; expr; consts; extra_asrts } -> - (expr, consts, extra_asrts) - | _ -> failwith "the thing inside forall is not boolean!" + let encoded = encode_expr ~gamma ~llen_lvars ~list_elem_vars expr in + + (* Extra asrts could contain these bound variables - separate these *) + let rec atoms (sexp : sexp) = + match sexp with + | Atom s -> SS.singleton s + | List lst -> List.fold_left SS.union SS.empty (List.map atoms lst) in - let quantified_vars = - quantified_vars + let bs = SS.of_list (List.map fst bound_vars) in + let contains_bound_vars asrt = not (SS.disjoint bs (atoms asrt)) in + let bound_asrts, extra_asrts = + List.partition contains_bound_vars encoded.extra_asrts + in + let encoded = { encoded with extra_asrts } in + + (* Don't declare consts for quantified vars *) + let bound_vars = + bound_vars |> List.map (fun (x, t) -> let sort = match t with @@ -746,17 +1032,50 @@ let encode_quantified_expr in (x, sort)) in - (* Don't declare consts for quantified vars *) let () = - consts + encoded.consts |> Hashtbl.filter_map_inplace (fun c () -> - if List.mem c quantified_vars then None else Some ()) + if List.mem c bound_vars then None else Some ()) + in + (bound_vars, bound_asrts, encoded) + +let encode_quantified_expr + ~(encode_expr : + gamma:Type_env.t -> + llen_lvars:SS.t -> + list_elem_vars:SS.t -> + 'a -> + Encoding.t) + ~mk_quant + ~gamma + ~llen_lvars + ~list_elem_vars + quantified_vars + (assertion : 'a) : Encoding.t = + let open Encoding in + let- () = + match quantified_vars with + | [] -> + (* A quantified assertion with no quantified variables is just the assertion *) + Some (encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion) + | _ -> None + in + let quantified_vars, bound_asrts, encoded = + encode_bound_expr ~encode_expr ~gamma ~llen_lvars ~list_elem_vars + quantified_vars assertion + in + let encoded_assertion, consts, extra_asrts = + match encoded with + | { kind = Native BooleanType; expr; consts; extra_asrts } -> + (expr, consts, extra_asrts) + | _ -> failwith "the thing inside forall is not boolean!" in + let encoded_assertion = bool_ands (encoded_assertion :: bound_asrts) in let expr = mk_quant quantified_vars encoded_assertion in native ~consts ~extra_asrts BooleanType expr let rec encode_logical_expression - ~(gamma : typenv) + ~(gamma : Type_env.t) ~(llen_lvars : SS.t) ~(list_elem_vars : SS.t) (le : Expr.t) : Encoding.t = @@ -767,7 +1086,7 @@ let rec encode_logical_expression | Lit lit -> encode_lit lit | LVar var -> let kind, typ = - match Hashtbl.find_opt gamma var with + match Type_env.get gamma var with | Some typ -> (Native typ, native_sort_of_type typ) | None -> if SS.mem var list_elem_vars then (Simple_wrapped, t_gil_literal) @@ -780,36 +1099,120 @@ let rec encode_logical_expression | BinOp (le1, op, le2) -> encode_binop op (f le1) (f le2) | NOp (SetUnion, les) -> let>-- les = List.map f les in - les |> List.map get_set |> set_union' Z3 >- SetType + let>-- sets = List.map get_set les in + let sets = List.map (fun set -> set.expr) sets in + set_union' Z3 sets >- SetType | NOp (SetInter, les) -> let>-- les = List.map f les in - les |> List.map get_set |> set_intersection' Z3 >- SetType + let>-- sets = List.map get_set les in + let sets = List.map (fun set -> set.expr) sets in + set_intersection' Z3 sets >- SetType | NOp (LstCat, les) -> let>-- les = List.map f les in - les |> List.map get_list |> seq_concat >- ListType + let>-- lists = List.map get_list les in + let lists = List.map (fun list -> list.expr) lists in + seq_concat lists >- ListType | EList les -> let>-- args = List.map f les in - args |> List.map simple_wrap |> seq_of ~typ:t_gil_literal_list >- ListType + let>-- args = List.map simple_wrap args in + let args = List.map (fun arg -> arg.expr) args in + seq_of ~typ:t_gil_literal_list args >- ListType | ESet les -> let>-- args = List.map f les in - args |> List.map simple_wrap |> set_of >- SetType + let>-- args = List.map simple_wrap args in + let args = List.map (fun arg -> arg.expr) args in + set_of args >- SetType | LstSub (lst, start, len) -> let>- lst = f lst in let>- start = f start in let>- len = f len in - let lst = get_list lst in - let start = get_int start in - let len = get_int len in - seq_extract lst start len >- ListType + let>- lst = get_list lst in + let>- start = get_int start in + let>- len = get_int len in + seq_extract lst.expr start.expr len.expr >- ListType | Exists (bt, e) -> encode_quantified_expr ~encode_expr:encode_logical_expression ~mk_quant:exists ~gamma ~llen_lvars ~list_elem_vars bt e | ForAll (bt, e) -> encode_quantified_expr ~encode_expr:encode_logical_expression ~mk_quant:forall ~gamma ~llen_lvars ~list_elem_vars bt e + | FuncApp (name, les) -> ( + let param_typs = Function_env.get_function_param_types name in + match param_typs with + | Some param_typs -> + let extend_wrap_or_native typopt = + match typopt with + | Some typ -> get_native_of_type ~typ + | None -> extend_wrap + in + let>-- args = List.map f les in + let>-- args = List.map2 extend_wrap_or_native param_typs args in + let args = List.map (fun arg -> arg.expr) args in + let sexp = app_ name args in + extended_wrapped sexp + | None -> + let msg = "SMT - Undefined function: " ^ name in + raise (Failure msg)) + | Cases (le, cs) -> + (* Type checking should ensure that all constructors belong to the same datatype *) + let constructors_t = + match cs with + | (cname, _, _) :: _ -> Datatype_env.get_constructor_type_unsafe cname + | [] -> + let msg = "SMT - No cases given in case statement" in + raise (Failure msg) + in + let>- le = f le in + (* Convert to native *) + let>- le_native = get_native_of_type ~typ:constructors_t le in + (* Encode match cases *) + let cs, encs = + List.split + (List.map + (fun (c, bs, e) -> + let (module N : Variant.Nary) = + Lit_operations.get_constructor_variant c + in + let pat = PCon (c, bs) in + let ts = Datatype_env.get_constructor_field_types_unsafe c in + let bts = List.combine bs ts in + (* TODO: How to handle extra asrts involving bound vars?? *) + (* Using ite and mapping to undefined values when extra asrts are false causes queries to time out *) + let _, _, encoded = + encode_bound_expr ~encode_expr:encode_logical_expression ~gamma + ~llen_lvars ~list_elem_vars bts e + in + let encoded = extend_wrap encoded in + let encoded_expr = encoded.expr in + ((pat, encoded_expr), encoded)) + cs) + in + let fallback = (PVar "_", (extend_wrap undefined_encoding).expr) in + let>-- _ = encs in + extended_wrapped (match_datatype le_native.expr (cs @ [ fallback ])) + | ConstructorApp (name, les) -> ( + let param_typs = Datatype_env.get_constructor_field_types name in + match param_typs with + | Some param_typs -> + let simple_wrap_or_native typopt = + match typopt with + | Some typ -> get_native_of_type ~typ + | None -> simple_wrap + in + let>-- args = List.map f les in + let>-- args = List.map2 simple_wrap_or_native param_typs args in + let (module V : Variant.Nary) = + Lit_operations.get_constructor_variant name + in + let args = List.map (fun arg -> arg.expr) args in + let sexp = V.construct args in + sexp >- Datatype_env.get_constructor_type_unsafe name + | None -> + let msg = "SMT - Undefined constructor: " ^ name in + raise (Failure msg)) let encode_assertion_top_level - ~(gamma : typenv) + ~(gamma : Type_env.t) ~(llen_lvars : SS.t) ~(list_elem_vars : SS.t) (a : Expr.t) : Encoding.t = @@ -820,7 +1223,7 @@ let encode_assertion_top_level let s = Printexc.to_string e in let msg = Fmt.str "Failed to encode %a in gamma %a with error %s\n" Expr.pp a - pp_typenv gamma s + Type_env.pp gamma s in let () = L.print_to_all msg in raise e @@ -843,7 +1246,8 @@ let lvars_only_in_llen (fs : Expr.Set.t) : SS.t = fs |> Expr.Set.iter (inspector#visit_expr ()); inspector#get_diff -let lvars_as_list_elements (assertions : Expr.Set.t) : SS.t = +let lvars_as_list_elements ?(exclude = SS.empty) (assertions : Expr.Set.t) : + SS.t = let collector = object (self) inherit [_] Visitors.reduce @@ -873,6 +1277,37 @@ let lvars_as_list_elements (assertions : Expr.Set.t) : SS.t = Containers.SS.union acc inner) Containers.SS.empty es + method! visit_ConstructorApp (exclude, _) _ les = + List.fold_left + (fun acc e -> + match e with + | Expr.LVar x -> + if not (Containers.SS.mem x exclude) then + Containers.SS.add x acc + else acc + | _ -> + let inner = self#visit_expr (exclude, true) e in + Containers.SS.union acc inner) + Containers.SS.empty les + + method! visit_Cases (exclude, is_in_list) le cs = + let cases = + List.fold_left + (fun acc (_, bs, e) -> + (* Treat binders as though they are in a list *) + let binders = + bs + |> List.filter (fun b -> not (Containers.SS.mem b exclude)) + |> List.to_seq + in + let binders = Containers.SS.add_seq binders acc in + let inner = self#visit_expr (exclude, is_in_list) e in + Containers.SS.union binders inner) + Containers.SS.empty cs + in + let scrutinee = self#visit_expr (exclude, is_in_list) le in + Containers.SS.union scrutinee cases + method! visit_LVar (exclude, is_in_list) x = if is_in_list && not (Containers.SS.mem x exclude) then Containers.SS.singleton x @@ -884,11 +1319,11 @@ let lvars_as_list_elements (assertions : Expr.Set.t) : SS.t = in Expr.Set.fold (fun f acc -> - let new_lvars = collector#visit_expr (SS.empty, false) f in + let new_lvars = collector#visit_expr (exclude, false) f in SS.union new_lvars acc) assertions SS.empty -let encode_assertions (fs : Expr.Set.t) (gamma : typenv) : sexp list = +let encode_assertions (fs : Expr.Set.t) (gamma : Type_env.t) : sexp list = let open Encoding in let- () = Hashtbl.find_opt encoding_cache fs in let llen_lvars = lvars_only_in_llen fs in @@ -911,6 +1346,71 @@ let encode_assertions (fs : Expr.Set.t) (gamma : typenv) : sexp list = let () = Hashtbl.replace encoding_cache fs encoded in encoded +let defn_funs_rec fs = + let mk_param_type (x, t) = list [ atom x; t ] in + let mk_param_types pts = list (List.map mk_param_type pts) in + let mk_decl (name, param_types, ret_type, _) = + list [ atom name; mk_param_types param_types; ret_type ] + in + + let decls = list (List.map mk_decl fs) in + let defns = list (List.map (fun (_, _, _, d) -> d) fs) in + app_ "define-funs-rec" [ decls; defns ] + +let encode_functions (fs : Func.t list) : sexp list = + let encode_function (f : Func.t) = + let name = f.func_name in + let param_types = + List.map + (fun (x, t) -> + let x = sanitize_identifier x in + match t with + | Some t -> (x, Encoding.native_sort_of_type t) + | None -> (x, t_gil_ext_literal)) + f.func_params + in + let ret_type = t_gil_ext_literal in + let gamma = Type_env.init () in + let () = + List.iter + (fun (x, t) -> + match t with + | Some t -> Type_env.update gamma x t + | None -> ()) + f.func_params + in + let function_def = Expr.Set.singleton f.func_definition in + let param_names = List.map fst param_types in + let param_names = SS.of_seq (List.to_seq param_names) in + let llen_lvars = lvars_only_in_llen function_def in + (* By excluding params, we ensure they are always encoded as + Extended GIL Literals in the encoded definition. + This allows us to make the assumption that if the type of a + function paramater is not known, then it is t_gil_ext_literal *) + let list_elem_vars = + lvars_as_list_elements ~exclude:param_names function_def + in + let encoded_def = + Encoding.extend_wrap + @@ encode_logical_expression ~gamma ~llen_lvars ~list_elem_vars + f.func_definition + in + let func_body = + if List.length encoded_def.extra_asrts == 0 then encoded_def.expr + else + ite + (bool_ands encoded_def.extra_asrts) + encoded_def.expr + (Encoding.extend_wrap Encoding.undefined_encoding).expr + in + (name, param_types, ret_type, func_body) + in + [ defn_funs_rec (List.map encode_function fs) ] + +module Function_operations = struct + let init_decls fs = encode_functions fs +end + module Dump = struct let counter = ref 0 @@ -946,25 +1446,71 @@ module Dump = struct (Format.formatter_of_out_channel c) "GIL query:\nFS: %a\nGAMMA: %a\nEncoded as SMT Query:\n%a@?" (Fmt.iter ~sep:Fmt.comma Expr.Set.iter Expr.pp) - fs pp_typenv gamma + fs Type_env.pp gamma (Fmt.list ~sep:(Fmt.any "\n") Sexplib.Sexp.pp_hum) cmds) end -let reset_solver () = - let () = cmd (pop 1) in - let () = RepeatCache.clear () in - let () = cmd (push 1) in +let rec init_solver () = + let z3 = new_solver z3 in + let command s = + try z3.command s + with Sys_error s -> + let msg = Fmt.str "Error when calling SMT solver: %s" s in + Logging.normal (fun m -> m "%s" msg); + init_solver (); + raise (Gillian_result.Exc.internal_error msg) + in + let () = solver := { z3 with command } in + (* Config, initial decls *) + let () = + z3_config |> List.iter (fun (k, v) -> cmd (set_option (":" ^ k) v)) + in () -let exec_sat' (fs : Expr.Set.t) (gamma : typenv) : sexp option = +let init () = + if !initialised then + (* Initial declarations already exist *) + (* Pop off initial declarations if necessary *) + cmd (pop 2) + else (* Need to set up Z3 *) + init_solver (); + + (* In both cases, we (re-)declare the initial declarations *) + cmd (push 1); + let type_init_decls = Type_operations.init_decls in + let lit_init_decls = + Lit_operations.init_decls (Datatype_env.get_datatypes ()) + in + let ext_lit_init_decls = Ext_lit_operations.init_decls in + let func_init_decls = + Function_operations.init_decls (Function_env.get_functions ()) + in + let init_decls = + [ type_init_decls; lit_init_decls; ext_lit_init_decls; func_init_decls ] + in + let decls = List.concat init_decls in + let () = decls |> List.iter cmd in + cmd (push 1); + initialised := true + +let init_or_reset () = + if not !initialised then init () + else + (* Otherwise reset it *) + let () = cmd (pop 1) in + let () = RepeatCache.clear () in + let () = cmd (push 1) in + () + +let exec_sat' (fs : Expr.Set.t) (gamma : Type_env.t) : sexp option = let () = L.verbose (fun m -> m "@[About to check SAT of:@\n%a@]@\nwith gamma:@\n@[%a@]\n" (Fmt.iter ~sep:(Fmt.any "@\n") Expr.Set.iter Expr.pp) - fs pp_typenv gamma) + fs Type_env.pp gamma) in - let () = reset_solver () in + let () = init_or_reset () in let encoded_assertions = encode_assertions fs gamma in let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in let () = List.iter cmd !builtin_funcs in @@ -987,7 +1533,7 @@ let exec_sat' (fs : Expr.Set.t) (gamma : typenv) : sexp option = let additional_data = [ ("expressions", fs_to_yojson fs); - ("gamma", typenv_to_yojson gamma); + ("gamma", Type_env.to_yojson gamma); ("encoded_assertions", sexps_to_yojson encoded_assertions); ] in @@ -999,19 +1545,19 @@ let exec_sat' (fs : Expr.Set.t) (gamma : typenv) : sexp option = in ret -let exec_sat (fs : Expr.Set.t) (gamma : typenv) : sexp option = +let exec_sat (fs : Expr.Set.t) (gamma : Type_env.t) : sexp option = try exec_sat' fs gamma with UnexpectedSolverResponse _ as e -> let additional_data = [ ("smt_error", `String (Printexc.to_string e)); ("expressions", fs_to_yojson fs); - ("gamma", typenv_to_yojson gamma); + ("gamma", Type_env.to_yojson gamma); ] in raise Gillian_result.Exc.(internal_error ~additional_data "SMT failure") -let check_sat (fs : Expr.Set.t) (gamma : typenv) : sexp option = +let check_sat (fs : Expr.Set.t) (gamma : Type_env.t) : sexp option = match Hashtbl.find_opt sat_cache fs with | Some result -> let () = @@ -1030,15 +1576,15 @@ let check_sat (fs : Expr.Set.t) (gamma : typenv) : sexp option = let () = Hashtbl.replace sat_cache fs ret in ret -let is_sat (fs : Expr.Set.t) (gamma : typenv) : bool = +let is_sat (fs : Expr.Set.t) (gamma : Type_env.t) : bool = check_sat fs gamma |> Option.is_some let lift_model (model : sexp) - (gamma : typenv) + (gamma : Type_env.t) (subst_update : string -> Expr.t -> unit) (target_vars : Expr.Set.t) : unit = - let () = reset_solver () in + let () = init_or_reset () in let model_eval = (model_eval' !solver model).eval [] in let get_val x = @@ -1057,7 +1603,7 @@ let lift_model in let lift_val (x : string) : Literal.t option = - let* gil_type = Hashtbl.find_opt gamma x in + let* gil_type = Type_env.get gamma x in let* v = get_val x in match gil_type with | NumberType -> @@ -1094,5 +1640,3 @@ let lift_model m "SMT binding for %s: %s\n" x binding) in v |> Option.iter (fun v -> subst_update x (Expr.Lit v))) - -let () = init_solver () diff --git a/GillianCore/engine/FOLogic/smt.mli b/GillianCore/engine/FOLogic/smt.mli new file mode 100644 index 00000000..f8902052 --- /dev/null +++ b/GillianCore/engine/FOLogic/smt.mli @@ -0,0 +1,17 @@ +open Gil_syntax + +exception SMT_unknown + +val init : unit -> unit +val exec_sat : Expr.Set.t -> Type_env.t -> Sexplib.Sexp.t option +val is_sat : Expr.Set.t -> Type_env.t -> bool +val check_sat : Expr.Set.t -> Type_env.t -> Sexplib.Sexp.t option + +val lift_model : + Sexplib.Sexp.t -> + Type_env.t -> + (string -> Expr.t -> unit) -> + Expr.Set.t -> + unit + +val pp_sexp : Sexplib.Sexp.t Fmt.t diff --git a/GillianCore/engine/FOLogic/typing.ml b/GillianCore/engine/FOLogic/typing.ml index edb1327e..8a86e12e 100644 --- a/GillianCore/engine/FOLogic/typing.ml +++ b/GillianCore/engine/FOLogic/typing.ml @@ -153,6 +153,121 @@ module Infer_types_to_gamma = struct tt = ListType && f le1 ListType && f le2 IntType && f le3 IntType | UnOp (op, le) -> infer_unop flag gamma new_gamma op le tt | BinOp (le1, op, le2) -> infer_binop flag gamma new_gamma op le1 le2 tt + | ConstructorApp (n, les) -> + if Datatype_env.is_initialised () then + let field_types = Datatype_env.get_constructor_field_types n in + let check_field le tt = + match tt with + | Some tt -> f le tt + | None -> true + in + match field_types with + | Some tts -> + if List.length tts <> List.length les then false + else + tt = Datatype_env.get_constructor_type_unsafe n + && List.for_all2 check_field les tts + | None -> false + else + (* Can't say for certain whether or not the constructor is typable *) + true + | FuncApp (n, les) -> + if Function_env.is_initialised () then + let check_field le tt = + match tt with + | Some tt -> f le tt + | None -> true + in + let param_types = Function_env.get_function_param_types n in + match param_types with + | Some tts -> + if List.length tts <> List.length les then false + else + (* Only check param types, we don't check return type of function *) + List.for_all2 check_field les tts + | None -> false + else + (* Can't say for certain whether or not the constructor is typable *) + true + | Cases (le, cs) -> + let scrutinee_type_check = + if Datatype_env.is_initialised () then + let constructors = List.map (fun (c, _, _) -> c) cs in + let constructor_types = + List.map Datatype_env.get_constructor_type constructors + in + let constructors_type = + match List.filter_map (fun t -> t) constructor_types with + | [] -> None (* No constructor type was 'Some' *) + | t :: ts -> + if + List.for_all (( = ) t) ts + && Stdlib.( = ) + (List.length constructor_types) + (List.length (t :: ts)) + then Some t (* All constructors have type t *) + else None (* Not all constructors have type t *) + in + (* We expect the scrutinee to have the same type as the constructors *) + (* against which it is being matched. *) + Option.fold ~none:false ~some:(f le) constructors_type + else + (* Can't type check scrutinee - we don't know types of constructors *) + (* Assume it type checks *) + true + in + + let case_type_check (c, bs, le) = + let gamma_copy = Type_env.copy gamma in + let new_gamma_copy = Type_env.copy new_gamma in + let binders_okay = + if Datatype_env.is_initialised () then + let binder_types = Datatype_env.get_constructor_field_types c in + match binder_types with + | None -> + (* Datatype env is initialised but can't find constructor *) + false + | Some ts -> + (* Update type info of binders *) + if List.length ts <> List.length bs then false + else + let () = + List.iter2 + (fun b t -> + let () = + match t with + | Some t -> Type_env.update gamma_copy b t + | None -> Type_env.remove gamma_copy b + in + Type_env.remove new_gamma_copy b) + bs ts + in + true + else + (* Type info not known about binders - simply remove them *) + let () = + List.iter + (fun b -> + let () = Type_env.remove gamma_copy b in + Type_env.remove new_gamma_copy b) + bs + in + true + in + let ret = + if binders_okay then + (* We expect le to have type tt *) + f' gamma_copy new_gamma_copy le tt + else false + in + (* We've updated our new_gamma_copy with a bunch of things. + We need to import everything except the bound variables to the new_gamma *) + Type_env.iter new_gamma_copy (fun x t -> + if not (List.exists (fun y -> String.equal x y) bs) then + Type_env.update new_gamma x t); + ret + in + scrutinee_type_check && List.for_all case_type_check cs | Exists (bt, le) | ForAll (bt, le) -> if not (tt = BooleanType) then false else @@ -296,25 +411,40 @@ module Type_lexpr = struct | false -> def_neg | true -> (None, true)) - let rec typable_list gamma ?(target_type : Type.t option) les = + let rec typable_list + gamma + ?(target_type : Type.t option) + ?(target_types : Type.t option list option) + les = let f = f gamma in - List.for_all - (fun elem -> - let t, ite = - let t, ite = f elem in - match t with - | Some _ -> (t, ite) - | None -> ( - match target_type with - | None -> (t, ite) - | Some tt -> infer_type gamma elem tt) - in - let correct_type = - let ( = ) = Option.equal Type.equal in - target_type = None || t = target_type - in - correct_type && ite) - les + let n = List.length les in + let target_types = + match target_type with + | Some tt -> List.init n (Fun.const (Some tt)) + | None -> ( + match target_types with + | Some tts -> tts + | None -> List.init n (Fun.const None)) + in + if n == List.length target_types then + List.for_all2 + (fun elem target_type -> + let t, ite = + let t, ite = f elem in + match t with + | Some _ -> (t, ite) + | None -> ( + match target_type with + | None -> (t, ite) + | Some tt -> infer_type gamma elem tt) + in + let correct_type = + let ( = ) = Option.equal Type.equal in + target_type = None || t = target_type + in + correct_type && ite) + les target_types + else false and type_unop gamma le (op : UnOp.t) e = let f = f gamma in @@ -444,6 +574,79 @@ module Type_lexpr = struct let _, ite = f gamma_copy e in if not ite then def_neg else infer_type gamma le BooleanType + and type_constructor_app gamma n les = + if Datatype_env.is_initialised () then + let tts_opt = Datatype_env.get_constructor_field_types n in + match tts_opt with + | Some tts -> + if typable_list gamma ?target_types:(Some tts) les then + (* TODO: We don't attempt to infer the type of function applications *) + (* How would we handle recursive functions? *) + (* Requires signifcant change to typing algorithm *) + (None, true) + else def_neg + | None -> def_neg + else (None, true) + + and type_func_app gamma n les = + if Function_env.is_initialised () then + let tts_opt = Function_env.get_function_param_types n in + match tts_opt with + | Some tts -> + if typable_list gamma ?target_types:(Some tts) les then + def_pos (Datatype_env.get_constructor_type n) + else def_neg + | None -> def_neg + else (None, true) + + and type_case gamma t_scrutinee (c, bs, le) = + if Datatype_env.is_initialised () then + let t_constructor = Datatype_env.get_constructor_type c in + let types_match = + match (t_scrutinee, t_constructor) with + | _, None -> false (* Constructor not found in datatype env *) + | Some t1, Some t2 when Type.equal t1 t2 -> true + | None, _ -> true + | _ -> false + in + if not types_match then def_neg + else + (* Set up gamma copy with the binders' type info *) + let gamma_copy = Type_env.copy gamma in + (* By this point we know c is in datatype env *) + let ts = Datatype_env.get_constructor_field_types_unsafe c in + let () = + List.iter2 + (fun b t -> + match t with + | Some t -> Type_env.update gamma_copy b t + | None -> Type_env.remove gamma_copy b) + bs ts + in + f gamma_copy le + else + let gamma_copy = Type_env.copy gamma in + let () = List.iter (fun b -> Type_env.remove gamma_copy b) bs in + f gamma_copy le + + and type_cases gamma le cs = + let topt, ite = f gamma le in + if not ite then def_neg + else + let cases = List.map (type_case gamma topt) cs in + if not (List.for_all (fun (_, ite) -> ite) cases) then def_neg + else + let known_case_types = List.filter_map (fun (topt, _) -> topt) cases in + let cases_type = + match known_case_types with + | [] -> None + | t :: ts when List.for_all (Type.equal t) ts -> Some t + | _ -> None + in + match cases_type with + | Some t -> infer_type gamma (Cases (le, cs)) t + | None -> (None, true) + (** This function returns a triple [(t_opt, b, fs)] where - [t_opt] is the type of [le] if we can find one - [b] indicates if the thing is typable @@ -474,6 +677,9 @@ module Type_lexpr = struct let all_typable = typable_list ?target_type:(Some ListType) les in if all_typable then (Some ListType, true) else def_neg | LstSub (le1, le2, le3) -> type_lstsub gamma le1 le2 le3 + | ConstructorApp (n, les) -> type_constructor_app gamma n les + | FuncApp (n, les) -> type_func_app gamma n les + | Cases (le, cs) -> type_cases gamma le cs in result diff --git a/GillianCore/engine/concrete_semantics/CExprEval.ml b/GillianCore/engine/concrete_semantics/CExprEval.ml index 95b0ce28..0f974c24 100644 --- a/GillianCore/engine/concrete_semantics/CExprEval.ml +++ b/GillianCore/engine/concrete_semantics/CExprEval.ml @@ -330,10 +330,18 @@ and evaluate_expr (store : CStore.t) (e : Expr.t) : CVal.M.t = | NOp (nop, le) -> evaluate_nop nop (List.map ee le) | EList ll -> evaluate_elist store ll | LstSub (e1, e2, e3) -> evaluate_lstsub store e1 e2 e3 - | ALoc _ | LVar _ | ESet _ | Exists _ | ForAll _ -> + | ALoc _ + | LVar _ + | ESet _ + | Exists _ + | ForAll _ + | ConstructorApp _ + | FuncApp _ + | Cases _ -> raise (Exceptions.Impossible - "eval_expr concrete: aloc, lvar, set, exists or for all") + "eval_expr concrete: aloc, lvar, set, exists, for all, case, \ + constructor or function application") with | TypeError msg -> raise (TypeError (msg ^ Fmt.str " in %a" Expr.pp e)) | EvaluationError msg -> diff --git a/GillianCore/engine/dune b/GillianCore/engine/dune index dbeebc87..fde0afa9 100644 --- a/GillianCore/engine/dune +++ b/GillianCore/engine/dune @@ -5,7 +5,6 @@ (public_name gillian.engine) (libraries utils - smt menhirLib fmt cmdliner @@ -14,7 +13,9 @@ gil_parsing logging incrementalAnalysis - debugger_log) + debugger_log + simple_smt + sexplib) (preprocess (pps ppx_deriving.std ppx_deriving_yojson)) (flags diff --git a/GillianCore/engine/general_semantics/eSubst.ml b/GillianCore/engine/general_semantics/eSubst.ml index 73db6e83..b788dd50 100644 --- a/GillianCore/engine/general_semantics/eSubst.ml +++ b/GillianCore/engine/general_semantics/eSubst.ml @@ -455,6 +455,18 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct @return Expression resulting from the substitution. No fresh locations are created. *) let rec subst_in_expr_opt (subst : t) (le : Expr.t) : Expr.t option = + let subst_in_bound_expr bs e = + (* We use Hashtbl.add so that we can later remove the binding and recover the old one! *) + List.iter + (fun x -> + let lvar = Expr.LVar x in + let lvar_e = Option.get (Val.from_expr lvar) in + Hashtbl.add subst lvar lvar_e) + bs; + let e' = subst_in_expr_opt subst e in + List.iter (fun x -> Hashtbl.remove subst (Expr.LVar x)) bs; + e' + in let f_before (le : Expr.t) = match (le : Expr.t) with | LVar _ | ALoc _ | PVar _ -> @@ -462,29 +474,25 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct | (UnOp (LstLen, PVar _) | UnOp (LstLen, LVar _)) when mem subst le -> (Option.map Val.to_expr (get subst le), false) | Exists (bt, e) -> - (* We use Hashtbl.add so that we can later remove the binding and recover the old one! *) - List.iter - (fun (x, _) -> - let lvar = Expr.LVar x in - let lvar_e = Option.get (Val.from_expr lvar) in - Hashtbl.add subst lvar lvar_e) - bt; - let e' = subst_in_expr_opt subst e in - List.iter (fun (x, _) -> Hashtbl.remove subst (Expr.LVar x)) bt; + let e' = subst_in_bound_expr (List.map fst bt) e in let result = Option.map (fun e' -> Expr.Exists (bt, e')) e' in (result, false) | ForAll (bt, e) -> - (* We use Hashtbl.add so that we can later remove the binding and recover the old one! *) - List.iter - (fun (x, _) -> - let lvar = Expr.LVar x in - let lvar_e = Option.get (Val.from_expr lvar) in - Hashtbl.add subst lvar lvar_e) - bt; - let e' = subst_in_expr_opt subst e in - List.iter (fun (x, _) -> Hashtbl.remove subst (Expr.LVar x)) bt; + let e' = subst_in_bound_expr (List.map fst bt) e in let result = Option.map (fun e' -> Expr.ForAll (bt, e')) e' in (result, false) + | Cases (le, cs) -> ( + let cs = + List_utils.flaky_map + (fun (c, bs, e) -> + let e' = subst_in_bound_expr bs e in + Option.map (fun e' -> (c, bs, e')) e') + cs + in + let le = subst_in_expr_opt subst le in + match (cs, le) with + | Some cs, Some le -> (Some (Expr.Cases (le, cs)), false) + | _ -> (None, false)) | _ -> (Some le, true) in Expr.map_opt f_before None le diff --git a/GillianCore/engine/logical_env/datatype_env.ml b/GillianCore/engine/logical_env/datatype_env.ml new file mode 100644 index 00000000..b54efad4 --- /dev/null +++ b/GillianCore/engine/logical_env/datatype_env.ml @@ -0,0 +1,93 @@ +type constructors_tbl = (string, Constructor.t) Hashtbl.t +type datatypes_tbl = (string, Datatype.t) Hashtbl.t +type t = { constructors : constructors_tbl; datatypes : datatypes_tbl } + +let datatype_env : t option ref = ref None + +(* Initialises the datatype env, ensuring datatype definitions are well formed. *) +let init datatypes = + let constructors = Hashtbl.create Config.medium_tbl_size in + + let check_type topt = + let open Type in + match topt with + | Some (DatatypeType n) -> + if not (Hashtbl.mem datatypes n) then + let msg = "Unknown type in constructor definition: " ^ n in + Logging.fail msg + | _ -> () + in + + let add_constructor_to_tbl (c : Constructor.t) = + if Hashtbl.mem constructors c.constructor_name then + let msg = + "Cannot reuse datatype constructor names: " ^ c.constructor_name + in + Logging.fail msg + else List.iter check_type c.constructor_fields; + Hashtbl.add constructors c.constructor_name c + in + + let add_constructors_to_tbl (cs : Constructor.t list) = + List.iter add_constructor_to_tbl cs + in + + let () = + Hashtbl.iter + (fun _ (d : Datatype.t) -> + add_constructors_to_tbl d.datatype_constructors) + datatypes + in + + datatype_env := Some { constructors; datatypes } + +let is_initialised () = + match !datatype_env with + | None -> false + | Some _ -> true + +let get_constructor_type cname : Type.t option = + let delta = !datatype_env in + let constructor = + Option.map (fun delta -> Hashtbl.find_opt delta.constructors cname) delta + in + Option.map + (fun (c : Constructor.t) -> Type.DatatypeType c.constructor_datatype) + (Option.join constructor) + +let get_constructor_type_unsafe cname : Type.t = + let typ = get_constructor_type cname in + match typ with + | Some t -> t + | None -> + raise + (Failure + ("Datatype_env.get_constructor_type_unsafe: constructor " ^ cname + ^ " not found.")) + +let get_constructor_field_types cname : Type.t option list option = + let delta = !datatype_env in + let constructor = + Option.map (fun delta -> Hashtbl.find_opt delta.constructors cname) delta + in + Option.map + (fun (c : Constructor.t) -> c.constructor_fields) + (Option.join constructor) + +let get_constructor_field_types_unsafe cname : Type.t option list = + let ts = get_constructor_field_types cname in + match ts with + | Some ts -> ts + | None -> + raise + (Failure + ("Datatype_env.get_constructor_field_types_unsafe: constructor " + ^ cname ^ " not found.")) + +let get_datatypes () : Datatype.t list = + let res = + Option.map + (fun delta -> List.of_seq (Hashtbl.to_seq_values delta.datatypes)) + !datatype_env + in + Option.value ~default:[] res diff --git a/GillianCore/engine/logical_env/datatype_env.mli b/GillianCore/engine/logical_env/datatype_env.mli new file mode 100644 index 00000000..58d46846 --- /dev/null +++ b/GillianCore/engine/logical_env/datatype_env.mli @@ -0,0 +1,10 @@ +type constructors_tbl = (string, Constructor.t) Hashtbl.t +type datatypes_tbl = (string, Datatype.t) Hashtbl.t + +val init : datatypes_tbl -> unit +val is_initialised : unit -> bool +val get_constructor_type : string -> Type.t option +val get_constructor_type_unsafe : string -> Type.t +val get_constructor_field_types : string -> Type.t option list option +val get_constructor_field_types_unsafe : string -> Type.t option list +val get_datatypes : unit -> Datatype.t list diff --git a/GillianCore/engine/logical_env/function_env.ml b/GillianCore/engine/logical_env/function_env.ml new file mode 100644 index 00000000..550692a3 --- /dev/null +++ b/GillianCore/engine/logical_env/function_env.ml @@ -0,0 +1,19 @@ +type t = (string, Func.t) Hashtbl.t + +let function_env : t option ref = ref None +let init tbl = function_env := Some tbl +let is_initialised () = Option.is_some !function_env + +let get_function_param_types fname = + let phi = !function_env in + let func = Option.map (fun phi -> Hashtbl.find_opt phi fname) phi in + let param_types = + Option.map (fun f -> f.Func.func_params) (Option.join func) + in + let types = Option.map (List.map snd) param_types in + types + +let get_functions () = + let phi = !function_env in + Option.value ~default:[] + @@ Option.map (fun phi -> List.of_seq (Hashtbl.to_seq_values phi)) phi diff --git a/GillianCore/engine/logical_env/function_env.mli b/GillianCore/engine/logical_env/function_env.mli new file mode 100644 index 00000000..403c84d3 --- /dev/null +++ b/GillianCore/engine/logical_env/function_env.mli @@ -0,0 +1,6 @@ +type t = (string, Func.t) Hashtbl.t + +val init : t -> unit +val is_initialised : unit -> bool +val get_function_param_types : string -> Type.t option list option +val get_functions : unit -> Func.t list diff --git a/GillianCore/engine/FOLogic/type_env.ml b/GillianCore/engine/logical_env/type_env.ml similarity index 96% rename from GillianCore/engine/FOLogic/type_env.ml rename to GillianCore/engine/logical_env/type_env.ml index 2cb62659..ea2852f7 100644 --- a/GillianCore/engine/FOLogic/type_env.ml +++ b/GillianCore/engine/logical_env/type_env.ml @@ -4,6 +4,8 @@ open Names open SVal module L = Logging +type constructors_tbl_t = (string, Constructor.t) Hashtbl.t [@@deriving yojson] +type datatypes_tbl_t = (string, Datatype.t) Hashtbl.t [@@deriving yojson] type t = (string, Type.t) Hashtbl.t [@@deriving yojson] let as_hashtbl x = x @@ -17,7 +19,7 @@ let as_hashtbl x = x let init () : t = Hashtbl.create Config.medium_tbl_size (* Copy *) -let copy (x : t) : t = Hashtbl.copy x +let copy x : t = Hashtbl.copy x (* Type of a variable *) let get (x : t) (var : string) : Type.t option = Hashtbl.find_opt x var diff --git a/GillianCore/engine/FOLogic/type_env.mli b/GillianCore/engine/logical_env/type_env.mli similarity index 90% rename from GillianCore/engine/FOLogic/type_env.mli rename to GillianCore/engine/logical_env/type_env.mli index c2d55c89..e69b4b42 100644 --- a/GillianCore/engine/FOLogic/type_env.mli +++ b/GillianCore/engine/logical_env/type_env.mli @@ -7,6 +7,9 @@ open SVal (** @canonical Gillian.Symbolic.Type_env.t *) type t [@@deriving yojson] +type constructors_tbl_t = (string, Constructor.t) Hashtbl.t [@@deriving yojson] +type datatypes_tbl_t = (string, Datatype.t) Hashtbl.t [@@deriving yojson] + val as_hashtbl : t -> (string, Type.t) Hashtbl.t val copy : t -> t val extend : t -> t -> unit diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index f1bbf84b..26dd0d39 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/GillianCore/engine/symbolic_semantics/SState.ml @@ -254,6 +254,10 @@ module Make (SMemory : SMemory.S) : | Exists (bt, e) -> Exists (bt, f e) | ForAll (bt, e) -> ForAll (bt, f e) | Lit _ | LVar _ | ALoc _ -> expr + | ConstructorApp (n, les) -> ConstructorApp (n, List.map f les) + | FuncApp (n, les) -> FuncApp (n, List.map f les) + | Cases (le, cs) -> + Cases (f le, List.map (fun (c, bs, le) -> (c, bs, f le)) cs) in (* Perform reduction *) if no_reduce then result diff --git a/GillianCore/gil_parser/gil_parsing.ml b/GillianCore/gil_parser/gil_parsing.ml index 781b1868..aeac7d36 100644 --- a/GillianCore/gil_parser/gil_parsing.ml +++ b/GillianCore/gil_parser/gil_parsing.ml @@ -294,7 +294,8 @@ module Make (Annot : Annot.S) = struct in Prog.make_indexed ~lemmas:ext_program.lemmas ~preds:ext_program.preds ~only_specs:ext_program.only_specs ~procs ~predecessors - ~macros:ext_program.macros ~bi_specs:ext_program.bi_specs () + ~funcs:ext_program.funcs ~macros:ext_program.macros + ~bi_specs:ext_program.bi_specs ~datatypes:ext_program.datatypes () let parse_literal lexbuf = parse GIL_Parser.lit_target lexbuf let parse_expression lexbuf = parse GIL_Parser.top_level_expr_target lexbuf diff --git a/GillianCore/monadic/delayed.ml b/GillianCore/monadic/delayed.ml index deae9e9a..5436ade0 100644 --- a/GillianCore/monadic/delayed.ml +++ b/GillianCore/monadic/delayed.ml @@ -1,5 +1,6 @@ module Expr = Gil_syntax.Expr module Type = Gil_syntax.Type +module Smt = Engine.Smt exception NonExhaustiveEntailment of Expr.t list diff --git a/GillianCore/monadic/dune b/GillianCore/monadic/dune index d54a77f3..32d89b3d 100644 --- a/GillianCore/monadic/dune +++ b/GillianCore/monadic/dune @@ -2,6 +2,6 @@ (name monadic) (public_name gillian.monadic) (flags -open Utils.Prelude) - (libraries gil_syntax engine utils fmt logging smt) + (libraries gil_syntax engine utils fmt logging) (preprocess (pps ppx_deriving.std ppx_deriving_yojson))) diff --git a/GillianCore/smt/dune b/GillianCore/smt/dune deleted file mode 100644 index 5f83de17..00000000 --- a/GillianCore/smt/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name smt) - (public_name gillian.smt) - (libraries gil_syntax utils simple_smt sexplib) - (preprocess - (pps ppx_deriving.std ppx_deriving_yojson)) - (flags :standard -open Utils.Prelude)) diff --git a/GillianCore/smt/smt.mli b/GillianCore/smt/smt.mli deleted file mode 100644 index 18cebade..00000000 --- a/GillianCore/smt/smt.mli +++ /dev/null @@ -1,18 +0,0 @@ -open Gil_syntax - -exception SMT_unknown - -val exec_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> Sexplib.Sexp.t option -val is_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> bool - -val check_sat : - Expr.Set.t -> (string, Type.t) Hashtbl.t -> Sexplib.Sexp.t option - -val lift_model : - Sexplib.Sexp.t -> - (string, Type.t) Hashtbl.t -> - (string -> Expr.t -> unit) -> - Expr.Set.t -> - unit - -val pp_sexp : Sexplib.Sexp.t Fmt.t diff --git a/wisl/examples/SLL_adt.wisl b/wisl/examples/SLL_adt.wisl new file mode 100644 index 00000000..7ff75bf2 --- /dev/null +++ b/wisl/examples/SLL_adt.wisl @@ -0,0 +1,317 @@ +datatype MyList { + Nil; + Cons(Any, MyList) +} + +pure function append(xs : MyList, x) { + case xs { + Nil -> 'Cons(x, 'Nil); + Cons(y, ys) -> 'Cons(y, append(ys, x)) + } +} + +pure function length(xs : MyList) { + case xs { + Nil -> 0; + Cons(x, xs) -> 1 + length(xs) + } +} + +pure function concatenate(xs : MyList, ys : MyList) { + case xs { + Nil -> ys; + Cons(x, xs) -> 'Cons(x, concatenate(xs, ys)) + } +} + +pure function double_length(xs : MyList) { + case xs { + Nil -> 0; + Cons(x, xs) -> 2 + length(xs) + } +} + +pure function reverse(xs : MyList) { + case xs { + Nil -> 'Nil; + Cons(x, xs) -> append(reverse(xs), x) + } +} + +pure function list_member(xs : MyList, x) { + case xs { + Nil -> false; + Cons(y, ys) -> (y == x) || list_member(ys, x) + } +} + +// +// Lemma: List membership append +// +lemma list_member_append { + statement: + forall vs, v, r, w. + (list_member(vs, v) == r) |- (list_member(append(vs, w), v) == (r || (w == v))) + + proof: + if (w == v) {} else {}; // FIXME: THIS IS HORRIFIC + if (vs != 'Nil) { + assert {bind: #nv, #nvs, #nr} (vs == 'Cons(#nv, #nvs)) * (list_member(#nvs, #v) == #nr); + apply list_member_append(#nvs, v, #nr, w) + } +} + +// +// Lemma: List membership concat +// +lemma list_member_concat { + statement: + forall vs1, vs2, v. + (list_member(vs1, v) == #r1) * (list_member(vs2, v) == #r2) |- (list_member(concatenate(vs1, vs2), v) == (#r1 || #r2)) + + proof: + if (vs1 != 'Nil) { + assert {bind: #nv1, #nvs1, #nr1} ('Cons(#nv1, #nvs1) == vs1) * (list_member(#nvs1, v) == #nr1); + apply list_member_concat(#nvs1, vs2, v) + } +} + +// +// Standard over-approximating SLL predicate with contents +// +predicate SLL(+x, vs) { + // Empty SLL + (x == null) * (vs == 'Nil); + // One SLL node and the rest + (x -b> #v, #next) * SLL(#next, #vs) * + (vs == 'Cons(#v, #vs)) +} + +// 00. Allocating an SLL node with the given value +{ v == #v } +function SLL_allocate_node(v){ + t := new(2); + [t] := v; + return t +} +{ SLL(ret, 'Cons(#v, 'Nil)) } + +// This incorrect spec should fail to verify +{ (v == #v) * (u == #u) } +function SLL_allocate_node_fails(u, v){ + t := new(2); + [t] := v; + return t +} +{ SLL(ret, 'Cons(#u, 'Nil)) } + + +// +// RECURSIVE SLL MANIPULATION +// + +// 01. Prepending a given value to a given SLL +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_prepend(x, k){ + z := SLL_allocate_node(k); + [z + 1] := x; + return z +} +{ SLL(ret, 'Cons(#k, #vs)) } + +// 02. Appending a given value to a given SLL +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_append(x, k){ + if (x == null) { + x := SLL_allocate_node(k) + } else { + t := [x + 1]; + z := SLL_append(t, k); + [x + 1] := z + }; + return x +} +{ SLL(ret, append(#vs, #k)) } + +// 03. Appending a given SLL node to a given SLL +{ (x == #x) * (y == #y) * SLL(#x, #vs) * SLL(#y, 'Cons(#vy, 'Nil)) } +function SLL_append_node(x, y) { + if (x == null) { + x := y + } else { + t := [x + 1]; + z := SLL_append_node(t, y); + [x + 1] := z + }; + return x +} +{ SLL(ret, append(#vs, #vy)) } + +// 04. Concatenating two lists +{(x == #x) * (y == #y) * SLL(#x, #vx) * SLL(#y, #vy) } +function SLL_concat(x, y) { + if (x == null){ + x := y + } else { + t := [x + 1]; + z := SLL_concat(t, y); + [x + 1] := z + }; + return x +} +{ SLL(ret, concatenate(#vx, #vy)) } + +// 05. Copying a given SLL +{ (x == #x) * SLL(#x, #vs) } +function SLL_copy(x){ + y := null; + if (x != null) { + k := [x]; + y := SLL_allocate_node(k); + t := [x + 1]; + z := SLL_copy(t); + [y + 1] := z + } else { + skip + }; + return y +} +{ SLL(#x, #vs) * SLL(ret, #vs) } + +// 06. Calculating the length of a given SLL +{ (x == #x) * SLL(#x, #vs) } +function SLL_length(x) { + n := 0; + if (x == null){ + n := 0 + } else { + t := [x + 1]; + n := SLL_length(t); + n := 1 + n + }; + return n +} +{ ret == length(#vs) } + +// This spec fails to verify +{ (x == #x) * SLL(#x, #vs) } +function SLL_length_fails(x) { + n := 0; + if (x == null){ + n := 0 + } else { + t := [x + 1]; + n := SLL_length(t); + n := 1 + n + }; + return n +} +{ ret == double_length(#vs) } + +// 07. Reversing a given SLL +{ (x == #x) * SLL(#x, #vs) } +function SLL_reverse(x){ + if (x != null) { + t := [x + 1]; + [x + 1] := null; + z := SLL_reverse(t); + y := SLL_append_node(z, x) + } else { + y := null + }; + return y +} +{ SLL(ret, reverse(#vs)) } + +// 08. Checking if a given value is in a given SLL +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_member(x, k){ + found := false; + if (x == null){ + skip + } else { + v := [x]; + if (v == k){ + found := true + } else { + t := [x + 1]; + found := SLL_member(t, k) + } + }; + return found +} +{ SLL(#x, #vs) * (ret == list_member(#vs, #k)) } + +// 09. Removing a given value from a given SLL +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_remove(x, k) { + if (x == null) { + skip + } else { + v := [x]; + next := [x + 1]; + if (v == k){ + free(x); + x := SLL_remove(next, k) + } else { + z := SLL_remove(next, k); + [x + 1] := z + } + }; + return x +} +{ SLL(ret, #nvs) * (list_member(#nvs, #k) == false) } + +// This spec should fail +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_remove_fails_1(x, k) { + if (x == null) { + skip + } else { + v := [x]; + next := [x + 1]; + if (v == k){ + free(x); + x := SLL_remove(next, k) + } else { + z := SLL_remove(next, k); + [x + 1] := z + } + }; + return x +} +{ SLL(ret, #nvs) * (list_member(#nvs, #k) == true) } + +// So should this one +{ (x == #x) * (k == #k) * SLL(#x, #vs) } +function SLL_remove_fails_2(x, k) { + if (x == null) { + skip + } else { + v := [x]; + next := [x + 1]; + if (v == k){ + z := SLL_remove(next, k); + [x + 1] := z + } else { + z := SLL_remove(next, k); + [x + 1] := z + } + }; + return x +} +{ SLL(ret, #nvs) * (list_member(#nvs, #k) == false) } + +// 10. Freeing a given SLL +{ (x == #x) * SLL(#x, #vs) } +function SLL_free(x){ + if (x == null) { + skip + } else { + t := [x + 1]; + z := SLL_free(t); + free(x) + }; + return null +} +{ (ret == null) } diff --git a/wisl/examples/SLL_ex_complete.wisl b/wisl/examples/SLL_ex_complete.wisl index 930f2bbd..82aa8857 100644 --- a/wisl/examples/SLL_ex_complete.wisl +++ b/wisl/examples/SLL_ex_complete.wisl @@ -481,4 +481,4 @@ function SLL_free_iter(x) { }; return null } -{ (ret == null) } \ No newline at end of file +{ (ret == null) } diff --git a/wisl/examples/SLL_ex_ongoing.wisl b/wisl/examples/SLL_ex_ongoing.wisl index 9eecc39b..71f353af 100644 --- a/wisl/examples/SLL_ex_ongoing.wisl +++ b/wisl/examples/SLL_ex_ongoing.wisl @@ -515,4 +515,4 @@ function SLL_free(x){ }; return null } -{ (ret == null) * SLL_free_post(#def, #x, #xs)} \ No newline at end of file +{ (ret == null) * SLL_free_post(#def, #x, #xs)} diff --git a/wisl/examples/SLL_iterative.wisl b/wisl/examples/SLL_iterative.wisl index dbe4782b..2c639b6d 100644 --- a/wisl/examples/SLL_iterative.wisl +++ b/wisl/examples/SLL_iterative.wisl @@ -96,4 +96,4 @@ function concat(x, y) { }; return x } -{ list(ret, #alpha @ #beta) } \ No newline at end of file +{ list(ret, #alpha @ #beta) } diff --git a/wisl/examples/SLL_recursive.wisl b/wisl/examples/SLL_recursive.wisl index ffd6a9df..5b01b5f1 100644 --- a/wisl/examples/SLL_recursive.wisl +++ b/wisl/examples/SLL_recursive.wisl @@ -73,4 +73,4 @@ function concat(x, y) { // }; // return null // } -// { emp } \ No newline at end of file +// { emp } diff --git a/wisl/examples/function.wisl b/wisl/examples/function.wisl new file mode 100644 index 00000000..4f87ad2f --- /dev/null +++ b/wisl/examples/function.wisl @@ -0,0 +1,29 @@ +pure function double(x : Int) { + x + x +} + +pure function triple(x : Int) { + x + x + x +} + +{ x == #x } +function times_two(x) { + y := x * 2; + return y +} +{ ret == double(#x) } + +{ x == #x } +function times_three(x) { + y := x * 3; + return y +} +{ ret == triple(#x) } + +// This spec fails to verify +{ x == #x } +function times_four(x) { + y := x * 4; + return y +} +{ ret == triple(#x) } diff --git a/wisl/examples/tree.wisl b/wisl/examples/tree.wisl index 15d79de7..3312d655 100644 --- a/wisl/examples/tree.wisl +++ b/wisl/examples/tree.wisl @@ -16,4 +16,4 @@ function tree_dispose(x) { }; return null } -{ emp } \ No newline at end of file +{ emp } diff --git a/wisl/lib/ParserAndCompiler/WLexer.mll b/wisl/lib/ParserAndCompiler/WLexer.mll index 8785c8b9..6aeb5813 100644 --- a/wisl/lib/ParserAndCompiler/WLexer.mll +++ b/wisl/lib/ParserAndCompiler/WLexer.mll @@ -34,8 +34,10 @@ rule read = | "new" { NEW (curr lexbuf) } | "free" { DELETE (curr lexbuf) } | "dispose"{ DELETE (curr lexbuf) } + | "pure" { PURE (curr lexbuf) } | "function" { FUNCTION (curr lexbuf) } | "predicate" { PREDICATE (curr lexbuf) } + | "datatype" { DATATYPE (curr lexbuf) } | "invariant" { INVARIANT (curr lexbuf) } | "return" { RETURN (curr lexbuf) } | "fold" { FOLD (curr lexbuf) } @@ -53,11 +55,13 @@ rule read = | "lemma" { LEMMA (curr lexbuf) } | "forall" { FORALL (curr lexbuf) } | "bind" { EXIST (curr lexbuf) } + | "case" { CASE (curr lexbuf) } (* types *) | "List" { TLIST (curr lexbuf) } | "Int" { TINT (curr lexbuf) } | "Bool" { TBOOL (curr lexbuf) } | "String" { TSTRING (curr lexbuf) } + | "Any" { TANY (curr lexbuf) } (* strings and comments *) | '"' { let () = l_start_string := curr lexbuf in read_string (Buffer.create 17) lexbuf } @@ -84,6 +88,7 @@ rule read = | ',' { COMMA (curr lexbuf) } | "." { DOT (curr lexbuf) } | ';' { SEMICOLON (curr lexbuf) } + | '\'' { QUOTE (curr lexbuf) } | "|-" { VDASH (curr lexbuf) } (* binary operators *) | "::" { LSTCONS } diff --git a/wisl/lib/ParserAndCompiler/WParser.mly b/wisl/lib/ParserAndCompiler/WParser.mly index d3624acb..a4b82e3c 100644 --- a/wisl/lib/ParserAndCompiler/WParser.mly +++ b/wisl/lib/ParserAndCompiler/WParser.mly @@ -2,8 +2,8 @@ (* key words *) %token TRUE FALSE NULL WHILE IF ELSE SKIP FRESH NEW DELETE -%token FUNCTION RETURN PREDICATE LEMMA -%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE EXIST FORALL +%token PURE FUNCTION RETURN PREDICATE LEMMA DATATYPE +%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE EXIST FORALL CASE %token STATEMENT WITH VARIANT PROOF CONFIG (* punctuation *) @@ -23,12 +23,14 @@ %token SETOPEN /* -{ */ %token SETCLOSE /* }- */ %token VDASH /* |- */ +%token QUOTE /* ' */ (* types *) %token TLIST %token TINT %token TBOOL %token TSTRING +%token TANY (* names *) %token IDENTIFIER @@ -85,56 +87,70 @@ %start prog %start assert_only -%type - definitions -%type config -%type fct_with_specs -%type fct -%type predicate -%type lemma -%type var_list -%type statement_list_and_return -%type statement_list -%type expression -%type expr_list -%type logic_command -%type logic_assertion -%type value_with_loc -%type unop_with_loc -%type binop -%type variant_def -%type with_variant_def -%type proof_def -%type <(string * WType.t option) * bool> pred_param_ins -%type bindings_with_loc -%type logic_expression -%type logic_binop -%type logic_value_with_loc +%type + definitions +%type config +%type fct_with_specs +%type fct +%type predicate +%type lemma +%type datatype +%type pure_function +%type var_list +%type statement_list_and_return +%type statement_list +%type expression +%type expr_list +%type logic_command +%type logic_assertion_top_level +%type logic_assertion +%type value_with_loc +%type unop_with_loc +%type binop +%type variant_def +%type with_variant_def +%type proof_def +%type <(string * WType.t option) * bool> pred_param_ins +%type bindings_with_loc +%type logic_expression +%type logic_binop +%type logic_value_with_loc +%type constructor +%type constructor_fields +%type pure_function_param +%type tuple_binders +%type logic_case %% prog: - | fcp = definitions; EOF { - let (fc, preds, lemmas, configs) = fcp in - let prog = WProg.{ lemmas = lemmas; predicates = preds; context = fc } in + | defs = definitions; EOF { + let (fc, preds, lemmas, datatypes, pure_funcs, configs) = defs in + let prog = WProg.{ lemmas = lemmas; predicates = preds; context = fc; datatypes = datatypes; pure_functions = pure_funcs} in prog, configs } assert_only: - | la = logic_assertion; EOF { la } + | la = logic_assertion_top_level; EOF { la } definitions: - | (* empty *) { ([], [], [], []) } - | defs = definitions; p = config - { let (fs, ps, ls, cs) = defs in - (fs, ps, ls, p::cs) } + | (* empty *) { ([], [], [], [], [], []) } | defs = definitions; p = predicate - { let (fs, ps, ls, cs) = defs in - (fs, p::ps, ls, cs) } + { let (fs, ps, ls, ds, pfs, cs) = defs in + (fs, p::ps, ls, ds, pfs, cs) } | defs = definitions; l = lemma - { let (fs, ps, ls, cs) = defs in - (fs, ps, l::ls, cs) } + { let (fs, ps, ls, ds, pfs, cs) = defs in + (fs, ps, l::ls, ds, pfs, cs) } | defs = definitions; f = fct_with_specs - { let (fs, ps, ls, cs) = defs in - (f::fs, ps, ls, cs) } + { let (fs, ps, ls, ds, pfs, cs) = defs in + (f::fs, ps, ls, ds, pfs, cs) } + | defs = definitions; d = datatype + { let (fs, ps, ls, ds, pfs, cs) = defs in + (fs, ps, ls, d::ds, pfs, cs) } + | defs = definitions; pf = pure_function + { let (fs, ps, ls, ds, pfs, cs) = defs in + (fs, ps, ls, ds, pf::pfs, cs) } + | defs = definitions; c = config + { let (fs, ps, ls, ds, pfs, cs) = defs in + (fs, ps, ls, ds, pfs, c::cs) } config: | lstart = CONFIG; id = IDENTIFIER; COLON; value = value_with_loc @@ -144,8 +160,8 @@ config: id, value, loc } fct_with_specs: - | lstart = LCBRACE; pre = logic_assertion; RCBRACE; variant = option(with_variant_def); f = fct; LCBRACE; - post = logic_assertion; lend = RCBRACE + | lstart = LCBRACE; pre = logic_assertion_top_level; RCBRACE; variant = option(with_variant_def); f = fct; LCBRACE; + post = logic_assertion_top_level; lend = RCBRACE { let loc = CodeLoc.merge lstart lend in WFun.add_spec f pre post variant loc } | f = fct { f } @@ -197,6 +213,8 @@ type_target: | TINT { WType.WInt } | TBOOL { WType.WBool } | TSTRING { WType.WString } + | TANY { WType.WAny } + | datatype = IDENTIFIER { let (_, datatype) = datatype in WType.WDatatype datatype } statement: | loc = SKIP { WStmt.make WStmt.Skip loc } @@ -355,7 +373,7 @@ lemma: | lstart = LEMMA; lname = IDENTIFIER; LCBRACE; STATEMENT; COLON; FORALL lemma_params = var_list; DOT; - lemma_hypothesis = logic_assertion; VDASH; lemma_conclusion = logic_assertion; + lemma_hypothesis = logic_assertion_top_level; VDASH; lemma_conclusion = logic_assertion_top_level; lemma_variant = option(variant_def); lemma_proof = option(proof_def); lend = RCBRACE @@ -385,7 +403,7 @@ proof_def: predicate: | lstart = PREDICATE; pred_nounfold = option(NOUNFOLD); lpname = IDENTIFIER; LBRACE; params_ins = separated_list(COMMA, pred_param_ins); RBRACE; LCBRACE; - pred_definitions = separated_nonempty_list(SEMICOLON, logic_assertion); + pred_definitions = separated_nonempty_list(SEMICOLON, logic_assertion_top_level); lend = RCBRACE; { let (_, pred_name) = lpname in let (pred_params, ins) : (string * WType.t option) list * bool list = List.split params_ins in @@ -396,7 +414,7 @@ predicate: (* ins looks like [Some 0, Some 2] *) let ins = List.map Option.get ins in (* ins looks like [0, 2] *) - let pred_ins = if (List.length ins) > 0 then ins else (List.mapi (fun i _ -> i) pred_params) in + let pred_ins = if (List.length ins) > 0 then ins else (List.mapi (fun i _ -> i) pred_params) in (* if ins is empty then everything is an in *) let pred_nounfold = (pred_nounfold <> None) in let pred_loc = CodeLoc.merge lstart lend in @@ -453,13 +471,13 @@ logic_command: { let bare_lcmd = WLCmd.LogicIf (g, thencmds, []) in let loc = CodeLoc.merge lstart lend in WLCmd.make bare_lcmd loc } - | lstart = ASSERT; lbopt = option(bindings_with_loc); a = logic_assertion; + | lstart = ASSERT; lbopt = option(bindings_with_loc); a = logic_assertion_top_level; { let lend = WLAssert.get_loc a in let (_, b) = Option.value ~default:(lstart, []) lbopt in let loc = CodeLoc.merge lstart lend in let bare_lcmd = WLCmd.Assert (a, b) in WLCmd.make bare_lcmd loc } - | lstart = INVARIANT; lbopt = option(bindings_with_loc); a = logic_assertion; variant = option(with_variant_def); + | lstart = INVARIANT; lbopt = option(bindings_with_loc); a = logic_assertion_top_level; variant = option(with_variant_def); { let lend = WLAssert.get_loc a in let (_, b) = Option.value ~default:(lstart, []) lbopt in let loc = CodeLoc.merge lstart lend in @@ -487,6 +505,12 @@ wand: ((lname, largs), (rname, rargs), loc) } +logic_assertion_top_level: + | formula = logic_expression; + { let bare_assert = WLAssert.LPure formula in + let loc = WLExpr.get_loc formula in + WLAssert.make bare_assert loc } + | la = logic_assertion; { la } logic_assertion: | lstart = LBRACE; la = logic_assertion; lend = RBRACE; @@ -537,16 +561,6 @@ logic_assertion: { let bare_assert = WLAssert.LPure formula in let loc = CodeLoc.merge lstart lend in WLAssert.make bare_assert loc } - | loc = TRUE - { let bare_lexpr = WLExpr.LVal (WVal.Bool true) in - let lexpr = WLExpr.make bare_lexpr loc in - let bare_assert = WLAssert.LPure lexpr in - WLAssert.make bare_assert loc } - | loc = FALSE - { let bare_lexpr = WLExpr.LVal (WVal.Bool false) in - let lexpr = WLExpr.make bare_lexpr loc in - let bare_assert = WLAssert.LPure lexpr in - WLAssert.make bare_assert loc } @@ -597,7 +611,24 @@ logic_expression: { let loc = CodeLoc.merge lstart lend in let bare_lexpr = WLExpr.LESet l in WLExpr.make bare_lexpr loc } - + | lpf = IDENTIFIER; LBRACE; l = separated_list(COMMA, logic_expression); lend = RBRACE + { let (lstart, pf) = lpf in + let loc = CodeLoc.merge lstart lend in + let bare_lexpr = WLExpr.LPureFunApp (pf, l) in + WLExpr.make bare_lexpr loc } + | lstart = QUOTE; lname = IDENTIFIER; + llend = option(logic_constructor_app_params) + { let (_, name) = lname in + let (l, lend) = Option.value ~default:([], lstart) llend in + let loc = CodeLoc.merge lstart lend in + let bare_lexpr = WLExpr.LConstructorApp (name, l) in + WLExpr.make bare_lexpr loc } + | lstart = CASE; scrutinee = logic_expression; LCBRACE; cases = separated_list(SEMICOLON, logic_case); lend = RCBRACE + { + let loc = CodeLoc.merge lstart lend in + let bare_lexpr = WLExpr.LCases(scrutinee, cases) in + WLExpr.make bare_lexpr loc + } (* We also have lists in the logic *) logic_binop: @@ -614,3 +645,86 @@ logic_value_with_loc: { let (_, vl) = List.split lvl in let loc = CodeLoc.merge lstart lend in (loc, WVal.VList vl) } */ + +logic_constructor_app_params: + | LBRACE; lst = separated_list(COMMA, logic_expression); lend = RBRACE; { (lst, lend) } + +logic_case: + | cname = IDENTIFIER; binders = option(tuple_binders); ARROW; expr = logic_expression + { + let binders = Option.value ~default:[] binders in + { WLExpr.constructor = snd cname; + binders = binders; + lexpr = expr } + } + +tuple_binders: + | LBRACE; xs = separated_list(COMMA, IDENTIFIER); RBRACE + { List.map snd xs } + + +(* ADT definitions *) + +datatype: + | lstart = DATATYPE; ldname = IDENTIFIER; LCBRACE; + raw_constructors = separated_nonempty_list(SEMICOLON, constructor); + lend = RCBRACE; + { + let (_, datatype_name) = ldname in + let datatype_loc = CodeLoc.merge lstart lend in + let datatype_id = Generators.gen_id () in + let datatype_constructors = + List.map + (fun (constructor_name, constructor_fields, constructor_loc, constructor_id) -> + WConstructor.{ + constructor_name; + constructor_fields; + constructor_loc; + constructor_id; + constructor_datatype = datatype_name; + }) + raw_constructors + in + WDatatype.{ + datatype_name; + datatype_constructors; + datatype_loc; + datatype_id; + } + } + +constructor: + | lcname = IDENTIFIER; fields_lend = option(constructor_fields) + { + let (lstart, constructor_name) = lcname in + let (constructor_fields, lend) = Option.value ~default:([], lstart) fields_lend in + let constructor_loc = CodeLoc.merge lstart lend in + let constructor_id = Generators.gen_id () in + (* Constructor_datatype is added later in the datatype rule *) + (constructor_name, constructor_fields, constructor_loc, constructor_id) + } + +constructor_fields: + | LBRACE; args = separated_list(COMMA, type_target); lend = RBRACE + { (args, lend) } + + +(* Pure Functions *) + +pure_function: + | lstart = PURE; FUNCTION; lpfname = IDENTIFIER; LBRACE; pure_fun_params = separated_list(COMMA, pure_function_param); + RBRACE; LCBRACE; pure_fun_definition=logic_expression; lend = RCBRACE + { + let pure_fun_loc = CodeLoc.merge lstart lend in + let (_, pure_fun_name) = lpfname in + WPureFun.{ + pure_fun_name; + pure_fun_params; + pure_fun_definition; + pure_fun_loc; + } + } + +pure_function_param: + | lx = IDENTIFIER; typ = option(preceded(COLON, type_target)) + { let (_, x) = lx in (x, typ) } diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml index 1540ae76..c6d2a0a7 100644 --- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml +++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml @@ -27,6 +27,7 @@ let compile_type t = | WPtr -> Some Type.ObjectType | WInt -> Some Type.IntType | WSet -> Some Type.SetType + | WDatatype n -> Some (Type.DatatypeType n) | WAny -> None) let compile_binop b = @@ -149,10 +150,12 @@ let rec compile_expr ?(fname = "main") ?(is_loop_prefix = false) expr : (* compile_lexpr : WLExpr.t -> (string list * Asrt.t list * Expr.t) compiles a WLExpr into an output expression and a list of Global Assertions. the string list contains the name of the variables that are generated. They are existentials. *) -let rec compile_lexpr ?(fname = "main") (lexpr : WLExpr.t) : - string list * Asrt.t * Expr.t = +let rec compile_lexpr + ?(fname = "main") + ?(is_pure_fun_def = false) + (lexpr : WLExpr.t) : string list * Asrt.t * Expr.t = let gen_str = Generators.gen_str fname in - let compile_lexpr = compile_lexpr ~fname in + let compile_lexpr = compile_lexpr ~fname ~is_pure_fun_def in let expr_pname_of_binop b = WBinOp.( match b with @@ -177,10 +180,14 @@ let rec compile_lexpr ?(fname = "main") (lexpr : WLExpr.t) : WLExpr.( match get lexpr with | LVal v -> ([], [], Expr.Lit (compile_val v)) + | PVar x when is_pure_fun_def -> ([], [], Expr.LVar x) | PVar x -> ([], [], Expr.PVar x) | LVar x -> ([], [], Expr.LVar x) - | LBinOp (e1, b, e2) when is_internal_pred b -> + | LBinOp (e1, b, e2) when is_internal_pred b && Stdlib.not is_pure_fun_def + -> (* Operator corresponds to pointer arithmetics *) + (* Functions are pure, so can't create global assertions *) + (* TODO: functions don't support pointer arithmetic *) let lout = gen_str sgvar in let internal_pred = expr_pname_of_binop b in let gvars1, asrtl1, comp_expr1 = compile_lexpr e1 in @@ -227,7 +234,29 @@ let rec compile_lexpr ?(fname = "main") (lexpr : WLExpr.t) : let gvars, asrtsl, comp_exprs = list_split_3 (List.map compile_lexpr l) in - (List.concat gvars, List.concat asrtsl, Expr.ESet comp_exprs)) + (List.concat gvars, List.concat asrtsl, Expr.ESet comp_exprs) + | LConstructorApp (n, l) -> + let gvars, asrtsl, comp_exprs = + list_split_3 (List.map compile_lexpr l) + in + ( List.concat gvars, + List.concat asrtsl, + Expr.ConstructorApp (n, comp_exprs) ) + | LPureFunApp (n, l) -> + let gvars, asrtsl, comp_exprs = + list_split_3 (List.map compile_lexpr l) + in + (List.concat gvars, List.concat asrtsl, Expr.FuncApp (n, comp_exprs)) + | LCases (le, cs) -> + let compile_case { constructor; binders; lexpr } = + let gvars, asrtsl, comp_lexpr = compile_lexpr lexpr in + (gvars, asrtsl, (constructor, binders, comp_lexpr)) + in + let gvar, asrtl, comp_le = compile_lexpr le in + let gvars, asrtsl, comp_cs = list_split_3 (List.map compile_case cs) in + ( List.concat (gvar :: gvars), + List.concat (asrtl :: asrtsl), + Expr.Cases (comp_le, comp_cs) )) (* compile_lassert returns the compiled assertion + the list of generated existentials *) let rec compile_lassert ?(fname = "main") asser : string list * Asrt.t = @@ -403,7 +432,7 @@ let rec compile_lcmd ?(fname = "main") lcmd = (None, LCmd.SL (SLCmd.SepAssert (comp_la, exs @ lb))) | Invariant _ -> failwith "Invariant is not before a loop." -let compile_inv_and_while ~fname ~while_stmt ~invariant = +let compile_inv_and_while ~proc_name:fname ~while_stmt ~invariant = (* FIXME: Variables that are in the invariant but not existential might be wrong. *) let loopretvar = "loopretvar__" in let gen_str = Generators.gen_str fname in @@ -593,7 +622,9 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl = | { snode = Logic invariant; _ } :: while_stmt :: rest when WLCmd.is_inv invariant && WStmt.is_while while_stmt && !Gillian.Utils.Config.current_exec_mode = Verification -> - let cmds, fct = compile_inv_and_while ~fname ~while_stmt ~invariant in + let cmds, fct = + compile_inv_and_while ~proc_name:fname ~while_stmt ~invariant + in let comp_rest, new_functions = compile_list rest in (cmds @ comp_rest, fct :: new_functions) | { snode = While _; _ } :: _ @@ -925,6 +956,31 @@ let compile_pred filepath pred = pred_nounfold = pred.pred_nounfold; } +let compile_pure_fun + filepath + WPureFun. + { pure_fun_name; pure_fun_params; pure_fun_definition; pure_fun_loc } = + let types = WType.infer_types_pure_fun pure_fun_params pure_fun_definition in + let get_wisl_type x = (x, WType.of_variable x types) in + let param_wisl_types = + List.map (fun (x, _) -> get_wisl_type x) pure_fun_params + in + let get_gil_type (x, t) = (x, Option.join (Option.map compile_type t)) in + let comp_func_params = List.map get_gil_type param_wisl_types in + let _, _, comp_func_def = + compile_lexpr ~is_pure_fun_def:true pure_fun_definition + in + let comp_func_loc = Some (CodeLoc.to_location pure_fun_loc) in + Func. + { + func_name = pure_fun_name; + func_source_path = Some filepath; + func_loc = comp_func_loc; + func_num_params = List.length comp_func_params; + func_params = comp_func_params; + func_definition = comp_func_def; + } + let rec compile_function filepath WFun.{ name; params; body; spec; return_expr; is_loop_body; _ } = @@ -1090,7 +1146,47 @@ let compile_lemma lemma_existentials; } -let compile ~filepath WProg.{ context; predicates; lemmas } = +let compile_constructor + filepath + WConstructor. + { + constructor_name; + constructor_fields; + constructor_loc; + constructor_datatype; + _; + } = + let comp_fields = List.map compile_type constructor_fields in + let constructor_loc = Some (CodeLoc.to_location constructor_loc) in + let constructor_num_fields = List.length comp_fields in + Constructor. + { + constructor_name; + constructor_source_path = Some filepath; + constructor_loc; + constructor_num_fields; + constructor_fields = comp_fields; + constructor_datatype; + } + +let compile_datatype + filepath + WDatatype.{ datatype_name; datatype_constructors; datatype_loc; _ } = + let comp_constructors = + List.map (compile_constructor filepath) datatype_constructors + in + let datatype_loc = Some (CodeLoc.to_location datatype_loc) in + Datatype. + { + datatype_name; + datatype_source_path = Some filepath; + datatype_loc; + datatype_constructors = comp_constructors; + } + +let compile + ~filepath + WProg.{ context; predicates; lemmas; datatypes; pure_functions } = (* stuff useful to build hashtables *) let make_hashtbl get_name deflist = let hashtbl = Hashtbl.create (List.length deflist) in @@ -1102,6 +1198,8 @@ let compile ~filepath WProg.{ context; predicates; lemmas } = let get_proc_name proc = proc.Proc.proc_name in let get_pred_name pred = pred.Pred.pred_name in let get_lemma_name lemma = lemma.Lemma.lemma_name in + let get_func_name func = func.Func.func_name in + let get_datatype_name datatype = datatype.Datatype.datatype_name in (* compile everything *) let comp_context = List.map (compile_function filepath) context in let comp_preds = List.map (compile_pred filepath) predicates in @@ -1110,10 +1208,14 @@ let compile ~filepath WProg.{ context; predicates; lemmas } = (fun lemma -> compile_lemma filepath (preprocess_lemma lemma)) lemmas in + let comp_funcs = List.map (compile_pure_fun filepath) pure_functions in + let comp_datatypes = List.map (compile_datatype filepath) datatypes in (* build the hashtables *) let gil_procs = make_hashtbl get_proc_name (List.concat comp_context) in let gil_preds = make_hashtbl get_pred_name comp_preds in let gil_lemmas = make_hashtbl get_lemma_name comp_lemmas in + let gil_funcs = make_hashtbl get_func_name comp_funcs in + let gil_datatypes = make_hashtbl get_datatype_name comp_datatypes in let proc_names = Hashtbl.fold (fun s _ l -> s :: l) gil_procs [] in let bi_specs = Hashtbl.create 1 in if Gillian.Utils.(Exec_mode.is_biabduction_exec !Config.current_exec_mode) @@ -1141,4 +1243,5 @@ let compile ~filepath WProg.{ context; predicates; lemmas } = ~imports:(List.map (fun imp -> (imp, false)) WislConstants.internal_imports) ~lemmas:gil_lemmas ~preds:gil_preds ~procs:gil_procs ~proc_names ~bi_specs ~only_specs:(Hashtbl.create 1) ~macros:(Hashtbl.create 1) - ~predecessors:(Hashtbl.create 1) () + ~predecessors:(Hashtbl.create 1) () (* TODO *) + ~datatypes:gil_datatypes ~funcs:gil_funcs diff --git a/wisl/lib/syntax/WConstructor.ml b/wisl/lib/syntax/WConstructor.ml new file mode 100644 index 00000000..708ea60e --- /dev/null +++ b/wisl/lib/syntax/WConstructor.ml @@ -0,0 +1,7 @@ +type t = { + constructor_name : string; + constructor_fields : WType.t list; + constructor_datatype : string; + constructor_loc : CodeLoc.t; + constructor_id : int; +} diff --git a/wisl/lib/syntax/WConstructor.mli b/wisl/lib/syntax/WConstructor.mli new file mode 100644 index 00000000..708ea60e --- /dev/null +++ b/wisl/lib/syntax/WConstructor.mli @@ -0,0 +1,7 @@ +type t = { + constructor_name : string; + constructor_fields : WType.t list; + constructor_datatype : string; + constructor_loc : CodeLoc.t; + constructor_id : int; +} diff --git a/wisl/lib/syntax/WDatatype.ml b/wisl/lib/syntax/WDatatype.ml new file mode 100644 index 00000000..6a454459 --- /dev/null +++ b/wisl/lib/syntax/WDatatype.ml @@ -0,0 +1,6 @@ +type t = { + datatype_name : string; + datatype_constructors : WConstructor.t list; + datatype_loc : CodeLoc.t; + datatype_id : int; +} diff --git a/wisl/lib/syntax/WDatatype.mli b/wisl/lib/syntax/WDatatype.mli new file mode 100644 index 00000000..6a454459 --- /dev/null +++ b/wisl/lib/syntax/WDatatype.mli @@ -0,0 +1,6 @@ +type t = { + datatype_name : string; + datatype_constructors : WConstructor.t list; + datatype_loc : CodeLoc.t; + datatype_id : int; +} diff --git a/wisl/lib/syntax/WLExpr.ml b/wisl/lib/syntax/WLExpr.ml index 161addca..54323f06 100644 --- a/wisl/lib/syntax/WLExpr.ml +++ b/wisl/lib/syntax/WLExpr.ml @@ -9,7 +9,11 @@ type tt = | LLSub of t * t * t | LEList of t list | LESet of t list + | LPureFunApp of string * t list (* Pure function application *) + | LConstructorApp of string * t list (* Constructor application *) + | LCases of t * case list +and case = { constructor : string; binders : string list; lexpr : t } and t = { wleid : int; wleloc : CodeLoc.t; wlenode : tt } let get le = le.wlenode @@ -60,6 +64,7 @@ let rec get_by_id id lexpr = | LUnOp (_, lep) -> getter lep | LEList lel -> list_visitor lel | LESet lel -> list_visitor lel + | LPureFunApp (_, lel) | LConstructorApp (_, lel) -> list_visitor lel | _ -> `None in let self_or_none = if get_id lexpr = id then `WLExpr lexpr else `None in @@ -83,6 +88,26 @@ let rec pp fmt lexpr = | LESet lel -> WPrettyUtils.pp_list ~pre:(format_of_string "@[-{") ~suf:(format_of_string "}-@]") pp fmt lel + | LPureFunApp (name, lel) -> + Format.fprintf fmt "@[%s" name; + WPrettyUtils.pp_list ~pre:(format_of_string "(") + ~suf:(format_of_string ")@]") ~empty:(format_of_string "@]") pp fmt lel + | LConstructorApp (name, lel) -> + Format.fprintf fmt "@['%s" name; + WPrettyUtils.pp_list ~pre:(format_of_string "(") + ~suf:(format_of_string ")@]") ~empty:(format_of_string "@]") pp fmt lel + | LCases (le, cs) -> + Format.fprintf fmt "@[case %a {@," pp le; + List.iter + (fun { constructor; binders; lexpr } -> + Format.fprintf fmt " %s" constructor; + WPrettyUtils.pp_list ~pre:(format_of_string "(") + ~suf:(format_of_string ")") ~empty:(format_of_string "") + (fun fmt s -> Format.fprintf fmt "%s" s) + fmt binders; + Format.fprintf fmt " -> %a;@," pp lexpr) + cs; + Format.fprintf fmt "}@]" let str = Format.asprintf "%a" pp @@ -99,6 +124,11 @@ let rec substitution (subst : (string, tt) Hashtbl.t) (e : t) : t = | LLSub (e1, e2, e3) -> LLSub (f e1, f e2, f e3) | LEList le -> LEList (List.map f le) | LESet le -> LESet (List.map f le) + | LPureFunApp (name, le) -> LPureFunApp (name, List.map f le) + | LConstructorApp (name, le) -> LConstructorApp (name, List.map f le) + | LCases (e, cs) -> + let cs = List.map (fun c -> { c with lexpr = f c.lexpr }) cs in + LCases (e, cs) in { wleid; wleloc; wlenode } diff --git a/wisl/lib/syntax/WLExpr.mli b/wisl/lib/syntax/WLExpr.mli index f485357e..751b0b61 100644 --- a/wisl/lib/syntax/WLExpr.mli +++ b/wisl/lib/syntax/WLExpr.mli @@ -7,7 +7,11 @@ type tt = | LLSub of t * t * t | LEList of t list | LESet of t list + | LPureFunApp of string * t list + | LConstructorApp of string * t list + | LCases of t * case list +and case = { constructor : string; binders : string list; lexpr : t } and t val get : t -> tt diff --git a/wisl/lib/syntax/WProg.ml b/wisl/lib/syntax/WProg.ml index 461e5d53..35711572 100644 --- a/wisl/lib/syntax/WProg.ml +++ b/wisl/lib/syntax/WProg.ml @@ -4,6 +4,8 @@ type t = { context : WFun.t list; predicates : WPred.t list; lemmas : WLemma.t list; + datatypes : WDatatype.t list; + pure_functions : WPureFun.t list; } let get_context p = p.context diff --git a/wisl/lib/syntax/WProg.mli b/wisl/lib/syntax/WProg.mli index 92353173..aa6539ce 100644 --- a/wisl/lib/syntax/WProg.mli +++ b/wisl/lib/syntax/WProg.mli @@ -2,6 +2,8 @@ type t = { context : WFun.t list; predicates : WPred.t list; lemmas : WLemma.t list; + datatypes : WDatatype.t list; + pure_functions : WPureFun.t list; } val get_context : t -> WFun.t list diff --git a/wisl/lib/syntax/WPureFun.ml b/wisl/lib/syntax/WPureFun.ml new file mode 100644 index 00000000..4d95649b --- /dev/null +++ b/wisl/lib/syntax/WPureFun.ml @@ -0,0 +1,6 @@ +type t = { + pure_fun_name : string; + pure_fun_params : (string * WType.t option) list; + pure_fun_definition : WLExpr.t; + pure_fun_loc : CodeLoc.t; +} diff --git a/wisl/lib/syntax/WPureFun.mli b/wisl/lib/syntax/WPureFun.mli new file mode 100644 index 00000000..4d95649b --- /dev/null +++ b/wisl/lib/syntax/WPureFun.mli @@ -0,0 +1,6 @@ +type t = { + pure_fun_name : string; + pure_fun_params : (string * WType.t option) list; + pure_fun_definition : WLExpr.t; + pure_fun_loc : CodeLoc.t; +} diff --git a/wisl/lib/syntax/WType.ml b/wisl/lib/syntax/WType.ml index 16a330b9..27a12c68 100644 --- a/wisl/lib/syntax/WType.ml +++ b/wisl/lib/syntax/WType.ml @@ -8,6 +8,7 @@ type t = | WInt | WAny | WSet + | WDatatype of string (** Are types t1 and t2 compatible *) let compatible t1 t2 = @@ -36,6 +37,7 @@ let pp fmt t = | WInt -> s "Int" | WAny -> s "Any" | WSet -> s "Set" + | WDatatype t -> s t let to_gil = function | WList -> Gil_syntax.Type.ListType @@ -156,6 +158,14 @@ let rec infer_logic_expr knownp lexpr = TypeMap.add bare_lexpr WList (List.fold_left infer_logic_expr knownp lel) | LESet lel -> TypeMap.add bare_lexpr WSet (List.fold_left infer_logic_expr knownp lel) + | LPureFunApp (_, lel) -> List.fold_left infer_logic_expr knownp lel + | LConstructorApp (n, lel) -> + TypeMap.add bare_lexpr (WDatatype n) + (List.fold_left infer_logic_expr knownp lel) + | LCases (le, cs) -> + let lel = List.map (fun (c : case) -> c.lexpr) cs in + let inferred = infer_logic_expr knownp le in + List.fold_left infer_logic_expr inferred lel (** Single step of inference for that gets a TypeMap from a single assertion *) let rec infer_single_assert_step asser known = @@ -216,3 +226,22 @@ let infer_types_pred (params : (string * t option) list) assert_list = TypeMap.merge join_params_and_asserts infers_on_params infers_on_asserts in result + +let infer_types_pure_fun (params : (string * t option) list) pure_fun_def = + let join _ param_t inferred_t = + match (param_t, inferred_t) with + | Some param_t, Some inferred_t when param_t = inferred_t -> Some param_t + | Some param_t, None when param_t <> WAny -> Some param_t + | None, Some inferred_t when inferred_t <> WAny -> Some inferred_t + | _ -> None + in + let infers_on_params = + List.fold_left + (fun (map : 'a TypeMap.t) (x, ot) -> + match ot with + | None -> map + | Some t -> TypeMap.add (PVar x) t map) + TypeMap.empty params + in + let infer_on_def = infer_logic_expr TypeMap.empty pure_fun_def in + TypeMap.merge join infers_on_params infer_on_def diff --git a/wisl/lib/syntax/WType.mli b/wisl/lib/syntax/WType.mli index 6f66fc14..1ba7dd84 100644 --- a/wisl/lib/syntax/WType.mli +++ b/wisl/lib/syntax/WType.mli @@ -1,4 +1,13 @@ -type t = WList | WNull | WBool | WString | WPtr | WInt | WAny | WSet +type t = + | WList + | WNull + | WBool + | WString + | WPtr + | WInt + | WAny + | WSet + | WDatatype of string val compatible : t -> t -> bool val strongest : t -> t -> t @@ -16,3 +25,5 @@ val of_variable : string -> t TypeMap.t -> t option val infer_types_pred : (string * t option) list -> WLAssert.t list -> t TypeMap.t + +val infer_types_pure_fun : (string * t option) list -> WLExpr.t -> t TypeMap.t