From a8228d3636bcf725e645f1a46fa813b4f56b8161 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Sat, 18 Jan 2020 09:14:10 +1100 Subject: [PATCH] Add support for abstract/free types Represent abstract types as roughly equivalent to a struct with one integer field. The integer describes a unique reference to an object of the abstract type -- like a pointer. This field is implemented as a different index type to regular record fields to ensure type safety. In implementing this new index type, I have erred on the side of emulating regular struct behaviour. I chose struct-like this representation over the Abstr type in terms/types.ml because it gives counterexamples, while Abstr did not when I tried it. As an example, the test in tests/regression/falsifiable/abstract_type.lus defines an abstract type `COUNTER`. It also defines imported (FFI) operations for retrieving the count and incrementing the counter, which returns a new counter with a one-higher count. For properties that fail, the counterexamples for the abstract type look like arbitrary numbers, but the important thing is that each number uniquely maps to an abstract state describing the counter's internals. For this test, I get the following counterexample. The initial counter is given a reference of 2, but the operation `get_counter` maps reference 2 to the actual count of 0. Then, incrementing counter referenced by 2 returns a new counter reference of 8. Asking this new counter for its count returns the actual incremented count of 1. ``` Property (true -> (get_counter(c) = get_counter((pre c)))) is invalid by bounded model checking for k=1 after 0.186s. Counterexample: Node test () == Inputs == init.COUNTER 2 2 == Outputs == c.COUNTER 2 8 Function get_counter (test[l17c40]) == Inputs == in.COUNTER 4 2 == Outputs == out 7 0 Function increment (test[l16c14]) == Inputs == in.COUNTER 3 2 == Outputs == out.COUNTER 6 8 Function get_counter (test[l17c23]) == Inputs == in.COUNTER 2 8 == Outputs == out 0 1 ``` --- src/inputParser.ml | 3 +- src/lustre/lustreAst.ml | 5 +++ src/lustre/lustreAst.mli | 1 + src/lustre/lustreContext.ml | 3 +- src/lustre/lustreDeclarations.ml | 31 ++++++++++---- src/lustre/lustreIndex.ml | 40 ++++++++++++++----- src/lustre/lustreIndex.mli | 3 ++ src/lustre/lustreSimplify.ml | 17 ++++++-- tests/regression/error/abstract_type.lus | 9 +++++ .../regression/falsifiable/abstract_type.lus | 19 +++++++++ tests/regression/success/abstract_type.lus | 29 ++++++++++++++ 11 files changed, 138 insertions(+), 22 deletions(-) create mode 100644 tests/regression/error/abstract_type.lus create mode 100644 tests/regression/falsifiable/abstract_type.lus create mode 100644 tests/regression/success/abstract_type.lus diff --git a/src/inputParser.ml b/src/inputParser.ml index 356fd05da..24075009d 100644 --- a/src/inputParser.ml +++ b/src/inputParser.ml @@ -218,7 +218,8 @@ let rec read_val scope name indexes arr_indexes json = | LustreIndex.ArrayIntIndex _ -> false | LustreIndex.RecordIndex _ | LustreIndex.TupleIndex _ - | LustreIndex.ListIndex _ -> true) + | LustreIndex.ListIndex _ + | LustreIndex.AbstractTypeIndex _ -> true) |> Format.asprintf "%s%a" name (LustreIndex.pp_print_index true) in diff --git a/src/lustre/lustreAst.ml b/src/lustre/lustreAst.ml index 6232af1f1..378ee4a62 100644 --- a/src/lustre/lustreAst.ml +++ b/src/lustre/lustreAst.ml @@ -160,6 +160,7 @@ and lustre_type = | IntRange of position * expr * expr | Real of position | UserType of position * ident + | AbstractType of position * ident | TupleType of position * lustre_type list | RecordType of position * typed_ident list | ArrayType of position * (lustre_type * expr) @@ -664,6 +665,10 @@ and pp_print_lustre_type ppf = function Format.fprintf ppf "%a" pp_print_ident s + | AbstractType (pos, s) -> + + Format.fprintf ppf "%a" pp_print_ident s + | TupleType (pos, l) -> Format.fprintf ppf diff --git a/src/lustre/lustreAst.mli b/src/lustre/lustreAst.mli index 2191fb93a..2c71d4297 100644 --- a/src/lustre/lustreAst.mli +++ b/src/lustre/lustreAst.mli @@ -155,6 +155,7 @@ and lustre_type = | IntRange of position * expr * expr | Real of position | UserType of position * ident + | AbstractType of position * ident | TupleType of position * lustre_type list | RecordType of position * typed_ident list | ArrayType of position * (lustre_type * expr) diff --git a/src/lustre/lustreContext.ml b/src/lustre/lustreContext.ml index 8725263b6..667d0f57b 100644 --- a/src/lustre/lustreContext.ml +++ b/src/lustre/lustreContext.ml @@ -635,7 +635,8 @@ let mk_state_var | D.ArrayIntIndex _ -> false | D.RecordIndex _ | D.TupleIndex _ - | D.ListIndex _ -> true) + | D.ListIndex _ + | D.AbstractTypeIndex _ -> true) index) in diff --git a/src/lustre/lustreDeclarations.ml b/src/lustre/lustreDeclarations.ml index 1a355be74..022e81d4b 100644 --- a/src/lustre/lustreDeclarations.ml +++ b/src/lustre/lustreDeclarations.ml @@ -1003,7 +1003,10 @@ let rec expand_tuple' pos accum bounds lhs rhs = match lhs, rhs with (* Record index on left-hand and right-hand side *) | (D.RecordIndex i :: lhs_index_tl, state_var) :: lhs_tl, - (D.RecordIndex j :: rhs_index_tl, expr) :: rhs_tl -> + (D.RecordIndex j :: rhs_index_tl, expr) :: rhs_tl + (* Abstract type index works like record except program cannot project field *) + | (D.AbstractTypeIndex i :: lhs_index_tl, state_var) :: lhs_tl, + (D.AbstractTypeIndex j :: rhs_index_tl, expr) :: rhs_tl -> (* Indexes are sorted, must match *) if i = j then @@ -1024,24 +1027,35 @@ let rec expand_tuple' pos accum bounds lhs rhs = match lhs, rhs with | (D.RecordIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _ | (D.RecordIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _ | (D.RecordIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _ + | (D.RecordIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _ | (D.TupleIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _ | (D.TupleIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _ | (D.TupleIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _ + | (D.TupleIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _ | (D.ListIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _ | (D.ListIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _ | (D.ListIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _ | (D.ListIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _ + | (D.ListIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _ | (D.ArrayIntIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _ | (D.ArrayIntIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _ | (D.ArrayIntIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _ | (D.ArrayIntIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _ + | (D.ArrayIntIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _ | (D.ArrayVarIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _ | (D.ArrayVarIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _ | (D.ArrayVarIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _ + | (D.ArrayVarIndex _ :: _, _) :: _, (D.AbstractTypeIndex _ :: _, _) :: _ + + | (D.AbstractTypeIndex _ :: _, _) :: _, (D.RecordIndex _ :: _, _) :: _ + | (D.AbstractTypeIndex _ :: _, _) :: _, (D.TupleIndex _ :: _, _) :: _ + | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ListIndex _ :: _, _) :: _ + | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ArrayIntIndex _ :: _, _) :: _ + | (D.AbstractTypeIndex _ :: _, _) :: _, (D.ArrayVarIndex _ :: _, _) :: _ | (_ :: _, _) :: _, ([], _) :: _ | ([], _) :: _, (_ :: _, _) :: _ -> @@ -2589,7 +2603,15 @@ and eval_node_decl (** Handle declaration and return context. *) and declaration_to_context ctx = function (* Declaration of a type as alias or free *) -| A.TypeDecl (pos, A.AliasType (_, i, type_expr)) -> +| A.TypeDecl (pos, type_rhs) -> + + let (i, type_expr) = match type_rhs with + (* Replace type aliases with their right-hand-side *) + | A.AliasType (_, i, type_expr) -> (i, type_expr) + (* Replace free types with an abstract type with no user-accessible + * representation. *) + | A.FreeType (_, i) -> (i, A.AbstractType (pos, i)) + in (* Identifier of AST identifier *) let ident = I.mk_string_ident i in @@ -2870,11 +2892,6 @@ and declaration_to_context ctx = function (* Unsupported below *) (* ******************************************************************** *) -(* Identifier is a free type *) -| A.TypeDecl (pos, (A.FreeType _)) -> - - C.fail_at_position pos "Free types not supported" - (* Parametric node declaration *) | A.NodeParamInst (pos, _) diff --git a/src/lustre/lustreIndex.ml b/src/lustre/lustreIndex.ml index be667c8f7..dd595f13f 100644 --- a/src/lustre/lustreIndex.ml +++ b/src/lustre/lustreIndex.ml @@ -43,6 +43,9 @@ type one_index = (* Array field indexed by variable *) | ArrayVarIndex of E.expr + (* Index to the representation field of an abstract type *) + | AbstractTypeIndex of string + (* Pretty-print a single index *) let pp_print_one_index' db = function @@ -54,7 +57,8 @@ let pp_print_one_index' db = function | TupleIndex i -> Format.fprintf ppf "<%d>" i | ListIndex i -> Format.fprintf ppf "{%d}" i | ArrayIntIndex i -> Format.fprintf ppf "[%d]" i - | ArrayVarIndex v -> ()) (* Format.fprintf ppf "[X%d(%a)]" db (E.pp_print_expr false) v ) *) + | ArrayVarIndex v -> () (* Format.fprintf ppf "[X%d(%a)]" db (E.pp_print_expr false) v ) *) + | AbstractTypeIndex i -> ()) | true -> @@ -63,7 +67,8 @@ let pp_print_one_index' db = function | TupleIndex i -> Format.fprintf ppf "_%d" i | ListIndex i -> Format.fprintf ppf "_%d" i | ArrayIntIndex i -> Format.fprintf ppf "_%d" i - | ArrayVarIndex v -> Format.fprintf ppf "_X%d" db) + | ArrayVarIndex v -> Format.fprintf ppf "_X%d" db + | AbstractTypeIndex i -> Format.fprintf ppf ".%s" i) (* Pretty-print a list of single indexes, given the number of previously seen *) @@ -106,7 +111,8 @@ type index = one_index list let compare_one_index a b = match a, b with (* Use polymorphic comparison on strings and integers *) - | RecordIndex a, RecordIndex b -> Pervasives.compare a b + | RecordIndex a, RecordIndex b + | AbstractTypeIndex a, AbstractTypeIndex b -> Pervasives.compare a b | TupleIndex a, TupleIndex b | ListIndex a, ListIndex b | ArrayIntIndex a, ArrayIntIndex b -> Pervasives.compare a b @@ -118,38 +124,51 @@ let compare_one_index a b = match a, b with | RecordIndex _, TupleIndex _ | RecordIndex _, ListIndex _ | RecordIndex _, ArrayIntIndex _ - | RecordIndex _, ArrayVarIndex _ -> 1 + | RecordIndex _, ArrayVarIndex _ + | RecordIndex _, AbstractTypeIndex _ -> 1 (* Tuple indexes are only smaller than record indexes *) | TupleIndex _, RecordIndex _ -> -1 | TupleIndex _, ListIndex _ | TupleIndex _, ArrayIntIndex _ - | TupleIndex _, ArrayVarIndex _ -> 1 + | TupleIndex _, ArrayVarIndex _ + | TupleIndex _, AbstractTypeIndex _ -> 1 (* List indexes are smaller than tuple and record indexes *) | ListIndex _, RecordIndex _ | ListIndex _, TupleIndex _ -> -1 | ListIndex _, ArrayIntIndex _ - | ListIndex _, ArrayVarIndex _ -> 1 + | ListIndex _, ArrayVarIndex _ + | ListIndex _, AbstractTypeIndex _ -> 1 - (* Intger array indexes are only greater than array variables indexes *) + (* Intger array indexes are greater than array variables + * and abstract type indexes *) | ArrayIntIndex _, RecordIndex _ | ArrayIntIndex _, TupleIndex _ | ArrayIntIndex _, ListIndex _ -> -1 - | ArrayIntIndex _, ArrayVarIndex _ -> 1 + | ArrayIntIndex _, ArrayVarIndex _ + | ArrayIntIndex _, AbstractTypeIndex _ -> 1 - (* Array variable indexes are smallest *) + (* Array variable indexes are only greater than abstract type indexes *) | ArrayVarIndex _, RecordIndex _ | ArrayVarIndex _, ArrayIntIndex _ | ArrayVarIndex _, ListIndex _ | ArrayVarIndex _, TupleIndex _ -> -1 + | ArrayVarIndex _, AbstractTypeIndex _ -> 1 + (* Abstract type indexes are the smallest *) + | AbstractTypeIndex _, RecordIndex _ + | AbstractTypeIndex _, ArrayIntIndex _ + | AbstractTypeIndex _, ListIndex _ + | AbstractTypeIndex _, TupleIndex _ + | AbstractTypeIndex _, ArrayVarIndex _ -> -1 (* Equality of indexes *) let equal_one_index a b = match a,b with (* String indexes are equal if the strings are *) - | RecordIndex a, RecordIndex b -> a = b + | RecordIndex a, RecordIndex b + | AbstractTypeIndex a, AbstractTypeIndex b -> a = b (* Integer indexes are equal if the integers are *) | TupleIndex a, TupleIndex b @@ -255,6 +274,7 @@ let compatible_one_index i1 i2 = match i1, i2 with | ArrayIntIndex _, ArrayVarIndex _ | ArrayVarIndex _, ArrayIntIndex _ | ArrayVarIndex _, ArrayVarIndex _ -> true + | AbstractTypeIndex s1, AbstractTypeIndex s2 -> s1 = s2 | _ -> false let compatible_indexes = List.for_all2 compatible_one_index diff --git a/src/lustre/lustreIndex.mli b/src/lustre/lustreIndex.mli index 4b1b26ecc..fa8c4124e 100644 --- a/src/lustre/lustreIndex.mli +++ b/src/lustre/lustreIndex.mli @@ -57,6 +57,9 @@ type one_index = (** Variable as index of an array of given size *) | ArrayVarIndex of LustreExpr.expr + (* Index to the representation field of an abstract type *) + | AbstractTypeIndex of string + (** A sequence of indexes *) type index = one_index list diff --git a/src/lustre/lustreSimplify.ml b/src/lustre/lustreSimplify.ml index df1aae59e..d99099f75 100644 --- a/src/lustre/lustreSimplify.ml +++ b/src/lustre/lustreSimplify.ml @@ -905,9 +905,10 @@ let rec eval_ast_expr bounds ctx = pos "Invalid index for expression" - (* Cannot be record, list or empty index *) + (* Cannot be record, list, abstract type or empty index *) | D.RecordIndex _ :: _, _ | D.ListIndex _ :: _, _ + | D.AbstractTypeIndex _ :: _, _ | [], _ -> C.fail_at_position @@ -1210,7 +1211,8 @@ let rec eval_ast_expr bounds ctx = (* Projection from a tuple expression *) | D.TupleIndex _ :: _, _ | D.RecordIndex _ :: _, _ - | D.ListIndex _ :: _, _ -> + | D.ListIndex _ :: _, _ + | D.AbstractTypeIndex _ :: _, _ -> (* Try again underneath *) @@ -1625,7 +1627,8 @@ and eval_ast_projection bounds ctx pos expr = function (* Cannot project array field this way, need to use select operator *) | D.ListIndex _ - | D.ArrayVarIndex _ -> raise (Invalid_argument "eval_ast_projection") + | D.ArrayVarIndex _ + | D.AbstractTypeIndex _ -> raise (Invalid_argument "eval_ast_projection") and try_eval_node_call bounds ctx pos ident cond restart args defaults = @@ -2118,6 +2121,14 @@ and eval_ast_type ctx = function Deps.Unknown_decl (Deps.Type, ident, pos) |> raise ) + (* User-defined abstract types are represented as an integer reference + * to an object. This reference is wrapped inside an index for that type + * so it cannot be used as a raw integer. + * There are abstract types in Type, but using an integer reference is able + * to give better counterexamples. *) + | A.AbstractType (pos, ident) -> + D.singleton [D.AbstractTypeIndex ident] Type.t_int + (* Record type, return trie of indexes in record *) | A.RecordType (pos, record_fields) -> diff --git a/tests/regression/error/abstract_type.lus b/tests/regression/error/abstract_type.lus new file mode 100644 index 000000000..dd049b010 --- /dev/null +++ b/tests/regression/error/abstract_type.lus @@ -0,0 +1,9 @@ +(* Check type checking for abstract types*) +type COUNTER; + +node test (const init : COUNTER) returns (out : int) ; +let + (* Type error *) + out = init + 1; +tel + diff --git a/tests/regression/falsifiable/abstract_type.lus b/tests/regression/falsifiable/abstract_type.lus new file mode 100644 index 000000000..75df58106 --- /dev/null +++ b/tests/regression/falsifiable/abstract_type.lus @@ -0,0 +1,19 @@ +(* An abstract / free type with axiomatised operations *) +type COUNTER; + +(* Operation to get counter value *) +function imported get_counter (in: COUNTER) returns (out: int) ; + +(* Increment a counter -- the new one is bigger than the old one *) +function imported increment (in: COUNTER) returns (out: COUNTER) ; +(*@contract + guarantee get_counter(out) = get_counter(in) + 1 ; +*) + +(* Try to prove that incrementing the counter does nothing... *) +node test (const init : COUNTER) returns (c : COUNTER) ; +let + c = init -> increment(pre c); + --%PROPERTY true -> (get_counter(c) = get_counter(pre c)); +tel + diff --git a/tests/regression/success/abstract_type.lus b/tests/regression/success/abstract_type.lus new file mode 100644 index 000000000..030636233 --- /dev/null +++ b/tests/regression/success/abstract_type.lus @@ -0,0 +1,29 @@ +(* An abstract / free type with axiomatised operations *) +type COUNTER; + +(* Operation to get counter value *) +function imported get_counter (in: COUNTER) returns (out: int) ; + +(* Increment a counter -- the new one is bigger than the old one *) +function imported increment (in: COUNTER) returns (out: COUNTER) ; +(*@contract + guarantee get_counter(out) = get_counter(in) + 1 ; +*) + +(* Construct a new counter *) +function imported zero () returns (out: COUNTER) ; +(*@contract + guarantee get_counter(out) = 0 ; +*) + +(* Prove that incrementing the counter works... *) +node test (const init : COUNTER) returns (c : COUNTER) ; +let + c = init -> increment(pre c); + --%PROPERTY true -> (get_counter(c) > get_counter(pre c)); + --%PROPERTY get_counter(init) >= 0 => get_counter(c) >= 0; + (* An example of a property that fails: *) + (* --%PROPERTY get_counter(init) >= 0 => get_counter(c) = get_counter(init); *) + (* An example of a property that should not typecheck: *) + (* --%PROPERTY get_counter(init) >= 0 => get_counter(c) = init; *) +tel