diff --git a/Gillian-C/lib/gilgen.ml b/Gillian-C/lib/gilgen.ml index 3473298d1..40ada8573 100644 --- a/Gillian-C/lib/gilgen.ml +++ b/Gillian-C/lib/gilgen.ml @@ -1048,6 +1048,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 2aabca77c..2343b1328 100644 --- a/Gillian-JS/lib/Compiler/JSIL2GIL.ml +++ b/Gillian-JS/lib/Compiler/JSIL2GIL.ml @@ -515,6 +515,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 000000000..3f34ab7f1 --- /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 000000000..09e9b05ee --- /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 f460ec0a0..0486e76f4 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 @@ -378,6 +381,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 @@ -415,6 +430,25 @@ let pp_custom ~pp ft = Fmt.pf ft "(forall %a . %a)" (Fmt.list ~sep:Fmt.comma pp_var_with_type) bt pp e + | ConstructorApp (n, ll) -> + Fmt.pf ft "'%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll + | FuncApp (n, ll) -> Fmt.pf ft "%s(%a)" n (Fmt.list ~sep:Fmt.comma pp) ll + | Cases (scrutinee, branches) -> + Fmt.pf ft "@[case %a {@," pp scrutinee; + List.iteri + (fun i (constructor, binders, expr) -> + Fmt.pf ft " %s" constructor; + (match binders with + | [] -> () + | _ -> + Fmt.pf ft "("; + Fmt.pf ft "%a" (Fmt.list ~sep:(Fmt.any ", ") Fmt.string) binders; + Fmt.pf ft ")"); + Fmt.pf ft " -> %a" pp expr; + if i < List.length branches - 1 then Fmt.pf ft ";@," + else Fmt.pf ft "@,") + branches; + Fmt.pf ft "}@]" let rec pp ft t = pp_custom ~pp ft t @@ -479,6 +513,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 000000000..70db2b3e9 --- /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 ad6d23758..5680990ed 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 @@ -17,6 +20,7 @@ module NOp = NOp module Pred = Pred module Proc = Proc module Prog = Prog +module Prog_env = Prog_env module SLCmd = SLCmd module Spec = Spec module Type = Type diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index c598f4a37..d6794552c 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} @@ -773,6 +777,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 *) @@ -1024,6 +1061,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; (** Procedures *) @@ -1039,6 +1078,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 -> @@ -1055,6 +1096,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 -> @@ -1069,6 +1112,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 -> @@ -1180,6 +1225,45 @@ module Prog : sig val make_callgraph : ('a, 'b) t -> Call_graph.t end +module Prog_env : sig + module Datatype_env : sig + type t + + val make : ('a, 'b) Prog.t -> t + val make' : (string, Datatype.t) Hashtbl.t -> t + val using : t -> (unit -> 'a) -> 'a + val using_prog : ('a, 'b) Prog.t -> (unit -> 'c) -> 'c + val get_datatype : string -> Datatype.t option + val get_datatype_exn : string -> Datatype.t + val get_datatypes : unit -> Datatype.t Containers.StringMap.t + val get_datatype_cycle : string -> SS.t + val get_constructor : string -> Constructor.t option + val get_constructor_exn : string -> Constructor.t + val get_constructor_type : string -> Type.t option + val get_constructor_type_exn : string -> Type.t + val get_constructor_field_types : string -> Type.t option list option + val get_constructor_field_types_exn : string -> Type.t option list + end + + module Function_env : sig + type t + + val make' : (string, Func.t) Hashtbl.t -> t + val make : ('a, 'b) Prog.t -> t + val using : t -> (unit -> 'a) -> 'a + val using_prog : ('a, 'b) Prog.t -> (unit -> 'c) -> 'c + val get_function : string -> Func.t option + val get_function_param_types : string -> Type.t option list option + val get_functions : unit -> Func.t Containers.StringMap.t + end + + type t + + val make : ('a, 'b) Prog.t -> t + val using : t -> (unit -> 'a) -> 'a + val using_prog : ('a, 'b) Prog.t -> (unit -> 'c) -> 'c +end + (** @canonical Gillian.Gil_syntax.Visitors *) module Visitors : sig (** Classes for traversing the GIL AST *) @@ -1218,8 +1302,16 @@ module Visitors : sig ; visit_Call : 'c -> 'f Cmd.t -> Cmd.function_call -> 'f 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 -> @@ -1245,6 +1337,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 @@ -1264,6 +1357,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 -> @@ -1415,8 +1509,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 @@ -1469,9 +1566,16 @@ module Visitors : sig 'c -> 'f Cmd.t -> Cmd.function_call -> 'f option -> '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 @@ -1492,6 +1596,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 @@ -1512,6 +1617,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 -> @@ -1676,8 +1783,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 @@ -1755,8 +1865,11 @@ module Visitors : sig ; visit_Bug : 'c -> 'f ; visit_Call : 'c -> Cmd.function_call -> 'g 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 : @@ -1780,6 +1893,7 @@ module Visitors : sig ; visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> 'f ; visit_function_call : 'c -> Cmd.function_call -> '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 @@ -1872,6 +1986,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 @@ -1921,8 +2036,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 @@ -1968,8 +2086,13 @@ module Visitors : sig method visit_Bug : 'c -> 'f method visit_Call : 'c -> Cmd.function_call -> 'g option -> '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 @@ -1997,6 +2120,7 @@ module Visitors : sig method visit_ForAll : 'c -> (string * Type.t option) list -> Expr.t -> 'f method visit_function_call : 'c -> Cmd.function_call -> '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 @@ -2089,6 +2213,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 @@ -2136,8 +2261,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 @@ -2185,8 +2313,11 @@ module Visitors : sig ; visit_Bug : 'c -> unit ; visit_Call : 'c -> Cmd.function_call -> 'f 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 @@ -2216,6 +2347,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 @@ -2307,6 +2439,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 @@ -2351,8 +2484,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 @@ -2397,8 +2533,13 @@ module Visitors : sig method visit_Bug : 'c -> unit method visit_Call : 'c -> Cmd.function_call -> 'f option -> 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 @@ -2432,6 +2573,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 @@ -2525,6 +2667,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 @@ -2579,8 +2722,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 bf7d85882..071e4f2e2 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/Prog_env.ml b/GillianCore/GIL_Syntax/Prog_env.ml new file mode 100644 index 000000000..d2aafe529 --- /dev/null +++ b/GillianCore/GIL_Syntax/Prog_env.ml @@ -0,0 +1,157 @@ +open Syntaxes.Option +module StringMap = Containers.StringMap + +module Datatype_env = struct + type t = { + datatypes : Datatype.t StringMap.t; + constructors : Constructor.t StringMap.t; + cycles : SS.t StringMap.t; + } + + type _ Effect.t += Get_datatype_env : t Effect.t + + let get () = Effect.perform Get_datatype_env + + let check_constructor_param datatype_tbl (c : Constructor.t) = + let open Type in + function + | Some (DatatypeType n) -> + if not (Hashtbl.mem datatype_tbl n) then + let msg = + Fmt.str "Unknown datatype %s in definition of constructor %s" n + c.constructor_name + in + raise + (Gillian_result.Exc.compilation_error ?loc:c.constructor_loc msg) + | _ -> () + + let check_constructor datatype_tbl cs (c : Constructor.t) = + let () = + if StringMap.mem c.constructor_name cs then + let msg = "Duplicate constructor name " ^ c.constructor_name in + raise (Gillian_result.Exc.compilation_error ?loc:c.constructor_loc msg) + in + List.iter (check_constructor_param datatype_tbl c) c.constructor_fields + + let find_cycles datatype_tbl = + let get_edge = + Hashtbl.memoize @@ fun name -> + let (d : Datatype.t) = Hashtbl.find datatype_tbl name in + d.datatype_constructors + |> List.concat_map @@ fun (c : Constructor.t) -> + c.constructor_fields + |> List.filter_map @@ function + | Some (Type.DatatypeType name') -> Some name' + | _ -> None + in + let iter_vertices f = Hashtbl.iter (fun k _ -> f k) datatype_tbl in + let cycle_lists = Tarjan.tarjan iter_vertices get_edge in + List.fold_left + (fun cycles cycle_list -> + let current_cycle = SS.of_list cycle_list in + SS.fold + (fun v cycles -> StringMap.add v current_cycle cycles) + current_cycle cycles) + StringMap.empty cycle_lists + + (* Initialises the datatype env, ensuring datatype definitions are well formed. *) + let make' datatype_tbl = + let ds = ref StringMap.empty in + let cs = ref StringMap.empty in + let () = + datatype_tbl + |> Hashtbl.iter @@ fun name (d : Datatype.t) -> + ds := StringMap.add name d !ds; + d.datatype_constructors + |> List.iter @@ fun c -> + check_constructor datatype_tbl !cs c; + cs := StringMap.add c.constructor_name c !cs + in + let cycles = find_cycles datatype_tbl in + { datatypes = !ds; constructors = !cs; cycles } + + let make prog = make' prog.Prog.datatypes + + let using (t : t) f = + match f () with + | x -> x + | effect Get_datatype_env, k -> Effect.Deep.continue k t + + let using_prog prog f = using (make prog) f + let get_datatypes () = (get ()).datatypes + let get_datatype name = StringMap.find_opt name (get_datatypes ()) + + let get_datatype_exn name = + match get_datatype name with + | Some d -> d + | None -> + Fmt.failwith "Datatype_env.get_datatype_exn: datatype %s not found" name + + let get_datatype_cycle name = + Option.value ~default:SS.empty (StringMap.find_opt name (get ()).cycles) + + let get_constructor cname = StringMap.find_opt cname (get ()).constructors + + let get_constructor_exn cname = + match get_constructor cname with + | Some c -> c + | None -> + Fmt.failwith + "Datatype_env.get_constructor_exn: constructor %s not found" cname + + let get_constructor_type cname : Type.t option = + let+ c = get_constructor cname in + Type.DatatypeType c.constructor_datatype + + let get_constructor_type_exn cname : Type.t = + match get_constructor_type cname with + | Some t -> t + | None -> + Fmt.failwith + "Datatype_env.get_constructor_type_exn: constructor %s not found." + cname + + let get_constructor_field_types cname : Type.t option list option = + let+ c = get_constructor cname in + c.constructor_fields + + let get_constructor_field_types_exn cname : Type.t option list = + match get_constructor_field_types cname with + | Some ts -> ts + | None -> + Fmt.failwith + "Datatype_env.get_constructor_field_types_exn: constructor %s not \ + found." + cname +end + +module Function_env = struct + type t = Func.t StringMap.t + type _ Effect.t += Get_function_env : t Effect.t + + let get () = Effect.perform Get_function_env + let make' func_tbl = Hashtbl.fold StringMap.add func_tbl StringMap.empty + let make prog = make' prog.Prog.funcs + + let using (t : t) f = + match f () with + | x -> x + | effect Get_function_env, k -> Effect.Deep.continue k t + + let using_prog prog f = using (make prog) f + let get_function fname = StringMap.find_opt fname (get ()) + + let get_function_param_types fname = + let+ func = get_function fname in + List.map snd func.func_params + + let get_functions () = get () +end + +type t = Datatype_env.t * Function_env.t + +let make prog = (Datatype_env.make prog, Function_env.make prog) +let using (dt, fn) f = Datatype_env.using dt (fun () -> Function_env.using fn f) + +let using_prog prog f = + Datatype_env.using_prog prog (fun () -> Function_env.using_prog prog f) diff --git a/GillianCore/GIL_Syntax/Type.ml b/GillianCore/GIL_Syntax/Type.ml index 6d452bb53..79c10b95d 100644 --- a/GillianCore/GIL_Syntax/Type.ml +++ b/GillianCore/GIL_Syntax/Type.ml @@ -13,6 +13,7 @@ type t = TypeDef__.typ = | ListType (** Type of lists *) | TypeType (** Type of types *) | SetType (** Type of sets *) + | DatatypeType of string (** User-defined datatypes *) [@@deriving yojson, eq, ord, show] (** Print *) @@ -30,6 +31,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 0dd12cb12..579a83ac7 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 @@ -247,6 +251,31 @@ and lemma = { lemma_location : location option; } +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/command_line/verification_console.ml b/GillianCore/command_line/verification_console.ml index cafe8ef3e..d1cc4f414 100644 --- a/GillianCore/command_line/verification_console.ml +++ b/GillianCore/command_line/verification_console.ml @@ -119,6 +119,7 @@ module Make (Prog.pp_indexed ?pp_annot:None) prog) in + Prog_env.using_prog prog @@ fun () -> Verification.verify_prog ~init_data prog incremental source_files_opt let verify_once diff --git a/GillianCore/command_line/wpst_console.ml b/GillianCore/command_line/wpst_console.ml index 1412118b9..de8eeb681 100644 --- a/GillianCore/command_line/wpst_console.ml +++ b/GillianCore/command_line/wpst_console.ml @@ -217,6 +217,7 @@ module Make in Printf.printf "Compilation time: %fs\n" (Unix.gettimeofday () -. t); let () = L.normal (fun m -> m "*** Stage 3: Symbolic Execution.\n") in + Prog_env.using_prog prog @@ fun () -> let prog' = MP.init_prog prog in run prog' init_data incremental source_files_opt diff --git a/GillianCore/debugging/adapter/state_initialized.ml b/GillianCore/debugging/adapter/state_initialized.ml index 72af41099..f4f3007a2 100644 --- a/GillianCore/debugging/adapter/state_initialized.ml +++ b/GillianCore/debugging/adapter/state_initialized.ml @@ -17,18 +17,13 @@ module Make (Debugger : Debugger.S) = struct (module Launch_command) (fun (launch_args : Launch_command.Arguments.t) -> prevent_reenter (); - let r = - try Debugger.launch launch_args.program launch_args.procedure_name - with e -> Gillian_result.internal_error (Printexc.to_string e) - in - let%lwt () = - match r with - | Ok dbg -> - Lwt.wakeup_later resolver (launch_args, dbg); - Lwt.return_unit - | Error e -> raise (Gillian_result.Exc.Gillian_error e) - in - Lwt.return_unit); + match + Debugger.launch launch_args.program launch_args.procedure_name + with + | Ok dbg -> + Lwt.wakeup_later resolver (launch_args, dbg); + Lwt.return_unit + | Error e -> raise (Gillian_result.Exc.Gillian_error e)); DL.set_rpc_command_handler rpc ~name:"Attach" (module Attach_command) (fun _ -> diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml index f09b732b4..24011b42c 100644 --- a/GillianCore/debugging/debugger/base_debugger.ml +++ b/GillianCore/debugging/debugger/base_debugger.ml @@ -69,6 +69,7 @@ struct source_file : string; source_files : SourceFiles.t option; prog : Verification.prog_t; + prog_env : Prog_env.t; tl_ast : tl_ast option; main_proc_name : string; report_state_base : L.Report_state.t; @@ -159,6 +160,8 @@ struct type debug_state = debug_state_ext base_debug_state type t = (proc, debug_state) state + let with_prog_env state = Prog_env.using state.debug_state.prog_env + let get_root_proc_name_of_id id = let content, type_ = L.Log_queryer.get_report id @@ -622,6 +625,7 @@ struct `Assoc status let get_map_update state = + with_prog_env state @@ fun () -> let nodes = get_changed_nodes ~clear:true state in let roots = get_roots state in let current_steps = Some (get_current_steps state) in @@ -629,6 +633,7 @@ struct Map_update_event_body.make ~nodes ~roots ~current_steps ~ext () let get_full_map state = + with_prog_env state @@ fun () -> let nodes = get_all_nodes state in let roots = get_roots state in let current_steps = Some (get_current_steps state) in @@ -672,7 +677,8 @@ struct } [@@deriving yojson] - let dump_state ({ debug_state; procs } : t) : Yojson.Safe.t = + let dump_state ({ debug_state; procs } as state) : Yojson.Safe.t = + with_prog_env state @@ fun () -> let procs = Hashtbl.fold (fun proc_name (proc : proc) acc -> @@ -1074,6 +1080,7 @@ struct stop_reason let lifter_call_with_id ?interaction state lifter_func = + with_prog_env state @@ fun () -> let proc_state = get_proc_state_exn state in let { cur_report_id; lifter_state; _ } = proc_state in let id = Option.get cur_report_id in @@ -1090,6 +1097,7 @@ struct lifter_call_with_id ~interaction:Step_out state Lifter.step_out let step_specific case id state = + with_prog_env state @@ fun () -> let proc_state = get_proc_state_exn ~cmd_id:id state in let { lifter_state; _ } = proc_state in let f () = Lifter.step_branch lifter_state id case in @@ -1111,6 +1119,7 @@ struct Lifter.continue_back let jump id state = + with_prog_env state @@ fun () -> let cmd_id, matches = L.Log_queryer.resolve_command_and_matches id in let** proc_state = get_proc_state ~cmd_id state in let++ () = jump_state_to_id cmd_id state.debug_state proc_state in @@ -1156,6 +1165,7 @@ struct Lifter.init_exn ~proc_name ~all_procs:proc_names tl_ast prog let f proc_name ~entrypoint state = + with_prog_env state @@ fun () -> let { debug_state; _ } = state in let report_state = L.Report_state.clone debug_state.report_state_base in report_state @@ -1207,6 +1217,7 @@ struct process_files ~proc_name ~outfile ~no_unfold ~already_compiled [ file_name ] in + let prog_env = Prog_env.make prog in let proc_names = prog.procs |> Hashtbl.to_seq |> Seq.filter_map (fun (name, proc) -> @@ -1217,8 +1228,8 @@ struct let cfg = let make ext = make_base_debug_state ~source_file:file_name ?source_files ~prog - ?tl_ast ~main_proc_name:proc_name ~report_state_base ~init_data - ~proc_names ~cur_proc:(proc_name, 0) ~ext () + ~prog_env ?tl_ast ~main_proc_name:proc_name ~report_state_base + ~init_data ~proc_names ~cur_proc:(proc_name, 0) ~ext () in let ext = Debugger_impl.init (make ()) in make ext @@ -1247,6 +1258,7 @@ struct let launch = Launch.f let start_proc proc_name state = + with_prog_env state @@ fun () -> let { debug_state; procs } = state in let++ proc_states, stop_reason = launch_proc proc_name ~entrypoint:proc_name state @@ -1256,12 +1268,14 @@ struct stop_reason let terminate state = + with_prog_env state @@ fun () -> L.Report_state.(activate global_state); Verification.postprocess_files state.debug_state.source_files; if !Config.stats then L.Statistics.print_statistics (); Usage_logs.Debug.stop () let get_frames state = + with_prog_env state @@ fun () -> let { frames; _ } = get_proc_state_exn state in frames @@ -1277,15 +1291,18 @@ struct proc_state.variables <- Some vs; vs - let get_scopes state = fst (get_scopes_and_variables state) + let get_scopes state = + with_prog_env state @@ fun () -> fst (get_scopes_and_variables state) let get_variables (var_ref : int) state : Variable.t list = + with_prog_env state @@ fun () -> let variables = snd (get_scopes_and_variables state) in match Hashtbl.find_opt variables var_ref with | None -> [] | Some vars -> vars let get_exception_info state = + with_prog_env state @@ fun () -> let proc_state = get_proc_state_exn state in let error = List.hd proc_state.errors in let non_mem_exception_info = @@ -1302,6 +1319,7 @@ struct | _ -> non_mem_exception_info let set_breakpoints source bp_list state = + with_prog_env state @@ fun () -> match source with (* We can't set the breakpoints if we do not know the source file *) | None -> () diff --git a/GillianCore/debugging/log/debugger_log.ml b/GillianCore/debugging/log/debugger_log.ml index ae81ac191..55a98e242 100644 --- a/GillianCore/debugging/log/debugger_log.ml +++ b/GillianCore/debugging/log/debugger_log.ml @@ -156,5 +156,5 @@ let try' ~name f x = Lwt.reraise err let set_rpc_command_handler rpc ?name ?(catchall = true) module_ f = - let f x = if catchall then try' ~name f x else f x in + let f = if catchall then try' ~name f else f in Debug_rpc.set_command_handler rpc module_ f diff --git a/GillianCore/debugging/log/debugger_log.mli b/GillianCore/debugging/log/debugger_log.mli index feadfaa38..0c80dab37 100644 --- a/GillianCore/debugging/log/debugger_log.mli +++ b/GillianCore/debugging/log/debugger_log.mli @@ -8,6 +8,8 @@ module Public : sig type t = (string * Yojson.Safe.t) list end + exception FailureJson of string * JsonMap.t + (** Sends a log message to the debugger frontend via a custom event. Optionally includes some accompanying JSON. diff --git a/GillianCore/engine/Abstraction/LogicPreprocessing.ml b/GillianCore/engine/Abstraction/LogicPreprocessing.ml index a852f82f1..6b03679ee 100644 --- a/GillianCore/engine/Abstraction/LogicPreprocessing.ml +++ b/GillianCore/engine/Abstraction/LogicPreprocessing.ml @@ -673,42 +673,41 @@ let add_closing_tokens preds = guarded_predicates let preprocess (prog : ('a, int) Prog.t) (unfold : bool) : ('a, int) Prog.t = - let f (prog : ('a, int) Prog.t) unfold = - let procs = prog.procs in - let preds = prog.preds in - let lemmas = prog.lemmas in - let onlyspecs = prog.only_specs in - - let procs', preds', lemmas' = explicit_param_types procs preds lemmas in - - let () = - Hashtbl.filter_map_inplace - (fun _ lemma -> - let lemma = Lemma.add_param_bindings lemma in - Some lemma) - lemmas' - in + L.Phase.with_normal ~title:"Logic preprocessing" @@ fun () -> + Prog_env.using_prog prog @@ fun () -> + let procs = prog.procs in + let preds = prog.preds in + let lemmas = prog.lemmas in + let onlyspecs = prog.only_specs in + + let procs', preds', lemmas' = explicit_param_types procs preds lemmas in + + let () = + Hashtbl.filter_map_inplace + (fun _ lemma -> + let lemma = Lemma.add_param_bindings lemma in + Some lemma) + lemmas' + in - let preds'', procs'', bi_specs, lemmas'', onlyspecs' = - match unfold with - | false -> (preds', procs', prog.bi_specs, lemmas', onlyspecs) - | true -> - let preds'', rec_info = unfold_preds preds' in - let procs'' = unfold_procs preds'' rec_info procs' in - let bi_specs = unfold_bispecs preds'' rec_info prog.bi_specs in - let lemmas'' = unfold_lemmas preds'' rec_info lemmas' in - let onlyspecs' = unfold_specs preds'' rec_info onlyspecs in - (* create_partial_matches procs''; *) - (preds'', procs'', bi_specs, lemmas'', onlyspecs') - in - add_closing_tokens preds''; - { - prog with - preds = preds''; - procs = procs''; - bi_specs; - lemmas = lemmas''; - only_specs = onlyspecs'; - } + let preds'', procs'', bi_specs, lemmas'', onlyspecs' = + match unfold with + | false -> (preds', procs', prog.bi_specs, lemmas', onlyspecs) + | true -> + let preds'', rec_info = unfold_preds preds' in + let procs'' = unfold_procs preds'' rec_info procs' in + let bi_specs = unfold_bispecs preds'' rec_info prog.bi_specs in + let lemmas'' = unfold_lemmas preds'' rec_info lemmas' in + let onlyspecs' = unfold_specs preds'' rec_info onlyspecs in + (* create_partial_matches procs''; *) + (preds'', procs'', bi_specs, lemmas'', onlyspecs') in - L.Phase.with_normal ~title:"Logic preprocessing" (fun () -> f prog unfold) + add_closing_tokens preds''; + { + prog with + preds = preds''; + procs = procs''; + bi_specs; + lemmas = lemmas''; + only_specs = onlyspecs'; + } diff --git a/GillianCore/engine/Abstraction/MP.ml b/GillianCore/engine/Abstraction/MP.ml index e88a8c03f..4e0de81e8 100644 --- a/GillianCore/engine/Abstraction/MP.ml +++ b/GillianCore/engine/Abstraction/MP.ml @@ -128,8 +128,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 @@ -138,6 +137,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 @@ -167,7 +170,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 -> @@ -175,6 +179,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 @@ -314,6 +324,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)); *) @@ -466,7 +499,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 2b38e9018..45153b6cb 100644 --- a/GillianCore/engine/Abstraction/Normaliser.ml +++ b/GillianCore/engine/Abstraction/Normaliser.ml @@ -160,7 +160,7 @@ module Make (SPState : PState.S) = struct match nle1 with | Lit llit -> Lit (Type (Literal.type_of llit)) | LVar lvar -> ( - try Lit (Type (Type_env.get_unsafe gamma lvar)) + try Lit (Type (Type_env.get_exn gamma lvar)) with _ -> UnOp (TypeOf, LVar lvar) (* raise (Failure (Printf.sprintf "Logical variables always have a type, in particular: %s." lvar))) *) @@ -171,10 +171,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 Prog_env.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 @@ -224,6 +229,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/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index eb93699c6..69dc22320 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/GillianCore/engine/FOLogic/FOSolver.ml @@ -38,7 +38,8 @@ 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 gamma_tbl = Type_env.as_hashtbl gamma in + let model = Smt.check_sat fs gamma_tbl in let lvars = List.fold_left (fun ac vs -> @@ -62,7 +63,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_tbl update smt_vars; Some subst with e -> let () = @@ -200,7 +201,7 @@ let check_entailment let model = Smt.check_sat (Expr.Set.of_list (PFS.to_list formulae)) - (Type_env.as_hashtbl gamma_left) + (Type_env.as_hashtbl 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 33b24cdcb..142cc3db3 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 @@ -928,6 +932,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 ------------------------- *) @@ -1878,6 +1915,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/engine/FOLogic/typing.ml b/GillianCore/engine/FOLogic/typing.ml index b664c9e57..40822523a 100644 --- a/GillianCore/engine/FOLogic/typing.ml +++ b/GillianCore/engine/FOLogic/typing.ml @@ -1,3 +1,4 @@ +open Prog_env module L = Logging module SSubst = SVal.SESubst @@ -126,6 +127,11 @@ module Infer_types_to_gamma = struct let f' = f flag in let f = f flag gamma new_gamma in let ( = ) = Type.equal in + let check_field le = function + | Some tt -> f le tt + | None -> true + in + let check_fields = List.for_all2 check_field in match le with (* Literals are always typable *) | Lit lit -> Literal.type_of lit = tt @@ -153,6 +159,64 @@ 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) -> ( + match Datatype_env.get_constructor_field_types n with + | None -> false + | Some field_types -> + List_utils.lengths_eq field_types les + && tt = Datatype_env.get_constructor_type_exn n + && check_fields les field_types) + | FuncApp (n, les) -> ( + match Function_env.get_function_param_types n with + | None -> false + | Some field_types -> + (* Only check param types, we don't check return type of function *) + List_utils.lengths_eq field_types les + && check_fields les field_types) + | Cases (le, cs) -> + let scrutinee_type_check = + let constructor_types = + List.map (fun (c, _, _) -> Datatype_env.get_constructor_type c) cs + in + match Option_utils.all constructor_types with + | None | Some [] -> false + | Some (t :: ts) -> List.for_all (( = ) t) ts && f le t + 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 = + match Datatype_env.get_constructor_field_types c with + | Some ts when List_utils.lengths_eq ts bs -> + 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; + true + | _ -> + (* Datatype env is initialised but can't find constructor *) + false + 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 +360,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 +523,68 @@ 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 = + match Datatype_env.get_constructor_field_types n 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 + + and type_func_app gamma n les = + match Function_env.get_function_param_types n 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 + + and type_case gamma t_scrutinee (c, bs, le) = + 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_exn 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 + + 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 +615,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 @@ -492,7 +636,7 @@ let te_of_list (vt : (Expr.t * Type.t) list) : Type_env.t option = if t <> t' then raise Break | LVar x | PVar x -> if Type_env.mem result x then ( - let t' = Type_env.get_unsafe result x in + let t' = Type_env.get_exn result x in if t <> t' then raise Break) else Type_env.update result x t | _ -> ( diff --git a/GillianCore/engine/concrete_semantics/CExprEval.ml b/GillianCore/engine/concrete_semantics/CExprEval.ml index 95b0ce28c..0f974c245 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/general_semantics/eSubst.ml b/GillianCore/engine/general_semantics/eSubst.ml index add2aa033..acd982ae5 100644 --- a/GillianCore/engine/general_semantics/eSubst.ml +++ b/GillianCore/engine/general_semantics/eSubst.ml @@ -425,6 +425,18 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct 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 _ -> @@ -432,29 +444,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/general_semantics/store.ml b/GillianCore/engine/general_semantics/store.ml index e087e61e5..cf094d4f2 100644 --- a/GillianCore/engine/general_semantics/store.ml +++ b/GillianCore/engine/general_semantics/store.ml @@ -28,7 +28,7 @@ module type S = sig val get : t -> Var.t -> vt option (** Return value of a given variable or throw *) - val get_unsafe : t -> Var.t -> vt + val get_exn : t -> Var.t -> vt (** Store constructor, with a list of bindings of the form (variable, value) *) @@ -101,10 +101,10 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct @param x Target variable @raise Failure Variable not found in the store @return Value of the variable in the store *) - let get_unsafe (store : t) (v : Var.t) : vt = + let get_exn (store : t) (v : Var.t) : vt = match get store v with | Some result -> result - | None -> Fmt.failwith "Store.get_unsafe: variable %s not found in store" v + | None -> Fmt.failwith "Store.get_exn: variable %s not found in store" v (** Store update (in-place) diff --git a/GillianCore/engine/general_semantics/store.mli b/GillianCore/engine/general_semantics/store.mli index c324adaf2..c39aa2d58 100644 --- a/GillianCore/engine/general_semantics/store.mli +++ b/GillianCore/engine/general_semantics/store.mli @@ -31,7 +31,7 @@ module type S = sig val get : t -> Var.t -> vt option (** Return value of a given variable or throw *) - val get_unsafe : t -> Var.t -> vt + val get_exn : t -> Var.t -> vt (** Store constructor, with a list of bindings of the form (variable, value) *) diff --git a/GillianCore/engine/FOLogic/type_env.ml b/GillianCore/engine/logical_env/type_env.ml similarity index 94% rename from GillianCore/engine/FOLogic/type_env.ml rename to GillianCore/engine/logical_env/type_env.ml index 839979e20..31384af2c 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 @@ -29,11 +31,11 @@ let mem (x : t) (v : string) : bool = Hashtbl.mem x v let empty (x : t) : bool = Hashtbl.length x == 0 (* Type of a variable *) -let get_unsafe (x : t) (var : string) : Type.t = +let get_exn (x : t) (var : string) : Type.t = match Hashtbl.find_opt x var with | Some t -> t | None -> - raise (Failure ("Type_env.get_unsafe: variable " ^ var ^ " not found.")) + raise (Failure ("Type_env.get_exn: variable " ^ var ^ " not found.")) (* Get all matchable elements *) let matchables (x : t) : SS.t = diff --git a/GillianCore/engine/FOLogic/type_env.mli b/GillianCore/engine/logical_env/type_env.mli similarity index 87% rename from GillianCore/engine/FOLogic/type_env.mli rename to GillianCore/engine/logical_env/type_env.mli index 9e4e61476..f3321c6af 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 @@ -15,7 +18,7 @@ val filter_in_place : t -> (string -> bool) -> unit val filter_vars : t -> Containers.SS.t -> t val filter_vars_in_place : t -> Containers.SS.t -> unit val get : t -> string -> Type.t option -val get_unsafe : t -> string -> Type.t +val get_exn : t -> string -> Type.t val get_var_type_pairs : t -> (string * Type.t) Seq.t val get_vars_of_type : t -> Type.t -> string list val init : unit -> t diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index e4c69ad75..52d0ef4c8 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/GillianCore/engine/symbolic_semantics/SState.ml @@ -269,6 +269,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/engine/symbolic_semantics/SStore.mli b/GillianCore/engine/symbolic_semantics/SStore.mli index 089b75c4e..1024028d8 100644 --- a/GillianCore/engine/symbolic_semantics/SStore.mli +++ b/GillianCore/engine/symbolic_semantics/SStore.mli @@ -8,7 +8,7 @@ type t [@@deriving yojson] val copy : t -> t val domain : t -> Containers.SS.t val get : t -> Var.t -> Expr.t option -val get_unsafe : t -> Var.t -> Expr.t +val get_exn : t -> Var.t -> Expr.t val init : (Var.t * Expr.t) list -> t val mem : t -> Var.t -> bool val partition : t -> (Expr.t -> bool) -> Var.Set.t * Var.Set.t diff --git a/GillianCore/gil_parser/gil_parsing.ml b/GillianCore/gil_parser/gil_parsing.ml index de592845c..d6cf31129 100644 --- a/GillianCore/gil_parser/gil_parsing.ml +++ b/GillianCore/gil_parser/gil_parsing.ml @@ -302,9 +302,11 @@ module Make (Annot : Annot.S) = struct (proc :: procs, new_predecessors @ predecessors)) ext_program.procs ([], []) 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 () + let { lemmas; preds; only_specs; funcs; macros; bi_specs; datatypes; _ } = + ext_program + in + Prog.make_indexed ~lemmas ~preds ~only_specs ~procs ~predecessors ~funcs + ~macros ~bi_specs ~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/smt/smt.ml b/GillianCore/smt/smt.ml index 8501dc004..2738f7411 100644 --- a/GillianCore/smt/smt.ml +++ b/GillianCore/smt/smt.ml @@ -2,6 +2,7 @@ open Gil_syntax open Utils open Simple_smt open Syntaxes.Option +open Prog_env (* open Ctx *) module L = Logging @@ -24,6 +25,86 @@ let () = Sys.(set_signal sigpipe Signal_ignore) exception SMT_unknown let pp_sexp = Sexplib.Sexp.pp_hum +let ( <| ) constr e = app constr [ e ] +let ( $$ ) constr l = app constr l + +module Variant = struct + module type S = sig + val name : string + val params : (string * sexp) list + val recognizer : string + val recognize : sexp -> sexp + end + + module type Nullary = sig + include S + + val construct : sexp + end + + module type Unary = sig + include S + + val construct : sexp -> sexp + 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 + let name = name + let params = [] + let construct = atom name $$ [] + let recognizer = recognizer + let recognize x = atom recognizer <| x + end in + (module M : Nullary) + + let un ?recognizer name param param_typ = + let module N = (val nul ?recognizer name : Nullary) in + let module M = struct + include N + + let params = [ (param, param_typ) ] + let construct x = atom name <| x + let accessor = atom param + 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 (** {2 Tracking the declarations a query depends on} @@ -34,38 +115,80 @@ let pp_sexp = Sexplib.Sexp.pp_hum type definition = { id : int; - decls : sexp list; (** the SMT commands declaring this definition *) + decls : unit -> sexp list; (** the SMT commands declaring this definition *) depends_on : definition list; (** definitions that must be emitted first *) } -let make_definition = +let make_definition' = let counter = ref 0 in fun ?(depends_on = []) decls -> incr counter; { id = !counter; decls; depends_on } -type _ Effect.t += Require_definition : definition -> unit Effect.t +let make_definition ?depends_on decls = + let decls () = decls in + make_definition' ?depends_on decls + +type _ Effect.t += + | Require_definition : definition -> unit Effect.t + | Require_usr_datatypes : SS.t -> unit Effect.t + | Get_usr_datatypes : + ((module Variant.S) * (string * string list * (module Variant.S) list)) + list + Effect.t let require_definition d = Effect.perform (Require_definition d) +let require_usr_datatypes ds = Effect.perform (Require_usr_datatypes ds) +let get_usr_datatypes () = Effect.perform Get_usr_datatypes + +let datatype_cache : + ( string, + SS.t + * (module Variant.Unary) + * (string * string list * (module Variant.S) list) ) + Hashtbl.t = + Hashtbl.create Config.medium_tbl_size + +let constructor_cache : (string, SS.t * (module Variant.Nary)) Hashtbl.t = + Hashtbl.create Config.medium_tbl_size + +let with_necessary_usr_datatypes (f : unit -> 'a) : 'a = + let needed_usr_datatypes = ref SS.empty in + match f () with + | x -> x + | effect Require_usr_datatypes ds, k -> + needed_usr_datatypes := SS.union !needed_usr_datatypes ds; + Effect.Deep.continue k () + | effect Get_usr_datatypes, k -> + let datatypes = + SS.fold + (fun name acc -> + let _, (module V : Variant.Unary), dt = + Hashtbl.find datatype_cache name + in + ((module V : Variant.S), dt) :: acc) + !needed_usr_datatypes [] + in + Effect.Deep.continue k datatypes (** Run [f], returning its result together with the set of definitions it required (keyed by id), closed under the [depends_on] relation. *) let with_necessary_definitions (f : unit -> 'a) : 'a * (int, definition) Hashtbl.t = - let needed = Hashtbl.create 17 in - let rec add d = - if not (Hashtbl.mem needed d.id) then ( - Hashtbl.replace needed d.id d; - List.iter add d.depends_on) + let needed_defs = Hashtbl.create 17 in + let rec add_def d = + if not (Hashtbl.mem needed_defs d.id) then ( + Hashtbl.replace needed_defs d.id d; + List.iter add_def d.depends_on) in let result = match f () with | x -> x | effect Require_definition d, k -> - add d; + add_def d; Effect.Deep.continue k () in - (result, needed) + (result, needed_defs) (** Send each required definition through [emit], preceded by the definitions it depends on (so declarations always come before their uses). *) @@ -75,7 +198,7 @@ let emit_definitions ~emit (needed : (int, definition) Hashtbl.t) = if not (Hashtbl.mem emitted d.id) then ( Hashtbl.replace emitted d.id (); List.iter go d.depends_on; - List.iter emit d.decls) + List.iter emit (d.decls ())) in Hashtbl.iter (fun _ d -> go d) needed @@ -145,8 +268,6 @@ let encoding_cache : let sat_cache : (Expr.Set.t, sexp option) Hashtbl.t = Hashtbl.create Config.big_tbl_size -let ( <| ) constr e = app constr [ e ] -let ( $$ ) constr l = app constr l let declare_const const typ = atom "declare-const" $$ [ atom const; typ ] let quant q (vars : (sexp * sexp) list) (s : sexp) : sexp = @@ -192,66 +313,13 @@ let set_intersection' ext xs = in f $$ xs -module Variant = struct - module type S = sig - val name : string - val params : (string * sexp) list - val recognizer : string - val recognize : sexp -> sexp - end - - module type Nullary = sig - include S - - val construct : sexp - end - - module type Unary = sig - include S - - val construct : sexp -> sexp - val access : sexp -> sexp - end - - let nul ?recognizer name = - let recognizer = Option.value recognizer ~default:("is" ^ name) in - let module M = struct - let name = name - let params = [] - let construct = atom name $$ [] - let recognizer = recognizer - let recognize x = atom recognizer <| x - end in - (module M : Nullary) - - let un ?recognizer name param param_typ = - let module N = (val nul ?recognizer name : Nullary) in - let module M = struct - include N - - let params = [ (param, param_typ) ] - let construct x = atom name <| x - let accessor = atom param - let access x = accessor <| x - end in - (module M : Unary) -end - let declare_recognizer ~name ~constructor ~typ = define_fun name [ ("x", typ) ] t_bool (list [ atom "_"; atom "is"; atom constructor ] <| atom "x") -(* Builds a datatype declaration together with its recognizers, and returns - both the type's atom and a {!definition} that can be required during - encoding. [depends_on] lists the datatypes this one refers to in its fields, - which must therefore be declared first. *) -let mk_datatype - ?depends_on - 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 -> @@ -264,8 +332,37 @@ let mk_datatype (constructor, recognizer_def)) |> List.split in + let datatype = (name, type_params, constructors) in + (atom name, datatype, recognizer_defs) + +(* Builds a datatype declaration together with its recognizers, and returns + both the type's atom and a {!definition} that can be required during + encoding. [depends_on] lists the datatypes this one refers to in its fields, + which must therefore be declared first. *) +let mk_datatype + ?depends_on + name + type_params + (variants : (module Variant.S) list) = + let name', (_, _, constructors), recognizer_defs = + mk_datatype' (name, type_params, variants) + in let decl = declare_datatype name type_params constructors in - (atom name, make_definition ?depends_on (decl :: recognizer_defs)) + (name', make_definition ?depends_on (decl :: recognizer_defs)) + +(* Builds a definition for mutually recursive datatypes that are evaluated dynamically on each use. + We use this for user datatypes, which must be mutually recursive with GIL literals *) +let mk_datatypes_dyn + ?depends_on + (get : unit -> (string * string list * (module Variant.S) list) list) = + let mk () = + let _, datatypes, recognizer_defs = + get () |> List.map mk_datatype' |> List_utils.split3 + in + let decl = declare_datatypes datatypes in + decl :: List.concat recognizer_defs + in + make_definition' ?depends_on mk let mk_fun_decl ?depends_on name param_types result_type = let decl = declare_fun name param_types result_type in @@ -285,6 +382,7 @@ 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 t_gil_type, def_gil_type = mk_datatype "GIL_Type" [] @@ -301,6 +399,7 @@ module Type_operations = struct (module List : Variant.S); (module Type : Variant.S); (module Set : Variant.S); + (module Datatype : Variant.S); ] end @@ -325,22 +424,30 @@ module Lit_operations = struct module List = (val un "List" "listValue" (t_seq t_gil_literal) : Unary) module None = (val nul "None" : Nullary) + let gil_literal_variants = + [ + (module Undefined : Variant.S); + (module Null : Variant.S); + (module Empty : Variant.S); + (module Bool : Variant.S); + (module Int : Variant.S); + (module Num : Variant.S); + (module String : Variant.S); + (module Loc : Variant.S); + (module Type : Variant.S); + (module List : Variant.S); + (module None : Variant.S); + ] + + let gil_literal_datatypes () = + let usr_datatype_lit_variants, usr_datatypes = + Stdlib.List.split (get_usr_datatypes ()) + in + (gil_literal_name, [], gil_literal_variants @ usr_datatype_lit_variants) + :: usr_datatypes + let def_gil_literal = - snd - @@ mk_datatype ~depends_on:[ def_gil_type ] gil_literal_name [] - [ - (module Undefined : Variant.S); - (module Null : Variant.S); - (module Empty : Variant.S); - (module Bool : Variant.S); - (module Int : Variant.S); - (module Num : Variant.S); - (module String : Variant.S); - (module Loc : Variant.S); - (module Type : Variant.S); - (module List : Variant.S); - (module None : Variant.S); - ] + mk_datatypes_dyn ~depends_on:[ def_gil_type ] gil_literal_datatypes end let t_gil_literal = Lit_operations.t_gil_literal @@ -348,6 +455,87 @@ let def_gil_literal = Lit_operations.def_gil_literal 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 -> + require_definition def_gil_literal; + t_gil_literal_list + | BooleanType -> t_bool + | NumberType -> t_real + | UndefinedType | NoneType | EmptyType | NullType -> + require_definition def_gil_literal; + t_gil_literal + | SetType -> + require_definition def_gil_literal; + t_gil_literal_set + | TypeType -> + require_definition def_gil_type; + t_gil_type + | DatatypeType name -> atom name + +module Datatype_operations = struct + 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 + Variant.un variant_name parameter_name t_datatype + + let rec encode_single_constructor ~cycle (c : Constructor.t) = + let param_types = + c.constructor_fields + |> List.map @@ function + | Some t -> + let () = + match t with + | Type.DatatypeType name -> ensure_encoded name + | _ -> () + in + native_sort_of_type t + | None -> t_gil_literal + in + let variant = Variant.n c.constructor_name param_types in + Hashtbl.replace constructor_cache c.constructor_name (cycle, variant); + (module (val variant : Variant.Nary) : Variant.S) + + and encode_single_datatype ~cycle name = + let d = Datatype_env.get_datatype_exn name in + let ctor_variants = + List.map (encode_single_constructor ~cycle) d.datatype_constructors + in + let datatype = (name, [], ctor_variants) in + let lit_variant = mk_user_def_datatype_lit_variant d in + Hashtbl.replace datatype_cache name (cycle, lit_variant, datatype) + + and ensure_encoded name : unit = + if not (Hashtbl.mem datatype_cache name) then + let cycle = SS.add name (Datatype_env.get_datatype_cycle name) in + SS.iter (encode_single_datatype ~cycle) cycle + + let ensure_encoded_c cname : unit = + let c = Datatype_env.get_constructor_exn cname in + ensure_encoded c.constructor_datatype + + let encode_datatype name = + ensure_encoded name; + let cycle, lit_variant, _ = Hashtbl.find datatype_cache name in + require_usr_datatypes cycle; + lit_variant + + let encode_constructor cname = + ensure_encoded_c cname; + let cycle, variant = Hashtbl.find constructor_cache cname in + require_usr_datatypes cycle; + variant +end + let seq_of ~typ xs = require_definition def_gil_literal; match xs with @@ -426,6 +614,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 _ -> exceptf "DEATH: encode_type with arg: %a" Type.pp t module Encoding = struct @@ -435,25 +625,6 @@ module Encoding = struct | Simple_wrapped (** Cannot be a set *) | Extended_wrapped (** Can be a set *) - let native_sort_of_type = - let open Type in - function - | IntType | StringType | ObjectType -> t_int - | ListType -> - require_definition def_gil_literal; - t_gil_literal_list - | BooleanType -> t_bool - | NumberType -> t_real - | UndefinedType | NoneType | EmptyType | NullType -> - require_definition def_gil_literal; - t_gil_literal - | SetType -> - require_definition def_gil_literal; - t_gil_literal_set - | TypeType -> - require_definition def_gil_type; - t_gil_type - type t = { consts : (string * sexp) Hashset.t; [@default Hashset.empty ()] kind : kind; @@ -504,30 +675,49 @@ module Encoding = struct in { enc' with consts; extra_asrts } - let get_native ~accessor { expr; kind; _ } = - (* No additional check is performed on native type, - it should be already type checked *) - match kind with - | Native _ -> expr - | Simple_wrapped -> - require_definition def_gil_literal; - accessor expr - | Extended_wrapped -> - require_definition def_gil_ext_literal; - accessor (Ext_lit_operations.Gil_sing_elem.access expr) + let get_native + ~accessor + ~recognizer + ~typ + ({ expr; kind; extra_asrts; _ } as enc) : t = + let expr, guards = + match kind with + | Native _ -> + (* No additional check is performed on native type, + it should be already type checked *) + (expr, []) + | Simple_wrapped -> + require_definition def_gil_literal; + (accessor expr, [ recognizer expr ]) + | Extended_wrapped -> + require_definition def_gil_ext_literal; + 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 expr = require_definition def_gil_literal; make ~kind:Simple_wrapped expr + let extended_wrapped expr = + require_definition def_gil_ext_literal; + make ~kind:Extended_wrapped expr + (** 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 require_definition def_gil_literal; match kind with - | Simple_wrapped -> expr + | Simple_wrapped -> enc | Native typ -> let construct = match typ with @@ -538,36 +728,92 @@ module Encoding = struct | TypeType -> Type.construct | BooleanType -> Bool.construct | ListType -> List.construct + | DatatypeType name -> + let (module U : Variant.Unary) = + Datatype_operations.encode_datatype name + in + U.construct | UndefinedType | NullType | EmptyType | NoneType | SetType -> exceptf "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 + { 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 extend_wrap e = + let extend_wrap ({ expr; kind; _ } as enc) = require_definition def_gil_ext_literal; - 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) + 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 enc = simple_wrap enc in + let expr = Ext_lit_operations.Gil_sing_elem.construct enc.expr in + { enc with expr; kind = Extended_wrapped } + + include struct + open Lit_operations + + let get_bool = + get_native ~accessor:Bool.access ~recognizer:Bool.recognize + ~typ:BooleanType + + let get_int = + get_native ~accessor:Int.access ~recognizer:Int.recognize ~typ:IntType + + let get_num = + get_native ~accessor:Num.access ~recognizer:Num.recognize ~typ:NumberType - 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 + let get_string = + get_native ~accessor:String.access ~recognizer:String.recognize + ~typ:StringType - let get_set { kind; expr; _ } = + let get_loc = + get_native ~accessor:Loc.access ~recognizer:Loc.recognize ~typ:ObjectType + + let get_list = + get_native ~accessor:List.access ~recognizer:List.recognize ~typ:ListType + + let get_type = + get_native ~accessor:Type.access ~recognizer:Type.recognize ~typ:TypeType + end + + let get_set ({ kind; expr; extra_asrts; _ } as enc) : t = match kind with | Native SetType -> require_definition def_gil_literal; - expr + enc | Extended_wrapped -> require_definition def_gil_ext_literal; - Ext_lit_operations.Gil_set.access expr + 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 kind; extra_asrts; expr } | _ -> exceptf "wrong encoding of set" - let get_string = get_native ~accessor:Lit_operations.String.access + let get_datatype name = + let (module V : Variant.Unary) = Datatype_operations.encode_datatype name in + get_native ~accessor:V.access ~recognizer:V.recognize + ~typ:(DatatypeType name) + + let get_native_of_type = function + | Type.BooleanType -> get_bool + | IntType -> get_int + | NumberType -> get_num + | StringType -> get_string + | ObjectType -> get_loc + | ListType -> get_list + | TypeType -> get_type + | DatatypeType name -> get_datatype name + | (UndefinedType | NullType | EmptyType | NoneType | SetType) as typ -> + Fmt.failwith "Cannot get native value of type %s" + (Gil_syntax.Type.str typ) end let typeof_simple e = @@ -660,7 +906,8 @@ let rec encode_lit (lit : Literal.t) : Encoding.t = | Type t -> encode_type t >- TypeType | LList lits -> require_definition def_gil_literal; - 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 -> exceptf "DEATH: encode_lit %a. %s" Literal.pp lit msg @@ -669,23 +916,26 @@ 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 _ -> exceptf "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 -> + let expr = + match Type.equal t1 BooleanType with + | true when is_true p1.expr -> p2.expr + | true when is_true p2.expr -> p1.expr + | _ -> eq p1.expr p2.expr + in + expr >- BooleanType + | Simple_wrapped, Simple_wrapped | Extended_wrapped, Extended_wrapped -> + eq p1.expr p2.expr >- BooleanType + | Native _, Native _ -> exceptf "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 = @@ -698,40 +948,99 @@ 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 + | 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 (* Numbers are encoded as reals, so float division must use SMT-LIB real division ["/" *) - | FDiv -> app_ "/" [ 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 + | FDiv -> + let>- p1 = get_num p1 in + let>- p2 = get_num p2 in + app_ "/" [ 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 -> require_definition Axiomatised_operations.def_snth; - 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 @@ -764,46 +1073,65 @@ 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 -> require_definition def_llen; - llen <| get_list le - | _ -> seq_len (get_list le) + llen <| le.expr + | _ -> seq_len le.expr in enc >- IntType | StrLen -> require_definition def_slen; - slen <| get_string le >- NumberType + let>- le = get_string le in + slen <| le.expr >- NumberType | ToStringOp -> require_definition def_num2str; - Axiomatised_operations.num2str <| get_num le >- StringType + let>- le = get_num le in + Axiomatised_operations.num2str <| le.expr >- StringType | ToNumberOp -> require_definition def_str2num; - Axiomatised_operations.str2num <| get_string le >- NumberType + let>- le = get_string le in + Axiomatised_operations.str2num <| le.expr >- NumberType | ToIntOp -> require_definition def_num2int; - Axiomatised_operations.num2int <| get_num le >- NumberType - | Not -> bool_not (get_bool le) >- BooleanType + 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 + | ToUint32Op -> + let>- le = get_num le in + le.expr |> real_to_int |> int_to_real >- NumberType | LstRev -> require_definition def_lrev; - Axiomatised_operations.lrev <| get_list le >- ListType - | NumToInt -> get_num le |> real_to_int >- IntType - | IntToNum -> get_int le |> int_to_real >- NumberType + let>- le = get_list le in + Axiomatised_operations.lrev <| le.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 -> - encode_equality - (get_num le |> real_to_int |> int_to_real >- NumberType) - le + let>- le = get_num le in + encode_equality (le.expr |> real_to_int |> int_to_real >- NumberType) le | BitwiseNot | M_isNaN | M_abs @@ -830,6 +1158,67 @@ let encode_unop ~llen_lvars ~e (op : UnOp.t) le = let () = L.print_to_all msg in raise (Failure msg) +let copy_extend_gamma gamma vars = + (* Start by updating gamma with the information provided by bound / quantifier types. + There's very few foralls, so it's ok to copy the gamma entirely *) + let gamma = Hashtbl.copy gamma in + let () = + vars + |> List.iter (fun (x, typ) -> + match typ with + | None -> Hashtbl.remove gamma x + | Some typ -> Hashtbl.replace gamma x typ) + in + (* Not the same gamma now!*) + gamma + +let encode_bound_expr + ~(encode_expr : + gamma:typenv -> + llen_lvars:SS.t -> + list_elem_vars:SS.t -> + 'a -> + Encoding.t) + ~gamma + ~llen_lvars + ~list_elem_vars + bound_vars + (expr : 'a) = + let open Encoding in + let gamma = copy_extend_gamma gamma bound_vars in + 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 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 + | None -> t_gil_ext_literal + | Some typ -> native_sort_of_type typ + in + (x, sort)) + in + let () = + encoded.consts + |> Hashtbl.filter_map_inplace (fun c () -> + if List.mem c bound_vars then None else Some ()) + in + (bound_vars, bound_asrts, encoded) + let encode_quantified_expr ~(encode_expr : gamma:typenv -> @@ -851,17 +1240,7 @@ let encode_quantified_expr 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 () = - quantified_vars - |> List.iter (fun (x, typ) -> - match typ with - | None -> Hashtbl.remove gamma x - | Some typ -> Hashtbl.replace gamma x typ) - in - (* Not the same gamma now!*) + let gamma = copy_extend_gamma gamma quantified_vars in let encoded_assertion, consts, extra_asrts = match encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion with | { kind = Native BooleanType; expr; consts; extra_asrts } -> @@ -874,7 +1253,7 @@ let encode_quantified_expr let sort = match t with | None -> t_gil_ext_literal - | Some typ -> Encoding.native_sort_of_type typ + | Some typ -> native_sort_of_type typ in (x, sort)) in @@ -916,33 +1295,107 @@ 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_types = + match Function_env.get_function_param_types name with + | None -> exceptf "SMT - Undefined function %s" name + | Some ps -> ps + in + let extend_wrap_or_native = function + | 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_types args in + let args = List.map (fun arg -> arg.expr) args in + extended_wrapped (app_ name args) + | Cases (le, cs) -> + (* Type checking should ensure that all constructors belong to the same datatype *) + let constructors_t = + match cs with + | (cname, _, _) :: _ -> + let c = Datatype_env.get_constructor_exn cname in + Type.DatatypeType c.Constructor.constructor_datatype + | [] -> exceptf "SMT - No cases given in case statement" + in + let>- le = f le in + (* Convert to native *) + let>- le_native = get_native_of_type constructors_t le in + (* Encode match cases *) + let cs, encs = + cs + |> List.map (fun (cname, bs, e) -> + let c = Datatype_env.get_constructor_exn cname in + let (module V : Variant.Nary) = + Datatype_operations.encode_constructor cname + in + let pat = PCon (cname, bs) in + let bts = List.combine bs c.constructor_fields in + (* TODO: How to handle extra aserts involving bound vars?? *) + (* Using ite and mapping to undefined values when extra asrts are false cases 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 + ((pat, encoded.expr), encoded)) + |> List.split + in + let fallback = (PVar "_", (extend_wrap undefined_encoding).expr) in + let>-- _ = encs in + extended_wrapped (match_datatype le_native.expr (cs @ [ fallback ])) + | ConstructorApp (cname, les) -> + let c = Datatype_env.get_constructor_exn cname in + let (module V : Variant.Nary) = + Datatype_operations.encode_constructor cname + in + let param_types = c.constructor_fields in + let simple_wrap_or_native = function + | 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_types args in + let args = List.map (fun arg -> arg.expr) args in + let sexp = V.construct args in + sexp >- DatatypeType c.constructor_datatype let encode_assertion_top_level ~(gamma : typenv) @@ -1118,6 +1571,7 @@ let exec_sat' (fs : Expr.Set.t) (gamma : typenv) : sexp option = fs pp_typenv gamma) in let () = reset_solver () in + with_necessary_usr_datatypes @@ fun () -> let encoded_assertions, necessary_definitions = encode_assertions fs gamma in let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in let () = emit_definitions ~emit:cmd necessary_definitions in diff --git a/GillianCore/utils/containers.ml b/GillianCore/utils/containers.ml index ad139d06a..108cd0b36 100644 --- a/GillianCore/utils/containers.ml +++ b/GillianCore/utils/containers.ml @@ -68,3 +68,5 @@ module SN = struct include Set.Make (MyNumber) end + +module StringMap = Map.Make (String) diff --git a/GillianCore/utils/gillian_result.ml b/GillianCore/utils/gillian_result.ml index a89df6444..298d8a191 100644 --- a/GillianCore/utils/gillian_result.ml +++ b/GillianCore/utils/gillian_result.ml @@ -138,6 +138,9 @@ module Exc = struct let analysis_failure ?(is_preprocessing = false) ?in_target ?loc msg = Gillian_error (make_analysis_failures ~is_preprocessing ?in_target ?loc msg) + + let compilation_error ?(additional_data : Yojson.Safe.t option) ?loc msg = + Gillian_error (CompilationError { msg; loc; additional_data }) end type 'a t = ('a, Error.t) result diff --git a/GillianCore/utils/list_utils.ml b/GillianCore/utils/list_utils.ml index 0b9b4afc4..c58b3389e 100644 --- a/GillianCore/utils/list_utils.ml +++ b/GillianCore/utils/list_utils.ml @@ -264,3 +264,11 @@ let[@tail_mod_cons] rec drop n = function let get_single = function | [ x ] -> Some x | _ -> None + +let lengths_eq a b = List.length a = List.length b + +let rec split3 = function + | [] -> ([], [], []) + | (x, y, z) :: l -> + let rx, ry, rz = split3 l in + (x :: rx, y :: ry, z :: rz) diff --git a/GillianCore/utils/prelude.ml b/GillianCore/utils/prelude.ml index dc514bf55..5d1d55085 100644 --- a/GillianCore/utils/prelude.ml +++ b/GillianCore/utils/prelude.ml @@ -101,6 +101,11 @@ module Hashtbl = struct `List [ key_to_yojson k; val_to_yojson v ] in `List (hashtbl |> to_seq |> Seq.map kv_to_yojson |> List.of_seq) + + let memoize ?(size = 1) f = + let cache = create size in + let f' x = find_or_else_add cache x (fun () -> f x) in + f' end (** Extension of Map with functions to serialize to and deserialize from yojson @@ -181,6 +186,8 @@ module Hashset = struct (** Applies [f] to each element of the set *) let iter f set = Hashtbl.iter (fun x () -> f x) set + let fold f tbl acc = Hashtbl.fold (fun k _ acc -> f k acc) tbl acc + (** Filters the set in-place *) let filter_in_place (h : 'a t) (f : 'a -> bool) = Hashtbl.filter_map_inplace (fun x () -> if f x then Some () else None) h diff --git a/GillianCore/utils/tarjan.ml b/GillianCore/utils/tarjan.ml new file mode 100644 index 000000000..093fcaa68 --- /dev/null +++ b/GillianCore/utils/tarjan.ml @@ -0,0 +1,69 @@ +(** Tarjan's strongly connected components algorithm (cycle detection *) + +open Prelude + +open struct + type 'a state = { + get_edges : 'a -> 'a list; [@main] + mutable index : int; [@default 0] + index_map : ('a, int) Hashtbl.t; [@default Hashtbl.create 0] + lowlink : ('a, int) Hashtbl.t; [@default Hashtbl.create 0] + on_stack : ('a, bool) Hashtbl.t; [@default Hashtbl.create 0] + mutable stack : 'a list; [@default []] + mutable sccs : 'a list list; [@default []] + } + [@@deriving make] + + (* Strong connect (core of Tarjan's algorithm) *) + let rec strong_connect state v = + (* Set the depth index for v to the smallest unused index *) + Hashtbl.replace state.index_map v state.index; + Hashtbl.replace state.lowlink v state.index; + state.index <- state.index + 1; + state.stack <- v :: state.stack; + Hashtbl.replace state.on_stack v true; + + let successors = state.get_edges v in + List.iter + (fun w -> + if not (Hashtbl.mem state.index_map w) then ( + (* Successor w has not yet been visited; recurse on it *) + strong_connect state w; + let v_low = Hashtbl.find state.lowlink v in + let w_low = Hashtbl.find state.lowlink w in + Hashtbl.replace state.lowlink v (min v_low w_low)) + else if Hashtbl.find state.on_stack w then + (* Successor w is on stack and hence in the current SCC *) + let v_low = Hashtbl.find state.lowlink v in + let w_idx = Hashtbl.find state.index_map w in + Hashtbl.replace state.lowlink v (min v_low w_idx)) + successors; + + (* If v is a root node, pop the stack and generate an SCC *) + let v_low = Hashtbl.find state.lowlink v in + let v_idx = Hashtbl.find state.index_map v in + if v_low = v_idx then ( + let scc = ref [] in + let rec pop_loop () = + let w = List.hd state.stack in + state.stack <- List.tl state.stack; + Hashtbl.replace state.on_stack w false; + scc := w :: !scc; + if w <> v then pop_loop () + in + pop_loop (); + state.sccs <- !scc :: state.sccs) +end + +(* Main entry point: returns a list of SCCs (each SCC is a list of node names) *) +let tarjan iter_vertices get_edges = + let state = make_state get_edges in + (* Collect all vertices (keys + values appearing in adjacency lists) *) + let vertices = Hashset.empty () in + iter_vertices (Hashset.add vertices); + (* Run strongconnect for every unvisited vertex *) + Hashset.iter + (fun v -> + if not (Hashtbl.mem state.index_map v) then strong_connect state v) + vertices; + state.sccs diff --git a/GillianCore/utils/utils.ml b/GillianCore/utils/utils.ml index 6ffddf42f..09d0f22a4 100644 --- a/GillianCore/utils/utils.ml +++ b/GillianCore/utils/utils.ml @@ -124,6 +124,8 @@ module Gillian_result = struct include Gillian_result end +module Tarjan = Tarjan + (**/**) module Preprocessing_utils = Preprocessing_utils diff --git a/wisl/examples/SLL_adt.wisl b/wisl/examples/SLL_adt.wisl new file mode 100644 index 000000000..7ff75bf21 --- /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 0c1da5a9e..4c1168ff0 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_recursive.wisl b/wisl/examples/SLL_recursive.wisl index 148a45062..af658ee96 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 000000000..4f87ad2f6 --- /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/lib/ParserAndCompiler/WLexer.mll b/wisl/lib/ParserAndCompiler/WLexer.mll index b520daed1..c41d7a9b1 100644 --- a/wisl/lib/ParserAndCompiler/WLexer.mll +++ b/wisl/lib/ParserAndCompiler/WLexer.mll @@ -35,9 +35,11 @@ rule read = | "new" { NEW (curr lexbuf) } | "free" { DELETE (curr lexbuf) } | "dispose"{ DELETE (curr lexbuf) } + | "pure" { PURE (curr lexbuf) } | "function" { FUNCTION (curr lexbuf) } | "par" { PAR (curr lexbuf) } | "predicate" { PREDICATE (curr lexbuf) } + | "datatype" { DATATYPE (curr lexbuf) } | "invariant" { INVARIANT (curr lexbuf) } | "return" { RETURN (curr lexbuf) } | "fold" { FOLD (curr lexbuf) } @@ -56,12 +58,14 @@ rule read = | "forall" { FORALL (curr lexbuf) } | "bind" { BIND (curr lexbuf) } | "spec" { SPEC (curr lexbuf) } + | "case" { CASE (curr lexbuf) } (* types *) | "List" { TLIST (curr lexbuf) } | "Int" { TINT (curr lexbuf) } | "Bool" { TBOOL (curr lexbuf) } | "String" { TSTRING (curr lexbuf) } | "Float" { TFLOAT (curr lexbuf) } + | "Any" { TANY (curr lexbuf) } (* strings and comments *) | '"' { let () = l_start_string := curr lexbuf in read_string (Buffer.create 17) lexbuf } @@ -88,6 +92,7 @@ rule read = | ',' { COMMA (curr lexbuf) } | "." { DOT (curr lexbuf) } | ';' { SCOLON (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 1805f6f2e..d2f34fb37 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 PAR -%token FUNCTION RETURN PREDICATE LEMMA -%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE BIND FORALL +%token PURE FUNCTION RETURN PREDICATE LEMMA DATATYPE +%token INVARIANT PACKAGE FOLD UNFOLD NOUNFOLD APPLY ASSERT ASSUME ASSUME_TYPE BIND FORALL CASE %token STATEMENT WITH VARIANT PROOF CONFIG %token SPEC @@ -24,12 +24,14 @@ %token SETOPEN /* -{ */ %token SETCLOSE /* }- */ %token VDASH /* |- */ +%token QUOTE /* ' */ (* types *) %token TLIST %token TINT %token TBOOL %token TSTRING +%token TANY %token TFLOAT (* names *) @@ -97,58 +99,72 @@ %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 pred_param -%type <(string * string) list> unfold_bindings -%type unfold_binding -%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 pred_param +%type <(string * string) list> unfold_bindings +%type unfold_binding +%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_val: | v = value_with_loc @@ -179,8 +195,8 @@ spec_bindings: (lstart, spec_name, variables) } 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 } | bindings = spec_bindings; LCBRACE; pre = logic_assertion; RCBRACE; variant = option(with_variant_def); f = fct; LCBRACE; @@ -239,6 +255,10 @@ type_target: | loc = TBOOL { WType.WBool, loc } | loc = TSTRING { WType.WString, loc } | loc = TFLOAT { WType.WFloat, loc } + | loc = TANY { WType.WAny, loc } + | datatype = IDENTIFIER + { let (loc, datatype) = datatype in + WType.WDatatype datatype, loc } logical_binding: | LBRACE; lhs = LVAR; COLON; rhs = LVAR; RBRACE @@ -275,7 +295,6 @@ function_call: function_call_list: sl = separated_nonempty_list(SCOLON, function_call) { sl } - statement: | loc = SKIP { WStmt.make WStmt.Skip loc } | lx = IDENTIFIER; ASSIGN; e = expression @@ -443,7 +462,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 @@ -479,7 +498,7 @@ predicate: ins = separated_list(COMMA, pred_param); outs = outs(pred_param); RBRACE; LCBRACE; - pred_definitions = separated_nonempty_list(SCOLON, logic_assertion); + pred_definitions = separated_nonempty_list(SCOLON, logic_assertion_top_level); lend = RCBRACE; { let (_, pred_name) = lpname in let pred_params = ins @ outs in @@ -539,13 +558,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 @@ -581,6 +600,13 @@ wand: ((lname, lins @ louts), (rname, rins @ routs), 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_expression_with_permission: | LBRACE; perm = logic_expression; COLON; expr = logic_expression; RBRACE; { (Some perm, expr) } @@ -656,8 +682,6 @@ logic_assertion: let loc = CodeLoc.merge lstart lend in WLAssert.make bare_assert loc } - - logic_expression: | lstart = LBRACE; le = logic_expression; lend = RBRACE { let loc = CodeLoc.merge lstart lend in @@ -705,7 +729,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(SCOLON, 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: @@ -723,6 +764,89 @@ logic_value_with_loc: 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(SCOLON, 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 + { (List.map fst 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, Option.map fst typ) } + /* https://discuss.ocaml.org/t/solving-shift-reduce-conflicts-for-optional-trailing-comma-in-menhir/15042 */ separated_nonempty_list_option_trailing(SEP, X): | x = X { [x] } diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml index 31d2ee622..9485922f8 100644 --- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml +++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml @@ -29,6 +29,7 @@ let compile_type t = | WInt -> Some Type.IntType | WFloat -> Some Type.NumberType | WSet -> Some Type.SetType + | WDatatype n -> Some (Type.DatatypeType n) | WAny -> None) let invert_binop : WBinOp.t -> bool = function @@ -168,9 +169,11 @@ 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 compile_lexpr = compile_lexpr ~fname in +let rec compile_lexpr + ?(fname = "main") + ?(is_pure_fun_def = false) + (lexpr : WLExpr.t) : string list * Asrt.t * Expr.t = + let compile_lexpr = compile_lexpr ~fname ~is_pure_fun_def in let expr_pname_of_binop b = WBinOp.( match b with @@ -195,10 +198,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 = Utils.Generators.fresh_lvar () in let internal_pred = expr_pname_of_binop b in let gvars1, asrtl1, comp_expr1 = compile_lexpr e1 in @@ -246,7 +253,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) )) let compile_lexpr_perm ?fname lexpr = match lexpr with @@ -1007,6 +1036,33 @@ 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 = + WTypeMap.infer_types_pure_fun pure_fun_params pure_fun_definition + in + let get_wisl_type x = (x, WTypeMap.type_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; loop_body_of; _ } = @@ -1183,7 +1239,47 @@ let compile_lemma lemma_location; } -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 @@ -1195,6 +1291,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 @@ -1203,10 +1301,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) @@ -1234,4 +1336,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 000000000..708ea60e9 --- /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 000000000..708ea60e9 --- /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 000000000..6a4544593 --- /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 000000000..6a4544593 --- /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 dae88d7d1..735b13fa8 100644 --- a/wisl/lib/syntax/WLExpr.ml +++ b/wisl/lib/syntax/WLExpr.ml @@ -1,4 +1,5 @@ open VisitorUtils +open Gillian.Utils.Containers type tt = | LVal of WVal.t @@ -9,7 +10,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 @@ -32,11 +37,9 @@ let rec from_expr expr = in { wleid; wleloc; wlenode } +let double_union (sa1, sb1) (sa2, sb2) = (SS.union sa1 sa2, SS.union sb1 sb2) + let rec get_vars_and_lvars le = - let module SS = Set.Make (String) in - let double_union (sa1, sb1) (sa2, sb2) = - (SS.union sa1 sa2, SS.union sb1 sb2) - in match get le with | LVar v -> (SS.empty, SS.singleton v) | PVar v -> (SS.singleton v, SS.empty) @@ -50,6 +53,20 @@ let rec get_vars_and_lvars le = List.fold_left double_union (SS.empty, SS.empty) (List.map get_vars_and_lvars lel) | LVal _ -> (SS.empty, SS.empty) + | LPureFunApp (_, lel) | LConstructorApp (_, lel) -> + List.fold_left double_union (SS.empty, SS.empty) + (List.map get_vars_and_lvars lel) + | LCases (le, cases) -> + let le_vars = get_vars_and_lvars le in + let cases_vars = List.map get_vars_and_lvars_of_case cases in + List.fold_left double_union le_vars cases_vars + +and get_vars_and_lvars_of_case { binders; lexpr; _ } = + let binders = SS.of_list binders in + let vars, lvars = get_vars_and_lvars lexpr in + (* I *think* we don't want bound vars. *) + let lvars = SS.diff lvars binders in + (vars, lvars) let rec get_by_id id lexpr = let getter = get_by_id id in @@ -60,6 +77,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 +101,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 +137,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 f485357ea..751b0b61b 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 461e5d53a..357115728 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 92353173e..aa6539ce8 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 000000000..4d95649b7 --- /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 000000000..4d95649b7 --- /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 7a809c92c..d8da64b96 100644 --- a/wisl/lib/syntax/WType.ml +++ b/wisl/lib/syntax/WType.ml @@ -9,6 +9,7 @@ type t = | WFloat | WAny | WSet + | WDatatype of string (** Are types t1 and t2 compatible *) let compatible t1 t2 = @@ -38,6 +39,7 @@ let pp fmt t = | WFloat -> s "Float" | WAny -> s "Any" | WSet -> s "Set" + | WDatatype t -> s t let to_gil : t -> Gil_syntax.Type.t = function | WList -> ListType diff --git a/wisl/lib/syntax/WType.mli b/wisl/lib/syntax/WType.mli index 576bb327e..4f644d3ab 100644 --- a/wisl/lib/syntax/WType.mli +++ b/wisl/lib/syntax/WType.mli @@ -1,4 +1,14 @@ -type t = WList | WNull | WBool | WString | WPtr | WInt | WFloat | WAny | WSet +type t = + | WList + | WNull + | WBool + | WString + | WPtr + | WInt + | WFloat + | WAny + | WSet + | WDatatype of string val compatible : t -> t -> bool val strongest : t -> t -> t diff --git a/wisl/lib/syntax/WTypeMap.ml b/wisl/lib/syntax/WTypeMap.ml index 7fee6bab0..9a7dc312d 100644 --- a/wisl/lib/syntax/WTypeMap.ml +++ b/wisl/lib/syntax/WTypeMap.ml @@ -110,6 +110,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 = @@ -182,3 +190,23 @@ let infer_types_pred (params : (string * WType.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 * WType.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/WTypeMap.mli b/wisl/lib/syntax/WTypeMap.mli index 65ad549c9..f8fa1cd7b 100644 --- a/wisl/lib/syntax/WTypeMap.mli +++ b/wisl/lib/syntax/WTypeMap.mli @@ -7,3 +7,4 @@ type t = WType.t TypeMap.t val type_of_variable : string -> t -> WType.t option val infer_types_pred : (string * WType.t option) list -> WLAssert.t list -> t +val infer_types_pure_fun : (string * WType.t option) list -> WLExpr.t -> t diff --git a/wisl/lib/syntax/dune b/wisl/lib/syntax/dune index 16ab3e187..86e28d4c1 100644 --- a/wisl/lib/syntax/dune +++ b/wisl/lib/syntax/dune @@ -1,5 +1,5 @@ (library (name wSyntax) (public_name wisl.syntax) - (libraries wUtils) + (libraries wUtils gillian) (flags :standard -open WUtils))