From 449e8a54371b0c707bb7e3c5acdb4fd475a016d0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 3 May 2018 11:03:27 +0100 Subject: Work in progress on the coq backend - originally based on the Lem backend - added externs to some of the library files and tests - added wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to return the valspec with the function's original names for bound type variables Note that most of the tests will fail currently --- lib/flow.sail | 42 +++++++++++++++++++++--------------------- lib/vector_dec.sail | 3 ++- 2 files changed, 23 insertions(+), 22 deletions(-) (limited to 'lib') diff --git a/lib/flow.sail b/lib/flow.sail index ef213ada..cd3665b4 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -1,33 +1,33 @@ $ifndef _FLOW $define _FLOW -val not_bool = "not" : bool -> bool -val and_bool = "and_bool" : (bool, bool) -> bool -val or_bool = "or_bool" : (bool, bool) -> bool +val not_bool = {coq: "negb", _: "not"} : bool -> bool +val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool +val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool -val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool function neq_atom (x, y) = not_bool(eq_atom(x, y)) -val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool -val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool -val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool - -val lt_range_atom = "lt" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val lteq_range_atom = "lteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val gt_range_atom = "gt" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val gteq_range_atom = "gteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool -val lt_atom_range = "lt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val gt_atom_range = "gt" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool - -val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool -val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : (int, int) -> bool -val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool"} : (bool, bool) -> bool +val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool + +val lt_range_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lteq_range_atom = {coq: "Z.lte", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gt_range_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val gteq_range_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool +val lt_atom_range = {coq: "Z.ltb", _: "lt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val lteq_atom_range = {coq: "Z.leb", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gt_atom_range = {coq: "Z.gtb", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool +val gteq_atom_range = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool + +val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool +val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool +val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool function neq_range (x, y) = not_bool(eq_range(x, y)) diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index eb2c9b7e..1307bb56 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -15,7 +15,7 @@ val eq_bits = { overload operator == = {eq_bit, eq_bits} -val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) +val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n) val vector_length = { ocaml: "length", @@ -36,6 +36,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val truncate = { ocaml: "vector_truncate", lem: "vector_truncate", + coq: "vector_truncate", c: "truncate" } : forall 'm 'n, 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) -- cgit v1.2.3 From 3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 3 May 2018 15:30:55 +0100 Subject: Flow typing and l-expression changes for ASL parser 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ --- lib/smt.sail | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lib') diff --git a/lib/smt.sail b/lib/smt.sail index f8521a4a..ae672947 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -10,6 +10,8 @@ val div = { c: "div_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)} +overload operator / = {div} + val mod = { smt: "mod", ocaml: "modulus", @@ -17,6 +19,8 @@ val mod = { c: "mod_int" } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)} +overload operator % = {mod} + val abs_atom = { smt : "abs", ocaml: "abs_int", -- cgit v1.2.3 From c6710bb09c1d492b4434f0b3b375750275b4d4b5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 4 May 2018 17:46:10 +0100 Subject: Run ARM built-in tests for Lem backend (via OCaml) --- lib/vector_dec.sail | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib') diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 1307bb56..17603e03 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -68,11 +68,13 @@ val vector_update = { val add_bits = { ocaml: "add_vec", + lem: "add_vec", c: "add_bits" } : forall 'n. (bits('n), bits('n)) -> bits('n) val add_bits_int = { ocaml: "add_vec_int", + lem: "add_vec_int", c: "add_bits_int" } : forall 'n. (bits('n), int) -> bits('n) -- cgit v1.2.3 From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 8 May 2018 18:48:18 +0100 Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64 --- lib/elf.sail | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib') diff --git a/lib/elf.sail b/lib/elf.sail index e953839d..2d799d4d 100644 --- a/lib/elf.sail +++ b/lib/elf.sail @@ -3,11 +3,13 @@ $define _ELF val elf_entry = { ocaml: "Elf_loader.elf_entry", + lem: "elf_entry", c: "elf_entry" } : unit -> int val elf_tohost = { ocaml: "Elf_loader.elf_tohost", + lem: "elf_tohost", c: "elf_tohost" } : unit -> int -- cgit v1.2.3 From 0d56f6be9e2e437c570da05b1c8cdc25eb24912c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 9 May 2018 16:55:58 +0100 Subject: Fix an issue with C compilation --- lib/arith.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/arith.sail b/lib/arith.sail index fa091772..54ecdbbc 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,7 +5,7 @@ $include // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm. (atom('n), atom('m)) -> atom('n + 'm) val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int -- cgit v1.2.3