From 5951a300d8f3e33430cf423c1e7a0b2fafb1fb92 Mon Sep 17 00:00:00 2001 From: hirataqdees Date: Sat, 28 Jul 2018 19:56:51 -0400 Subject: Update INSTALL.md adding sail's installation steps for macOS--- INSTALL.md | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 7a8a387b..51b97e81 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,32 +1,42 @@ -Installing Sail on Ubuntu +Installing Sail on Ubuntu and macOS ========================= This note lists the commands needed to get Sail and all dependencies -working on a new Ubuntu install. I recently (2018-02-17) tested these -on Xubuntu 16.04 LTS in a virtual machine, so they should +working on a new Ubuntu install or macOS. We have recently (2018-02-17) tested these +on Xubuntu 16.04 LTS in a virtual machine and on macOS Sierre 10.12.6, so they should work. Hopefully this will be useful as a reference. Basics ------ First we need some basic packages if they're not already installed. + +For Ubuntu: ``` sudo apt-get install build-essential git ``` +For macOS: compilers and supporting utilities are called Xcode instead of build-essential. First, download Xcode from the Mac App Store, and then run the following in the terminal: +``` +xcode-select --install +``` +git can be installed using ```brew install git``` + OCaml and sail expect some packages. m4 is for OPAM, libgmp-dev is for zarith which most of our tools rely on. Sail uses Z3 as a constraint solver. ``` sudo apt-get install m4 libgmp-dev z3 ``` +For macOS: ```brew install m4 gmp z3``` OCaml and OPAM -------------- Install OPAM. Either directly from [https://opam.ocaml.org] or from -the package manager - both should work, but I used the install script -from the website. This should install OCaml 4.05. +the package manager - both should work, but we used the install script +from the website. This should install OCaml 4.05. Don't forget to run +```opam init``` after installing OPAM. We now need ocamlbuild, zarith, and menhir from OPAM. ``` @@ -47,6 +57,8 @@ cd ott make cd .. ``` +Sail depends on ott, so add the ott executable (``` path-to-ott/bin```) in the $PATH. + Lem --- @@ -65,7 +77,7 @@ cd ../.. Linksem ------- -Make sure the LEMLIB environment variable is set correctly before building linksem. This should be the library directory within the checked-out lem directory. +Before installing linksem, we are required to set the LEMLIB environment variable and to put the lem executable in $PATH. LEMLIB should be the library directory within the checked-out lem directory (i.e. ```path-to-lem/library/```). Next, install linksem as ``` git clone git@github.com:rems-project/linksem.git -- cgit v1.2.3 From 63ce7e5fbc3ea28b6f2824f8c54c4049341097a4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 31 Jul 2018 11:58:01 +0100 Subject: Add Coq names for more Aarch64 builtins --- aarch64/prelude.sail | 55 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 33 insertions(+), 22 deletions(-) diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 65109485..5cf6b9f4 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -6,9 +6,9 @@ $include type bits ('n : Int) = vector('n, dec, bit) -val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool +val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool -val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool +val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string"} : (string, string) -> bool @@ -18,11 +18,12 @@ val eq_anything = { ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", - c: "eq_anything" + c: "eq_anything", + coq: "generic_eq" } : forall ('a : Type). ('a, 'a) -> bool val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) -val vector_length = {ocaml: "length", lem: "length_list", c: "length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) +val vector_length = {ocaml: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) val list_length = {ocaml: "length", lem: "length_list", c: "length"} : forall ('a : Type). list('a) -> int overload length = {bitvector_length, vector_length, list_length} @@ -32,7 +33,8 @@ overload operator == = {eq_bit, eq_vec, eq_string, eq_real, eq_anything} val vector_subrange_A = { ocaml: "subrange", lem: "subrange_vec_dec", - c: "vector_subrange" + c: "vector_subrange", + coq: "subrange_vec_dec" } : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) @@ -48,19 +50,22 @@ overload vector_subrange = {vector_subrange_A, vector_subrange_B} val bitvector_access_A = { ocaml: "access", lem: "access_vec_dec", - c: "vector_access" + c: "vector_access", + coq: "access_vec_dec" } : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. (bits('n), atom('m)) -> bit val bitvector_access_B = { ocaml: "access", lem: "access_vec_dec", - c: "vector_access" + c: "vector_access", + coq: "access_vec_dec" } : forall ('n : Int). (bits('n), int) -> bit val vector_access_A = { ocaml: "access", lem: "access_list_dec", - c: "vector_access" + c: "vector_access", + coq: "vec_access_dec" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a val vector_access_B = { @@ -71,10 +76,10 @@ val vector_access_B = { overload vector_access = {bitvector_access_A, bitvector_access_B, vector_access_A, vector_access_B} -val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update"} : forall 'n. +val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n. (bits('n), int, bit) -> bits('n) -val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update"} : forall 'n ('a : Type). +val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) overload vector_update = {bitvector_update_B, vector_update_B} @@ -82,13 +87,14 @@ overload vector_update = {bitvector_update_B, vector_update_B} val vector_update_subrange = { ocaml: "update_subrange", lem: "update_subrange_vec_dec", - c: "vector_update_subrange" + c: "vector_update_subrange", + coq: "update_subrange_vec_dec" } : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) val vcons : forall ('n : Int) ('a : Type). ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). @@ -108,7 +114,7 @@ val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) -val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool +val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool function neq_anything (x, y) = not_bool(x == y) @@ -134,7 +140,8 @@ val UInt = { ocaml: "uint", lem: "uint", interpreter: "uint", - c: "sail_unsigned" + c: "sail_unsigned", + coq: "uint" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val SInt = { @@ -202,7 +209,8 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string val xor_vec = { ocaml: "xor_vec", lem: "xor_vec", - c: "xor_bits" + c: "xor_bits", + coq: "xor_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n) val int_power = {lem: "pow"} : (int, int) -> int @@ -214,13 +222,15 @@ overload operator ^ = {xor_vec, int_power, real_power} val add_vec = { ocaml: "add_vec", lem: "add_vec", - c: "add_bits" + c: "add_bits", + coq: "add_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n) val add_vec_int = { ocaml: "add_vec_int", lem: "add_vec_int", - c: "add_bits_int" + c: "add_bits_int", + coq: "add_vec_int" } : forall 'n. (bits('n), int) -> bits('n) val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real"} : (real, real) -> real @@ -232,7 +242,8 @@ val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> val sub_vec_int = { ocaml: "sub_vec_int", lem: "sub_vec_int", - c: "sub_bits_int" + c: "sub_bits_int", + coq: "sub_vec_int" } : forall 'n. (bits('n), int) -> bits('n) val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real"} : (real, real) -> real @@ -277,11 +288,11 @@ val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat, val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real"} : (real, real) -> real -val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (int, int) -> int +val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int overload operator / = {quotient_nat, quotient, quotient_real} -val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int +val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int overload operator % = {modulus} @@ -289,11 +300,11 @@ val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> rea val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat -val min_int = {ocaml: "min_int", lem: "min", c: "min_int"} : (int, int) -> int +val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "min_int"} : (int, int) -> int val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat -val max_int = {ocaml: "max_int", lem: "max", c: "max_int"} : (int, int) -> int +val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "min_int"} : (int, int) -> int overload min = {min_nat, min_int} -- cgit v1.2.3 From f1ec636b83611f9d69e2a4d6ce34413399b73823 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 1 Aug 2018 14:26:12 +0100 Subject: Coq: implicit range conversions for function arguments, debug tracing The new option -dcoq_debug_on takes a list of functions to output tracing on. --- lib/coq/Sail2_values.v | 4 +++ src/pretty_print_coq.ml | 72 ++++++++++++++++++++++++++++++++++++++++--------- src/sail.ml | 3 +++ 3 files changed, 67 insertions(+), 12 deletions(-) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 0ce6134f..5752e6c0 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1036,6 +1036,10 @@ Qed. Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances. +Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x. + + + Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := { bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v)); of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v)); diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 713cfb34..5e3326bf 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -58,6 +58,7 @@ open Pretty_print_common module StringSet = Set.Make(String) let opt_undef_axioms = ref false +let opt_debug_on : string list ref = ref [] (**************************************************************************** * PPrint-based sail-to-coq pprinter @@ -69,6 +70,7 @@ type context = { kid_id_renames : id KBindings.t; (* tyvar -> argument renames *) bound_nexps : NexpSet.t; build_ex_return : bool; + debug : bool; } let empty_ctxt = { early_ret = false; @@ -76,8 +78,20 @@ let empty_ctxt = { kid_id_renames = KBindings.empty; bound_nexps = NexpSet.empty; build_ex_return = false; + debug = false; } +let debug_depth = ref 0 + +let rec indent n = match n with + | 0 -> "" + | n -> "| " ^ indent (n - 1) + +let debug ctxt m = + if ctxt.debug + then print_endline (indent !debug_depth ^ Lazy.force m) + else () + let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar @@ -763,12 +777,29 @@ let replace_atom_return_type ret_typ = true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l) | _ -> false, ret_typ +let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = + match argty, fnty with + | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp nexp,_)]), + Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); + Typ_arg_aux(Typ_arg_nexp high,_)]) -> + Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high)) + | Typ_exist (_, _, Typ_aux (Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp _,_)]), _)), + Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); + Typ_arg_aux(Typ_arg_nexp high,_)]) -> + Type_check.prove env (nc_eq low high) + | _ -> false let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = let rec top_exp (ctxt : context) (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) = + let top_exp c a e = + let () = debug_depth := !debug_depth + 1 in + let r = top_exp c a e in + let () = debug_depth := !debug_depth - 1 in + r + in let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in @@ -984,6 +1015,7 @@ let doc_exp_lem, doc_let_lem = parens (separate_map comma (expV false) args) in if aexp_needed then parens (align epp) else epp else + let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in let call, is_extern = if Env.is_extern f env "coq" then string (Env.get_extern f env "coq"), true @@ -996,33 +1028,44 @@ let doc_exp_lem, doc_let_lem = | _ -> [arg_typ], ret_typ, eff) | _ -> raise (Reporting_basic.err_unreachable l "Function not a function type") in + let inst = + match instantiation_of_without_type full_exp with + | x -> x + (* Not all function applications can be inferred, so try falling back to the + type inferred when we know the target type. + TODO: there are probably some edge cases where this won't pick up a need + to cast. *) + | exception _ -> instantiation_of full_exp + in + let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in + (* Insert existential unpacking of arguments where necessary *) let doc_arg arg typ_from_fn = let arg_pp = expY arg in - let arg_ty = expand_range_type (Env.expand_synonyms (env_of arg) (typ_of arg)) in - let typ_from_fn = expand_range_type (Env.expand_synonyms (env_of arg) typ_from_fn) in + let arg_ty_plain = Env.expand_synonyms (env_of arg) (typ_of arg) in + let arg_ty = expand_range_type arg_ty_plain in + let typ_from_fn_plain = subst_unifiers inst typ_from_fn in + let typ_from_fn_plain = Env.expand_synonyms (env_of arg) typ_from_fn_plain in + let typ_from_fn = expand_range_type typ_from_fn_plain in (* TODO: more sophisticated check *) + let () = + debug ctxt (lazy ("arg type found " ^ string_of_typ arg_ty_plain)); + debug ctxt (lazy ("arg type expected " ^ string_of_typ typ_from_fn_plain)) + in match destruct_exist env arg_ty, destruct_exist env typ_from_fn with | Some _, None -> parens (string "projT1 " ^^ arg_pp) (* Usually existentials have already been built elsewhere, but this is useful for (e.g.) ranges *) | None, Some _ -> parens (string "build_ex " ^^ arg_pp) + | Some _, Some _ when is_range_from_atom (env_of arg) arg_ty_plain typ_from_fn_plain -> + parens (string "to_range " ^^ parens (string "projT1 " ^^ arg_pp)) | _, _ -> arg_pp in let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in + (* Decide whether to unpack an existential result, pack one, or cast. To do this we compare the expected type stored in the checked expression with the inferred type. *) - let inst = - match instantiation_of_without_type full_exp with - | x -> x - (* Not all function applications can be inferred, so try falling back to the - type inferred when we know the target type. - TODO: there are probably some edge cases where this won't pick up a need - to cast. *) - | exception _ -> instantiation_of full_exp - in - let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in let ret_typ_inst = subst_unifiers inst ret_typ in @@ -1033,6 +1076,10 @@ let doc_exp_lem, doc_let_lem = let ret_typ_inst = if is_no_Z_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in + let () = + debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); + debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) + in let unpack, build_ex, in_typ, out_typ = match ret_typ_inst, ann_typ with | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) -> @@ -1639,6 +1686,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = kid_id_renames = kid_to_arg_rename; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); build_ex_return = effectful eff && build_ex; + debug = List.mem (string_of_id id) (!opt_debug_on) } in (* Put the constraints after pattern matching so that any type variable that's been replaced by one of the term-level arguments is bound. *) diff --git a/src/sail.ml b/src/sail.ml index e698090e..0b56ab21 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -146,6 +146,9 @@ let options = Arg.align ([ ( "-dcoq_warn_nonex", Arg.Set Rewrites.opt_coq_warn_nonexhaustive, "Generate warnings for non-exhaustive pattern matches in the Coq backend"); + ( "-dcoq_debug_on", + Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on), + " Produce debug messages for Coq output on given function"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); -- cgit v1.2.3 From 844bd43fe83ef1cad31baf3d3c56bc2b8511b43d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 11:25:53 +0100 Subject: Support for comment commands in emacs mode --- editors/sail2-mode.el | 3 +++ 1 file changed, 3 insertions(+) diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index dc851efd..b9d7ab06 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -54,6 +54,9 @@ (kill-all-local-variables) (set-syntax-table sail2-mode-syntax-table) (setq font-lock-defaults '(sail2-font-lock-keywords)) + (setq comment-start-skip "\\(//+\\|/\\*+\\)\\s *") + (setq comment-start "/*") + (setq comment-end "*/") (setq major-mode 'sail2-mode) (setq mode-name "Sail2") (run-hooks 'sail2-mode-hook)) -- cgit v1.2.3 From 5980711d118ad6d0c28644be605447c3dc82be64 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 11:52:04 +0100 Subject: Update a few prover gitignores --- lib/hol/.gitignore | 19 ++++++++++--------- lib/isabelle/.gitignore | 2 ++ 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore index fe652801..73d33f88 100644 --- a/lib/hol/.gitignore +++ b/lib/hol/.gitignore @@ -1,9 +1,10 @@ -prompt_monadScript.sml -promptScript.sml -sail_instr_kindsScript.sml -sail_operators_bitlistsScript.sml -sail_operators_mwordsScript.sml -sail_operatorsScript.sml -sail_valuesScript.sml -state_monadScript.sml -stateScript.sml +sail2_prompt_monadScript.sml +sail2_promptScript.sml +sail2_instr_kindsScript.sml +sail2_operators_bitlistsScript.sml +sail2_operators_mwordsScript.sml +sail2_operatorsScript.sml +sail2_valuesScript.sml +sail2_state_monadScript.sml +sail2_stateScript.sml +sail2_stringScript.sml diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore index ed83cdc1..fad6adbd 100644 --- a/lib/isabelle/.gitignore +++ b/lib/isabelle/.gitignore @@ -10,4 +10,6 @@ Sail2_valuesAuxiliary.thy Sail2_values.thy Sail2_stateAuxiliary.thy Sail2_state_monad.thy +Sail2_state_lifting.thy Sail2_state.thy +Sail2_string.thy \ No newline at end of file -- cgit v1.2.3 From 8a06df3ad1b90a355d3e5adb694002f00e67823e Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 15:58:45 +0100 Subject: Fill in more Coq builtins for aarch64 --- aarch64/prelude.sail | 18 ++++++++++-------- lib/coq/Sail2_values.v | 5 ++++- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 5cf6b9f4..a1bddec1 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -10,7 +10,7 @@ val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anythi val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string"} : (string, string) -> bool +val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real"} : (real, real) -> bool @@ -24,7 +24,7 @@ val eq_anything = { val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) val vector_length = {ocaml: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) -val list_length = {ocaml: "length", lem: "length_list", c: "length"} : forall ('a : Type). list('a) -> int +val list_length = {ocaml: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int overload length = {bitvector_length, vector_length, list_length} @@ -97,7 +97,7 @@ val vcons : forall ('n : Int) ('a : Type). val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) -val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). +val vector_concat = {ocaml: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) overload append = {bitvector_concat, vector_concat} @@ -105,7 +105,8 @@ overload append = {bitvector_concat, vector_concat} val not_vec = { ocaml: "not_vec", lem: "not_vec", - c: "not_bits" + c: "not_bits", + coq: "not_vec" } : forall 'n. bits('n) -> bits('n) overload ~ = {not_bool, not_vec} @@ -122,7 +123,7 @@ overload operator != = {neq_vec, neq_anything} val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val and_vec = {lem: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) function and_vec (xs, ys) = builtin_and_vec(xs, ys) @@ -130,7 +131,7 @@ overload operator & = {and_bool, and_vec} val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val or_vec = {lem: "or_vec", c: "or_bits"}: forall 'n. (bits('n), bits('n)) -> bits('n) +val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n) function or_vec (xs, ys) = builtin_or_vec(xs, ys) @@ -191,10 +192,11 @@ val putchar = { ocaml: "putchar", lem: "putchar", interpreter: "putchar", - c: "sail_putchar" + c: "sail_putchar", + coq: "putchar" } : int -> unit -val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str"} : (string, string) -> string +val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string val DecStr = "dec_str" : int -> string diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 5752e6c0..6fcbbb52 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y)) }. destruct (eqdec x y); simpl; split; congruence. -Qed. +Defined. + +Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := + Decidable_eq_from_dec String.string_dec. (* Project away range constraints in comparisons *) -- cgit v1.2.3 From 03dcb84bb8330cfa7b947ff4ecc0c5c9efca8ab0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 16:35:47 +0100 Subject: Coq: limit eauto to ensure termination in reasonable time --- lib/coq/Sail2_values.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 6fcbbb52..41414c96 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1020,7 +1020,7 @@ prepare_for_solver; solve [apply ArithFact_mword; assumption | constructor; omega with Z (* The datatypes hints give us some list handling, esp In *) - | constructor; eauto with datatypes zarith sail + | constructor; eauto 3 with datatypes zarith sail | constructor; idtac "Unable to solve constraint"; dump_context; fail]. Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. -- cgit v1.2.3 From 7dbc1523cdb82bdbfb9fea84b5afcdb4f6e829c2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 17:31:58 +0100 Subject: Coq: proper precedence for constraints (both prop and bool) --- src/pretty_print_coq.ml | 75 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 54 insertions(+), 21 deletions(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5e3326bf..d5925dc0 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -310,37 +310,70 @@ let drop_duplicate_atoms kids ty = | Typ_app _ -> Some full_typ in aux_typ ty -(* TODO: parens *) -let rec doc_nc_prop ctx (NC_aux (nc,_)) = +(* Follows Coq precedence levels *) +let rec doc_nc_prop ctx nc = + let rec l85 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) + | _ -> l80 nc_full + and l80 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) + | _ -> l70 nc_full + and l70 (NC_aux (nc,_) as nc_full) = match nc with | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2) | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_set (kid, is) -> (* TODO: is this a good translation? *) + | _ -> l10 nc_full + and l10 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_set (kid, is) -> separate space [string "In"; doc_var_lem ctx kid; brackets (separate (string "; ") (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) - | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2) | NC_true -> string "True" | NC_false -> string "False" - -(* TODO: parens *) -let rec doc_nc_exp ctx (NC_aux (nc,_)) = - match nc with - | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) - | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)) - | NC_set (kid, is) -> (* TODO: is this a good translation? *) - separate space [string "member_Z_list"; doc_var_lem ctx kid; - brackets (separate (string "; ") - (List.map (fun i -> string (Nat_big_num.to_string i)) is))] - | NC_or (nc1, nc2) -> doc_op (string "||") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2) - | NC_and (nc1, nc2) -> doc_op (string "&&") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2) - | NC_true -> string "true" - | NC_false -> string "false" + | NC_or _ + | NC_and _ + | NC_equal _ + | NC_bounded_ge _ + | NC_bounded_le _ + | NC_not_equal _ -> parens (l85 nc_full) + in l85 nc + +(* Follows Coq precedence levels *) +let doc_nc_exp ctx nc = + let rec l70 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2) + | _ -> l50 nc_full + and l50 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_or (nc1, nc2) -> doc_op (string "||") (l50 nc1) (l40 nc2) + | _ -> l40 nc_full + and l40 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_and (nc1, nc2) -> doc_op (string "&&") (l40 nc1) (l10 nc2) + | _ -> l10 nc_full + and l10 (NC_aux (nc,_) as nc_full) = + match nc with + | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)) + | NC_set (kid, is) -> + separate space [string "member_Z_list"; doc_var_lem ctx kid; + brackets (separate (string "; ") + (List.map (fun i -> string (Nat_big_num.to_string i)) is))] + | NC_true -> string "true" + | NC_false -> string "false" + | NC_equal _ + | NC_bounded_ge _ + | NC_bounded_le _ + | NC_or _ + | NC_and _ -> parens (l70 nc_full) + in l70 nc let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = match typ with -- cgit v1.2.3 From d2a01be233f1ea4bed66819096949aa4f56b2695 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 18:15:02 +0100 Subject: Coq: remove type removal holdover from Lem backend, add MIPS lemma --- mips/mips_extras.v | 9 +++++++++ src/pretty_print_coq.ml | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 6a6aed5c..8ca4546c 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -160,3 +160,12 @@ Definition prerr_string (_:string) : unit := tt. Definition putchar {T} (_:T) : unit := tt. Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). + + +Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * size รท 8). +intros. +rewrite Z.mul_comm. +rewrite Z.quot_mul; auto with zarith. +Qed. +Hint Resolve MEMr_wrapper_lemma : sail. + diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d5925dc0..93a24f4e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1311,7 +1311,7 @@ let doc_exp_lem, doc_let_lem = let epp = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in let middle = - match fst (untyp_pat pat) with + match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) -> -- cgit v1.2.3 From 430cf3778555fd9dfef5dccb3f57052df994cbc4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Aug 2018 18:16:45 +0100 Subject: Coq mips: fix deprecation warning --- mips/mips_extras.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 8ca4546c..626b4109 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -143,7 +143,7 @@ Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 refine (existT _ (ZEuclid.modulo m n) _). constructor. destruct H. -assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. } +assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } rewrite <- H at 3. lapply (ZEuclid.mod_always_pos m n); omega. Qed. -- cgit v1.2.3 From 967909c0df6808f09220d5cd22faf23f546be6ef Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Thu, 2 Aug 2018 20:52:29 -0700 Subject: fix some typos --- doc/tutorial.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/tutorial.tex b/doc/tutorial.tex index d325dc4d..5bd32c67 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -69,7 +69,7 @@ defined in the Sail library. These declarations work much like FFI bindings in many programming languages---in Sail we provide the \ll{val} declaration, except rather than giving a function body we supply a string used to identify the external operator in each -backend. For example, we could link the \ll{>>} operator with the +backend. For example, we could link the \ll{<<} operator with the \verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the external function has the same name as the sail function, such as \ll{shiftl = "shiftl"}, then we can use the shorthand syntax @@ -419,7 +419,7 @@ match ys { Like OCaml, Sail also supports naming parts of patterns using the \ll{as} keyword. For example, in the above list pattern we could bind -the entire list as ys as follows: +the entire list as zs as follows: \begin{lstlisting} match ys { x :: xs as zs => print("cons with as pattern"), @@ -869,7 +869,7 @@ val div2 : (int, int) -> option(int) \end{lstlisting} The first guarantees that if the first argument is greater than or equal to zero, and the second argument is greater than zero, then the -result will be greater than or not equal to zero. If we overload these +result will be greater than or equal to zero. If we overload these definitions as \begin{lstlisting} overload operator / = {div1, div2} -- cgit v1.2.3 From 2cb15665392d0b87da9e0c1f43e19267f28c3a82 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Aug 2018 14:52:44 +0100 Subject: Coq: generalise dependent pair handling a little 1. for monadic values (not in a terribly useful way, though) 2. for more types --- lib/coq/Sail2_prompt.v | 10 ++++++++++ lib/coq/Sail2_values.v | 2 +- src/pretty_print_coq.ml | 9 ++++++--- 3 files changed, 17 insertions(+), 4 deletions(-) diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index c98e2926..0b3a2cd8 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -115,3 +115,13 @@ let rec untilM vars cond body = write_reg r1 r1_v >> write_reg r2 r2_v*) *) + +(* If we need to build an existential after a monadic operation, assume that + we can do it entirely from the type. *) + +Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e := + x >>= fun y => returnm (existT _ y (H y)). + +Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e := + x >>= fun y => returnm (projT1 y). + diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 41414c96..acd11b45 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -21,7 +21,7 @@ Lemma use_ArithFact {P} `(ArithFact P) : P. apply fact. Defined. -Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} := +Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := existT _ n H. Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 93a24f4e..dff68092 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1133,10 +1133,13 @@ let doc_exp_lem, doc_let_lem = | _ -> false in unpack,build_ex,autocast in - let autocast_id = if effectful eff then "autocast_m" else "autocast" in - let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in + let autocast_id, proj_id, build_id = + if effectful eff + then "autocast_m", "projT1_m", "build_ex_m" + else "autocast", "projT1", "build_ex" in + let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in - let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in + let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> -- cgit v1.2.3 From baabef2bc2d39fc47ba47cd2ac5305856dd212a2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Aug 2018 15:04:18 +0100 Subject: Coq: use a dummy constraint when the real one is unknown Not really what we want, but a useful placeholder because of the widespread use of ex_int. --- lib/coq/Sail2_values.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index acd11b45..e4fff741 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1017,7 +1017,8 @@ Ltac prepare_for_solver := Ltac solve_arithfact := prepare_for_solver; (*dump_context;*) - solve [apply ArithFact_mword; assumption + solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end + | apply ArithFact_mword; assumption | constructor; omega with Z (* The datatypes hints give us some list handling, esp In *) | constructor; eauto 3 with datatypes zarith sail -- cgit v1.2.3 From bcb0bb41b9b0058ec03383cc27ec0ef613511c65 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 3 Aug 2018 16:50:31 +0100 Subject: Fix existential variable problems in monomorphisation One due to using raw types from the type checker in casts without trying to turn them into sane types, the other due to forgetting to use the constraint when trying to simplify sizes in existential types. Both triggered because the type checker now records more specific types. --- src/monomorphise.ml | 99 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 68 insertions(+), 31 deletions(-) diff --git a/src/monomorphise.ml b/src/monomorphise.ml index adc4d6d2..e9e2c6b6 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3167,13 +3167,15 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = | None -> r | Some (tenv,typ,_) -> let typ = Env.base_typ_of tenv typ in - let env, typ = + let env, tenv, typ = match destruct_exist tenv typ with - | None -> env, typ + | None -> env, tenv, typ | Some (kids, nc, typ) -> { env with kid_deps = List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids }, - typ + Env.add_constraint nc + (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids), + typ in if is_bitvector_typ typ then let size,_,_ = vector_typ_args_of typ in @@ -3644,6 +3646,14 @@ let is_constant_vec_typ env typ = let rewrite_app env typ (id,args) = let is_append = is_id env (Id "append") in + let try_cast_to_typ (E_aux (e,_) as exp) = + let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in + match size with + | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp) + | _ -> match solve env size with + | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp) + | None -> e + in if is_append id then let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in @@ -3661,14 +3671,23 @@ let rewrite_app env typ (id,args) = not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_app (append, - [e1; - E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "subrange_subrange_concat", - [vector1; start1; end1; vector2; start2; end2]), - (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + | _ -> + E_app (append, + [e1; + E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))]) + end | [E_aux (E_app (append, [e1; E_aux (E_app (slice1, @@ -3680,14 +3699,23 @@ let rewrite_app env typ (id,args) = not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_app (append, - [e1; - E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]), - (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + E_app (append, + [e1; + E_aux (E_cast (midtyp, + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,empty_tannot))),(Unknown,empty_tannot))]) + | _ -> + E_app (append, + [e1; + E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]), + (Unknown,empty_tannot))]) + end (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, @@ -3696,10 +3724,10 @@ let rewrite_app env typ (id,args) = [vector2; start2; end2]),_)] when is_subrange subrange1 && is_subrange subrange2 && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> - E_cast (typ, - E_aux (E_app (mk_id "subrange_subrange_concat", - [vector1; start1; end1; vector2; start2; end2]), - (Unknown,empty_tannot))) + try_cast_to_typ + (E_aux (E_app (mk_id "subrange_subrange_concat", + [vector1; start1; end1; vector2; start2; end2]), + (Unknown,empty_tannot))) (* variable-slice @ variable-slice *) | [E_aux (E_app (slice1, @@ -3708,9 +3736,9 @@ let rewrite_app env typ (id,args) = [vector2; start2; length2]),_)] when is_slice slice1 && is_slice slice2 && not (is_constant length1 || is_constant length2) -> - E_cast (typ, - E_aux (E_app (mk_id "slice_slice_concat", - [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) + try_cast_to_typ + (E_aux (E_app (mk_id "slice_slice_concat", + [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) | [E_aux (E_app (append1, [e1; @@ -3721,16 +3749,25 @@ let rewrite_app env typ (id,args) = not (is_constant length1 || is_constant length2) -> let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in - let midsize = nminus size size1 in - let midtyp = vector_typ midsize order bittyp in - E_cast (typ, - E_aux (E_app (mk_id "append", + let midsize = nminus size size1 in begin + match solve env midsize with + | Some c -> + let midtyp = vector_typ (nconstant c) order bittyp in + try_cast_to_typ + (E_aux (E_app (mk_id "append", [e1; E_aux (E_cast (midtyp, E_aux (E_app (mk_id "slice_zeros_concat", [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]), (Unknown,empty_tannot))) - + | _ -> + try_cast_to_typ + (E_aux (E_app (mk_id "append", + [e1; + E_aux (E_app (mk_id "slice_zeros_concat", + [vector1; start1; length1; length2]),(Unknown,empty_tannot))]), + (Unknown,empty_tannot))) + end | _ -> E_app (id,args) else if is_id env (Id "eq_vec") id then -- cgit v1.2.3 From f9282ab5dec29d7ec99d473d013d32b41a0b8dbc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 11:02:09 +0100 Subject: Improve cast introduction for Lem Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types. --- lib/mono_rewrites.sail | 3 ++- src/monomorphise.ml | 65 ++++++++++++++++++++++++++++++++++++++----------- src/pretty_print_lem.ml | 35 ++++++++++++++------------ 3 files changed, 73 insertions(+), 30 deletions(-) diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index aa8d05cd..9e837e10 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v) /* This is generated internally to deal with case splits which reveal the size of a bitvector */ -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure /* Definitions for the rewrites */ diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e9e2c6b6..ab6d9e2d 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3912,7 +3912,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) = (* These functions add cast functions across case splits, so that when a bitvector size becomes known in sail, the generated Lem code contains a function call to change mword 'n to (say) mword ty16, and vice versa. *) -let make_bitvector_cast_fns env quant_kids src_typ target_typ = +let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ = let genunk = Generated Unknown in let fresh = let counter = ref 0 in @@ -3945,7 +3945,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = P_aux (P_id var,(Generated src_l,src_ann)), E_aux (E_cast (tar_typ', - E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), + E_aux (E_app (Id_aux (Id cast_name, genunk), [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))), (genunk, tar_ann)) | _ -> @@ -3971,12 +3971,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = (fun var exp -> let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)), - E_aux (E_app (Id_aux (Id "bitvector_cast",genunk), + E_aux (E_app (Id_aux (Id cast_name,genunk), [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)), exp),(genunk,exp_ann))), (fun (E_aux (_,(exp_l,exp_ann)) as exp) -> E_aux (E_cast (one_target_typ, - E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))), + E_aux (E_app (Id_aux (Id cast_name, genunk), [exp]), (Generated exp_l,tar_ann))), (Generated exp_l,tar_ann))) | _ -> (fun var exp -> @@ -3991,12 +3991,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ = (* TODO: bound vars *) let make_bitvector_env_casts env quant_kids (kid,i) exp = - let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in + let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in let locals = Env.get_locals env in Bindings.fold (fun var (mut,typ) exp -> if mut = Immutable then mk_cast var typ exp else exp) locals exp -let make_bitvector_cast_exp env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) exp +let make_bitvector_cast_exp cast_name env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns cast_name env quant_kids typ target_typ)) exp let rec extract_value_from_guard var (E_aux (e,_)) = match e with @@ -4023,6 +4023,12 @@ let fill_in_type env typ = subst_src_typ subst typ (* TODO: top-level patterns *) +(* TODO: proper environment tracking for variables. Currently we pretend that + we can print the type of a variable in the top-level environment, but in + practice they might be below a case split. Note that we'd also need to + provide some way for the Lem pretty printer to know what to use; currently + we just use two names for the cast, bitvector_cast_in and bitvector_cast_out, + to let the pretty printer know whether to use the top-level environment. *) let add_bitvector_casts (Defs defs) = let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = @@ -4039,13 +4045,13 @@ let add_bitvector_casts (Defs defs) = let body = match pat, guard with | P_aux (P_lit (L_aux (L_num i,_)),_), _ -> let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in - make_bitvector_cast_exp env quant_kids src_typ result_typ + make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ (make_bitvector_env_casts env quant_kids (kid,i) body) | P_aux (P_id var,_), Some guard -> (match extract_value_from_guard var guard with | Some i -> let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in - make_bitvector_cast_exp env quant_kids src_typ result_typ + make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ (make_bitvector_env_casts env quant_kids (kid,i) body) | None -> body) | _ -> @@ -4056,15 +4062,46 @@ let add_bitvector_casts (Defs defs) = E_aux (E_case (exp', List.map map_case cases),ann) | _ -> E_aux (e,ann) end + | E_if (e1,e2,e3) -> + let env = env_of_annot ann in + let result_typ = Env.base_typ_of env (typ_of_annot ann) in + let rec extract (E_aux (e,_)) = + match e with + | E_app (op, + ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] | + [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)])) + when string_of_id op = "eq_atom" -> + (match destruct_atom_nexp (env_of y) (typ_of y) with + | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] + | _ -> []) + | E_app (op, [x;y]) when string_of_id op = "and_bool" -> + extract x @ extract y + | _ -> [] + in + let insts = extract e1 in + let e2' = List.fold_left (fun body inst -> + make_bitvector_env_casts env quant_kids inst body) e2 insts in + let insts = List.fold_left (fun insts (kid,i) -> + KBindings.add kid (nconstant i) insts) KBindings.empty insts in + let src_typ = subst_src_typ insts result_typ in + let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in + E_aux (E_if (e1,e2',e3), ann) | E_return e' -> - E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) - (* TODO: (env_of_annot ann) isn't suitable, because it contains - constraints revealing the case splits involved; needs a more - subtle approach *) + E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann) | E_assign (LEXP_aux (lexp,lexp_annot),e') -> E_aux (E_assign (LEXP_aux (lexp,lexp_annot), - make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e')) + make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) (typ_of_annot lexp_annot) e'),ann) + | E_id id -> begin + let env = env_of_annot ann in + match Env.lookup_id id env with + | Local (Mutable, vtyp) -> + make_bitvector_cast_exp "bitvector_cast_in" top_env quant_kids + (fill_in_type (env_of_annot ann) (typ_of_annot ann)) + vtyp + (E_aux (e,ann)) + | _ -> E_aux (e,ann) + end | _ -> E_aux (e,ann) in let open Rewriter in @@ -4089,7 +4126,7 @@ let add_bitvector_casts (Defs defs) = let body = rewrite_body id quant_kids body_env ret_typ body in (* Also add a cast around the entire function clause body, if necessary *) let body = - make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body + make_bitvector_cast_exp "bitvector_cast_out" fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body in let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 75284418..bef54f05 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -65,8 +65,9 @@ let opt_mwords = ref false type context = { early_ret : bool; bound_nexps : NexpSet.t; + top_env : Env.t } -let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty } +let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty } let print_to_from_interp_value = ref false let langlebar = string "<|" @@ -328,10 +329,9 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_arg_order o -> empty in typ', atomic_typ -(* Check for variables in types that would be pretty-printed and are not - bound in the val spec of the function. *) +(* Check for variables in types that would be pretty-printed. *) let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = - NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps + lem_nexps_of_typ typ |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp)) let replace_typ_size ctxt env (Typ_aux (t,a)) = @@ -341,14 +341,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - let is_equal nexp = - prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> - match Type_check.solve env size with - | Some n -> mk_typ (nconstant n) - | None -> None + match Type_check.solve env size with + | Some n -> mk_typ (nconstant n) + | None -> + let is_equal nexp = + prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> None end | _ -> None @@ -760,8 +760,12 @@ let doc_exp_lem, doc_let_lem = let env = env_of full_exp in let t = Env.expand_synonyms env (typ_of full_exp) in let eff = effect_of full_exp in - if typ_needs_printed t - then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) + if typ_needs_printed t then + if Id.compare f (mk_id "bitvector_cast_out") <> 0 + then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) + (* TODO: coordinate with the code in monomorphise.ml to find the correct + typing environment to use *) + else (align (group (prefix 0 1 epp (doc_tannot_lem ctxt ctxt.top_env (effectful eff) t))), true) else (epp, aexp_needed) in liftR (if aexp_needed then parens (align taepp) else taepp) end @@ -1255,7 +1259,8 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = let pat,guard,exp,(l,_) = destruct_pexp pexp in let ctxt = { early_ret = contains_early_return exp; - bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in + bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); + top_env = env_of_annot annot } in let pats, bind = untuple_args_pat pat in let patspp = separate_map space (doc_pat_lem ctxt true) pats in let _ = match guard with -- cgit v1.2.3 From e9ac694490707b29cf68ca3aefce46331149c003 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 11:13:07 +0100 Subject: Fix propagation of overly-specific types in early_return rewrite --- src/rewrites.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/rewrites.ml b/src/rewrites.ml index 5ed174ea..0a8c8156 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4381,6 +4381,8 @@ let rewrite_defs_lem = [ ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); ("fix_val_specs", rewrite_fix_val_specs); + (* early_return currently breaks the types *) + ("recheck_defs", recheck_defs); ("remove_blocks", rewrite_defs_remove_blocks); ("letbind_effects", rewrite_defs_letbind_effects); ("remove_e_assign", rewrite_defs_remove_e_assign); -- cgit v1.2.3 From 88fbe39a24a9432a58bc9998130f0b075344ef4c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 7 Aug 2018 14:50:07 +0100 Subject: Lem: print more bitvector types Especially for return expressions, which fixes a test case --- src/pretty_print_lem.ml | 59 ++++++++++++++++++++++++++++--------------------- test/mono/castreq.sail | 3 ++- 2 files changed, 36 insertions(+), 26 deletions(-) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index bef54f05..e9e6befb 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -352,18 +352,21 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = end | _ -> None -let doc_tannot_lem ctxt env eff typ = - let of_typ typ = - let ta = doc_typ_lem typ in - if eff then string " : M " ^^ parens ta - else string " : " ^^ ta - in +let make_printable_type ctxt env typ = if contains_t_pp_var ctxt typ then match replace_typ_size ctxt env typ with - | None -> empty - | Some typ -> of_typ typ - else of_typ typ + | None -> None + | Some typ -> Some typ + else Some typ + +let doc_tannot_lem ctxt env eff typ = + match make_printable_type ctxt env typ with + | None -> empty + | Some typ -> + let ta = doc_typ_lem typ in + if eff then string " : M " ^^ parens ta + else string " : " ^^ ta let doc_lit_lem (L_aux(lit,l)) = match lit with @@ -495,8 +498,9 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with parens (separate comma_sp (List.map2 doc_elem typs pats)) | P_typ(typ,p) -> let doc_p = doc_pat_lem ctxt true p in - if contains_t_pp_var ctxt typ then doc_p - else parens (doc_op colon doc_p (doc_typ_lem typ)) + (match make_printable_type ctxt (env_of_annot (l,annot)) typ with + | None -> doc_p + | Some typ -> parens (doc_op colon doc_p (doc_typ_lem typ))) | P_vector pats -> let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in if apat_needed then parens ppp else ppp @@ -727,14 +731,16 @@ let doc_exp_lem, doc_let_lem = | [exp] -> let epp = separate space [string "early_return"; expY exp] in let aexp_needed, tepp = - if contains_t_pp_var ctxt (typ_of exp) || - contains_t_pp_var ctxt (typ_of full_exp) then - aexp_needed, epp - else - let tannot = separate space [string "MR"; - doc_atomic_typ_lem false (typ_of full_exp); - doc_atomic_typ_lem false (typ_of exp)] in - true, doc_op colon epp tannot in + match Util.option_bind (make_printable_type ctxt ctxt.top_env) + (Env.get_ret_typ (env_of exp)), + make_printable_type ctxt (env_of full_exp) (typ_of full_exp) with + | Some typ, Some full_typ -> + let tannot = separate space [string "MR"; + doc_atomic_typ_lem false full_typ; + doc_atomic_typ_lem false typ] in + true, doc_op colon epp tannot + | _ -> aexp_needed, epp + in if aexp_needed then parens tepp else tepp | _ -> raise (Reporting_basic.err_unreachable l "Unexpected number of arguments for early_return builtin") @@ -920,12 +926,15 @@ let doc_exp_lem, doc_let_lem = "pretty-printing non-constant sizeof expressions to Lem not supported")) | E_return r -> let ta = - if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r) - then empty - else separate space - [string ": MR"; - parens (doc_typ_lem (typ_of full_exp)); - parens (doc_typ_lem (typ_of r))] in + match Util.option_bind (make_printable_type ctxt ctxt.top_env) (Env.get_ret_typ (env_of full_exp)), + make_printable_type ctxt (env_of r) (typ_of r) with + | Some full_typ, Some r_typ -> + separate space + [string ": MR"; + parens (doc_typ_lem full_typ); + parens (doc_typ_lem r_typ)] + | _ -> empty + in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) | E_constraint _ -> string "true" | E_internal_value _ -> diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail index 3400d650..586aa54b 100644 --- a/test/mono/castreq.sail +++ b/test/mono/castreq.sail @@ -15,7 +15,8 @@ function extzv(v) = extz_vec(sizeof('m),v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) overload length = {bitvector_length} -- cgit v1.2.3 From e3933fd35222995a3b44015aa288fdf34696bc8a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 7 Aug 2018 15:47:21 +0100 Subject: Revert "Warnings: deal with all the deprecation warnings" One day we will be free from the 4.02.3 menace, but today is not that day. :( This should fix Sail on Jenkins This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414. --- src/latex.ml | 2 +- src/lem_interp/printing_functions.ml | 2 +- src/ocaml_backend.ml | 2 +- src/pretty_print_lem.ml | 2 +- src/process_file.ml | 6 +++--- src/rewriter.ml | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/latex.ml b/src/latex.ml index 39db43db..0520d074 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -126,7 +126,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l | Some l -> Printf.sprintf "\\label{%s}" l in let cmd = !opt_prefix_latex ^ prefix ^ cmd in - let lcmd = String.lowercase_ascii cmd in (* lowercase to avoid file names differing only by case *) + let lcmd = String.lowercase cmd in (* lowercase to avoid file names differing only by case *) if StringSet.mem lcmd !commands then latex_command ~label:label dir (cmd ^ "v") no_loc annot else diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index c17e879f..a5cb96ff 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -481,7 +481,7 @@ let rec instr_parms_to_string ps = let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s let instruction_to_string (name, parms) = - ((*pad 5*) (String.lowercase_ascii name)) ^ " " ^ instr_parms_to_string parms + ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms let print_backtrace_compact printer (IState(stack,_)) = List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack) diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 3e4dc650..236c4222 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -673,7 +673,7 @@ let ocaml_main spec sail_dir = with | End_of_file -> close_in chan; lines := List.rev !lines end; - (("open " ^ String.capitalize_ascii spec ^ ";;\n\n") :: !lines + (("open " ^ String.capitalize spec ^ ";;\n\n") :: !lines @ [ " zinitializze_registers ();"; if !opt_trace_ocaml then " Sail_lib.opt_trace := true;" else " ();"; " Printexc.record_backtrace true;"; diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index e9e6befb..d300f699 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -129,7 +129,7 @@ let doc_id_lem_ctor (Id_aux(i,_)) = | Id("nat") -> string "integer" | Id("Some") -> string "Just" | Id("None") -> string "Nothing" - | Id i -> string (fix_id false (String.capitalize_ascii i)) + | Id i -> string (fix_id false (String.capitalize i)) | DeIid x -> string (Util.zencode_string ("op " ^ x)) let deinfix = function diff --git a/src/process_file.ml b/src/process_file.ml index 5fdd3d24..958720ea 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -271,14 +271,14 @@ let output_lem filename libs defs = operators_module ] @ monad_modules in - let isa_thy_name = String.capitalize_ascii filename ^ "_lemmas" in + let isa_thy_name = String.capitalize filename ^ "_lemmas" in let isa_lemmas = separate hardline [ string ("theory " ^ isa_thy_name); string " imports"; string " Sail.Sail2_values_lemmas"; string " Sail.Sail2_state_lemmas"; - string (" " ^ String.capitalize_ascii filename); + string (" " ^ String.capitalize filename); string "begin"; string ""; State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs; @@ -292,7 +292,7 @@ let output_lem filename libs defs = open_output_with_check_unformatted (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) - (o, base_imports @ (String.capitalize_ascii types_module :: libs)) + (o, base_imports @ (String.capitalize types_module :: libs)) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; diff --git a/src/rewriter.ml b/src/rewriter.ml index 01ff62b1..6d88730d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -266,7 +266,7 @@ let vector_string_to_bit_list l lit = | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in let s_bin = match lit with - | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase_ascii s_hex))) + | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex))) | L_bin s_bin -> explode s_bin | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in -- cgit v1.2.3 From 991dd7696058770d384b2aee3be0097f9af8d35d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:16:41 +0100 Subject: Coq: a bit more handling of unknown constraints --- lib/coq/Sail2_values.v | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e4fff741..14ed0459 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1017,12 +1017,20 @@ Ltac prepare_for_solver := Ltac solve_arithfact := prepare_for_solver; (*dump_context;*) - solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end - | apply ArithFact_mword; assumption - | constructor; omega with Z - (* The datatypes hints give us some list handling, esp In *) - | constructor; eauto 3 with datatypes zarith sail - | constructor; idtac "Unable to solve constraint"; dump_context; fail]. + solve + [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end + | match goal with |- ArithFact (?x = ?y) => + (is_evar x || is_evar y); + (* compute to allow projections to remove proofs that might not be allowed in the evar *) + let x := eval cbn in x in + let y := eval cbn in y in + idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end + | apply ArithFact_mword; assumption + | constructor; omega with Z + (* The datatypes hints give us some list handling, esp In *) + | constructor; eauto 3 with datatypes zarith sail + | constructor; idtac "Unable to solve constraint"; dump_context; fail + ]. Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. Hint Unfold length_mword : sail. -- cgit v1.2.3 From 07cb99b638d118a23cc8610c6cffbf5834b0fa87 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:17:21 +0100 Subject: Coq: handle nats like ranges, not atoms --- src/pretty_print_coq.ml | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index dff68092..74d10f44 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -152,7 +152,6 @@ let doc_id id = string (string_id id) let doc_id_type (Id_aux(i,_)) = match i with | Id("int") -> string "Z" - | Id("nat") -> string "Z" | Id i -> string (fix_id false i) | DeIid x -> string (Util.zencode_string ("op " ^ x)) @@ -384,6 +383,11 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = let var = nvar kid in let nc = nc_and (nc_lteq low var) (nc_lteq var high) in Some (Typ_aux (Typ_exist ([kid], nc, atom_typ var),Parse_ast.Generated l)) + | Typ_id (Id_aux (Id "nat",_)) -> + let kid = mk_kid "n" in + let var = nvar kid in + Some (Typ_aux (Typ_exist ([kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var), + Generated l)) | _ -> None let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ) @@ -428,7 +432,8 @@ let doc_typ, doc_atomic_typ = | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in if atyp_needed then parens tpp else tpp - | Typ_app(Id_aux (Id "range", _), _) -> + | Typ_app(Id_aux (Id "range", _), _) + | Typ_id (Id_aux (Id "nat", _)) -> (match maybe_expand_range_type ty with | Some typ -> atomic_typ atyp_needed typ | None -> raise (Reporting_basic.err_unreachable l "Bad range type")) @@ -805,9 +810,6 @@ let replace_atom_return_type ret_typ = | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l) - | Typ_aux (Typ_id (Id_aux (Id "nat",_)),l) -> - let kid = mk_kid "_retval" in - true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l) | _ -> false, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -816,10 +818,6 @@ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); Typ_arg_aux(Typ_arg_nexp high,_)]) -> Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high)) - | Typ_exist (_, _, Typ_aux (Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp _,_)]), _)), - Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_); - Typ_arg_aux(Typ_arg_nexp high,_)]) -> - Type_check.prove env (nc_eq low high) | _ -> false let prefix_recordtype = true @@ -1618,10 +1616,6 @@ let rec atom_constraint ctxt (pat, typ) = | _ -> Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp))))) - | P_aux (P_id id, _), - Typ_aux (Typ_id (Id_aux (Id "nat",_)),_) -> - Some (bquote ^^ braces (string "ArithFact" ^^ space ^^ - parens (doc_op (string ">=") (doc_id id) (string "0")))) | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ) | _ -> None -- cgit v1.2.3 From 93b8618d2b1c14c58340eae4873632fb4d7c1a20 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:17:46 +0100 Subject: Coq: decompose dependent pairs at internal_plet as well as let --- src/pretty_print_coq.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 74d10f44..d55e226b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1315,9 +1315,11 @@ let doc_exp_lem, doc_let_lem = match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" - | P_aux (P_id id,_) -> + | P_aux (P_id id,_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) -> separate space [string ">>= fun"; doc_id id; bigarrow] - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] -- cgit v1.2.3 From 9368ae447257efea8b0af8725350e195b2bb9731 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 11:18:00 +0100 Subject: Coq: tidy up debugging messages --- src/pretty_print_coq.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d55e226b..4e2193c1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1080,8 +1080,8 @@ let doc_exp_lem, doc_let_lem = let typ_from_fn = expand_range_type typ_from_fn_plain in (* TODO: more sophisticated check *) let () = - debug ctxt (lazy ("arg type found " ^ string_of_typ arg_ty_plain)); - debug ctxt (lazy ("arg type expected " ^ string_of_typ typ_from_fn_plain)) + debug ctxt (lazy (" arg type found " ^ string_of_typ arg_ty_plain)); + debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn_plain)) in match destruct_exist env arg_ty, destruct_exist env typ_from_fn with | Some _, None -> parens (string "projT1 " ^^ arg_pp) @@ -1108,8 +1108,8 @@ let doc_exp_lem, doc_let_lem = if is_no_Z_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in let () = - debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); - debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) + debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); + debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in let unpack, build_ex, in_typ, out_typ = match ret_typ_inst, ann_typ with -- cgit v1.2.3 From 58f585cfd9b1f5fd7724fdcb71b46179524653ca Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 9 Aug 2018 15:28:38 +0100 Subject: Coq: debugging on top-level lets --- src/pretty_print_coq.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4e2193c1..90276cb3 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1929,6 +1929,7 @@ let doc_val pat exp = in let env = env_of exp in let typ = expand_range_type (Env.expand_synonyms env (typ_of exp)) in + let ctxt = { empty_ctxt with debug = List.mem (string_of_id id) (!opt_debug_on) } in let id, opt_unpack = match destruct_exist env typ with | None -> id, None @@ -1943,7 +1944,7 @@ let doc_val pat exp = let idpp = doc_id id in let basepp = group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^ - doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline + doc_exp_lem ctxt false exp ^^ dot) ^^ hardline in match opt_unpack with | None -> basepp ^^ hardline -- cgit v1.2.3 From f05a7be239c7063727dcb529821edc7db20d4812 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Thu, 9 Aug 2018 18:14:12 -0700 Subject: fix tutorial infix example The syntax for these directives requires the precedence first. E.g. a real world version of this in riscv/prelude.sail. --- doc/tutorial.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tutorial.tex b/doc/tutorial.tex index 5bd32c67..5a362c28 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -751,7 +751,7 @@ operator names. Operators may be left, right, or non-associative, and there are 10 different precedence levels, ranging from 0 to 9, with 9 binding the tightest. To declare the precedence of an operator, we use a fixity declaration like: \begin{lstlisting} -infix <=_u 4 +infix 4 <=_u \end{lstlisting} For left or right associative operators, we'd use the keywords \ll{infixl} or \ll{infixr} respectively. An operator can be used -- cgit v1.2.3 From 3f2205e552d850c5eb128f4763ea0e4016e43ad2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 10 Aug 2018 18:37:24 +0100 Subject: Coq: add some of string library --- lib/coq/Makefile | 2 +- lib/coq/Sail2_string.v | 16 ++++++++++++++++ src/process_file.ml | 1 + 3 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 lib/coq/Sail2_string.v diff --git a/lib/coq/Makefile b/lib/coq/Makefile index 97869e3c..99321aae 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,6 +1,6 @@ BBV_DIR=../../../bbv/theories -SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v +SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v new file mode 100644 index 00000000..8bd7f0a6 --- /dev/null +++ b/lib/coq/Sail2_string.v @@ -0,0 +1,16 @@ +Require Import Sail2_values. + +Definition string_sub (s : string) (start : Z) (len : Z) : string := + String.substring (Z.to_nat start) (Z.to_nat len) s. + +Definition string_startswith s expected := + let prefix := String.substring 0 (String.length expected) s in + generic_eq prefix expected. + +Definition string_drop s n := + let n := Z.to_nat n in + String.substring n (String.length s - n) s. + +Definition string_length s := Z.of_nat (String.length s). + +Definition string_append := String.append. \ No newline at end of file diff --git a/src/process_file.ml b/src/process_file.ml index 958720ea..96029587 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -309,6 +309,7 @@ let output_coq filename libs defs = let base_imports = [ "Sail2_instr_kinds"; "Sail2_values"; + "Sail2_string"; operators_module ] @ monad_modules in -- cgit v1.2.3 From 67b48947300cf4ac5f792dc31436cb241a4c7126 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Sun, 12 Aug 2018 15:23:22 +0100 Subject: Coq: handle enums in binders, make top-level patterns exhaustive --- src/pretty_print_coq.ml | 21 ++++++++++++++++----- src/rewriter.mli | 2 ++ src/rewrites.ml | 36 +++++++++++++++++++++++++++++++++++- 3 files changed, 53 insertions(+), 6 deletions(-) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 90276cb3..d5aa7151 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -105,6 +105,11 @@ let is_number_char c = c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' || c = '6' || c = '7' || c = '8' || c = '9' +let is_enum env id = + match Env.lookup_id id env with + | Enum _ -> true + | _ -> false + let rec fix_id remove_tick name = match name with | "assert" | "lsl" @@ -1316,10 +1321,12 @@ let doc_exp_lem, doc_let_lem = | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) -> + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) -> + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] @@ -1373,12 +1380,14 @@ let doc_exp_lem, doc_let_lem = (* Prefer simple lets over patterns, because I've found Coq can struggle to work out return types otherwise *) | LB_val(P_aux (P_id id,_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) -> + when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) && + not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) typ) -> + when Util.is_none (is_auto_decomposed_exist (env_of e) typ) && + not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) (top_exp ctxt false e) @@ -1730,7 +1739,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let exp_typ = Env.expand_synonyms env typ in match p with | P_id id - | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> + | P_typ (_,P_aux (P_id id,_)) + when Util.is_none (is_auto_decomposed_exist env exp_typ) && + not (is_enum env id) -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) | _ -> (used_a_pattern := true; diff --git a/src/rewriter.mli b/src/rewriter.mli index 3e582071..da4702b5 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -74,6 +74,8 @@ val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat +val rewrite_pexp : tannot rewriters -> tannot pexp -> tannot pexp + val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind val rewrite_def : tannot rewriters -> tannot def -> tannot def diff --git a/src/rewrites.ml b/src/rewrites.ml index 0a8c8156..825073b4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4043,7 +4043,10 @@ let rewrite_defs_realise_mappings (Defs defs) = (* Rewrite to make all pattern matches in Coq output exhaustive. - Assumes that guards, vector patterns, etc have been rewritten already. *) + Assumes that guards, vector patterns, etc have been rewritten already, + and the scattered functions have been merged. + Will add escape effect where a default is needed, so effects will + need recalculated afterwards. *) let opt_coq_warn_nonexhaustive = ref false @@ -4285,6 +4288,37 @@ let rewrite_case (e,ann) = end | _ -> E_aux (e,ann) +let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = + let id,fcl_ann = + match fcls with + | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann + | [] -> raise (Reporting_basic.err_unreachable (fst f_ann) + "Empty function") + in + let env = env_of_annot fcl_ann in + let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in + let rps = List.fold_left process_funcl [RP_any] fcls in + let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) -> + FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann)) + fcls in + match rps with + | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann) + | (example::_) -> + let _ = + if !opt_coq_warn_nonexhaustive + then Reporting_basic.print_err false false + (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in + + let l = Parse_ast.Generated Parse_ast.Unknown in + let p = P_aux (P_wild, (l, empty_tannot)) in + let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in + (* TODO: use an expression that specifically indicates a failed pattern match *) + let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in + let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in + + FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann) + + let rewrite = let alg = { id_exp_alg with e_aux = rewrite_case } in rewrite_defs_base -- cgit v1.2.3 From a8fc6f2480790149a689e58d55a9dd3d6818dd3c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 11:52:30 +0100 Subject: Coq: drop irrelevant definitions before constraint solving (which were slowing down RISCV unacceptably because dealing with the xlen max/min values is surprisingly expensive) --- lib/coq/Sail2_values.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 14ed0459..7766e6af 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -938,6 +938,11 @@ end. Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end. Ltac clear_non_Z_defns := repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end. +Ltac clear_irrelevant_defns := +repeat match goal with X := _ |- _ => + match goal with |- context[X] => idtac end || + match goal with _ : context[X] |- _ => idtac end || clear X +end. Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0). constructor. @@ -1005,6 +1010,7 @@ Ltac dump_context := match goal with |- ?X => idtac "Goal:" X end. Ltac prepare_for_solver := (*dump_context;*) + clear_irrelevant_defns; clear_non_Z_defns; extract_properties; repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end; -- cgit v1.2.3 From 0de3a32ed759773bf1e8ff4460d21371c0a715e8 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 13:37:59 +0100 Subject: Basic Coq support for RISC-V Note that constraints have been added to ensure that all bitvector types are inhabited. --- riscv/Makefile | 9 +++ riscv/prelude.sail | 56 +++++++++--------- riscv/riscv_extras.v | 162 +++++++++++++++++++++++++++++++++++++++++++++++++++ riscv/riscv_mem.sail | 4 +- 4 files changed, 201 insertions(+), 30 deletions(-) create mode 100644 riscv/riscv_extras.v diff --git a/riscv/Makefile b/riscv/Makefile index 4805c8b2..5093c41e 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -77,6 +77,14 @@ riscvScript.sml : riscv.lem riscv_extras.lem riscvTheory.uo riscvTheory.ui: riscvScript.sml Holmake riscvTheory.uo +COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail + +riscv.v riscv_types.v: $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS) +%.vo: %.v + coqc $(COQ_LIBS) $< +riscv.vo: riscv_types.vo riscv_extras.vo + # we exclude prelude.sail here, most code there should move to sail lib LOC_FILES:=$(SAIL_SRCS) main.sail include ../etc/loc.mk @@ -89,5 +97,6 @@ clean: -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml -rm -f platform_main.native platform coverage.native + -rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v -Holmake cleanAll ocamlbuild -clean diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 6eeda601..131162ec 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -134,7 +134,7 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) (' overload append = {bitvector_concat, vector_concat} -val not_bool = "not" : bool -> bool +val not_bool = {coq: "negb", _: "not"} : bool -> bool val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) @@ -158,7 +158,7 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} -val and_bool = "and_bool" : (bool, bool) -> bool +val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -168,7 +168,7 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys) overload operator & = {and_bool, and_vec} -val or_bool = "or_bool" : (bool, bool) -> bool +val or_bool = {coq: "orb", _:"or_bool"} : (bool, bool) -> bool val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -182,7 +182,7 @@ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) -val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) +val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm) val __SetSlice_bits = "set_slice" : forall 'n 'm. (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) @@ -191,16 +191,16 @@ val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int -val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) +val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w) -val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) +val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n) function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) val __raw_SetSlice_bits : forall 'n 'w. (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) -val __raw_GetSlice_bits : forall 'n 'w. +val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0. (atom('n), atom('w), bits('n), int) -> bits('w) val "shiftl" : forall 'm. (bits('m), int) -> bits('m) @@ -239,10 +239,10 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> r overload operator ^ = {xor_vec, int_power, real_power, concat_str} -val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p. +val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int +val add_int = {ocaml: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -252,10 +252,10 @@ val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} -val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. +val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val sub_int = {ocaml: "sub_int", lem: "integerMinus"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", lem: "integerMinus"} : (nat, nat) -> nat @@ -266,9 +266,9 @@ val "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real -val negate_range = {ocaml: "minus_big_int", lem: "integerNegate"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) +val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) -val negate_int = {ocaml: "minus_big_int", lem: "integerNegate"} : int -> int +val negate_int = {ocaml: "minus_big_int", lem: "integerNegate", coq: "Z.opp"} : int -> int val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real @@ -279,7 +279,7 @@ overload negate = {negate_range, negate_int, negate_real} val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) -val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int +val mult_int = {ocaml: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real @@ -287,25 +287,25 @@ overload operator * = {mult_range, mult_int, mult_real} val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real -val gteq_int = "gteq" : (int, int) -> bool +val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool overload operator >= = {gteq_atom, gteq_int, gteq_real} -val lteq_int = "lteq" : (int, int) -> bool +val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool overload operator <= = {lteq_atom, lteq_int, lteq_real} -val gt_int = "gt" : (int, int) -> bool +val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool overload operator > = {gt_atom, gt_int, gt_real} -val lt_int = "lt" : (int, int) -> bool +val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool @@ -315,7 +315,7 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int -val abs_int = {ocaml: "abs_int", lem: "abs"} : int -> int +val abs_int = {ocaml: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real @@ -365,25 +365,25 @@ function __RISCV_write (addr, width, data) = { val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm. +val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __RISCV_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} +val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} function __RISCV_read (addr, width, aq, rl, res) = match (aq, rl, res) { (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)), @@ -398,7 +398,7 @@ function __RISCV_read (addr, width, aq, rl, res) = val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) +val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm) val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} @@ -476,7 +476,7 @@ val vector64 : int -> bits(64) function vector64 n = __raw_GetSlice_int(64, n, 0) -val to_bits : forall 'l.(atom('l), int) -> bits('l) +val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v new file mode 100644 index 00000000..a3cb3fb9 --- /dev/null +++ b/riscv/riscv_extras.v @@ -0,0 +1,162 @@ +Require Import Sail2_instr_kinds. +Require Import Sail2_values. +Require Import Sail2_operators_mwords. +Require Import Sail2_prompt_monad. +Require Import Sail2_prompt. +Require Import String. +Require Import List. +Import List.ListNotations. + +Axiom real : Type. + +(* +val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e +val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e +*) +Definition MEMr {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_plain addr size. +Definition MEMr_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (mword b) e := read_mem Read_reserve addr size. + +(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*) +Definition read_tag_bool {regval a e} (addr : mword a) : monad regval bool e := + read_tag addr >>= fun t => + maybe_fail "read_tag_bool" (bool_of_bitU t). + +(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*) +Definition write_tag_bool {regval a e} (addr : mword a) t : monad regval unit e := + write_tag addr (bitU_of_bool t) >>= fun _ => returnm tt. + +Definition MEMr_tag {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := + read_mem Read_plain addr size >>= fun v => + read_tag_bool addr >>= fun t => + returnm (t, v). + +Definition MEMr_tag_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e := + read_mem Read_plain addr size >>= fun v => + read_tag_bool addr >>= fun t => + returnm (t, v). + +(* +val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e +*) +Definition MEMea {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. +Definition MEMea_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size. + +Definition MEMea_tag {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_plain addr size. +Definition MEMea_tag_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size. + +(* +val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e +val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e +val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e +val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e +*) +Definition MEMval {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => returnm tt. +Definition MEMval_conditional {regval a b e} (_ : mword a) (size : Z) (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => returnm (if b then true else false). +Definition MEMval_tag {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval unit e := write_mem_val v >>= fun _ => write_tag_bool addr t >>= fun _ => returnm tt. +Definition MEMval_tag_conditional {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => write_tag_bool addr t >>= fun _ => returnm (if b then true else false). + +(*val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e*) + +Definition MEM_sync {regval e} (_:unit) : monad regval unit e := barrier Barrier_MIPS_SYNC. + +(* Some wrappers copied from aarch64_extras *) +(* TODO: Harmonise into a common library *) +(* +Definition get_slice_int_bl len n lo := + (* TODO: Is this the intended behaviour? *) + let hi := lo + len - 1 in + let bs := bools_of_int (hi + 1) n in + subrange_list false bs hi lo + +val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a +Definition get_slice_int len n lo := of_bools (get_slice_int_bl len n lo) +*) +Definition write_ram {rv e} m size (hexRAM : mword m) (addr : mword m) (data : mword (8 * size)) : monad rv bool e := + write_mem_val data. + +Definition read_ram {rv e} m size `{ArithFact (size >= 0)} (_ : mword m) (addr : mword m) : monad rv (mword (8 * size)) e := + read_mem Read_plain addr size. +(* +Definition string_of_bits bs := string_of_bv (bits_of bs). +Definition string_of_int := show + +Definition _sign_extend bits len := maybe_failwith (of_bits (exts_bv len bits)) +Definition _zero_extend bits len := maybe_failwith (of_bits (extz_bv len bits)) +*) +Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a := + shiftl v (int_of_mword false n). + +Definition shift_bits_right {a b} (v : mword a) (n : mword b) : mword a := + shiftr v (int_of_mword false n). + +Definition shift_bits_right_arith {a b} (v : mword a) (n : mword b) : mword a := + arith_shiftr v (int_of_mword false n). + +(* Use constants for undefined values for now *) +Definition internal_pick {rv a e} (vs : list a) : monad rv a e := +match vs with +| (h::_) => returnm h +| _ => Fail "empty list in internal_pick" +end. +Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string. +Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. +Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). +(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) +Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >= 0)} : monad rv (vec a len) e := returnm (vec_init u len). +(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0). +(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) +Definition undefined_bits {rv e} := @undefined_bitvector rv e. +Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. +(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) +Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i). +Definition undefined_atom {rv e} i : monad rv Z e := returnm i. +Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). + +Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. + +(*val elf_entry : unit -> integer*) +Definition elf_entry (_:unit) : Z := 0. +(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*) + +(*Definition print_bits msg bs := prerr_endline (msg ^ (string_of_bits bs)) + +val get_time_ns : unit -> integer*) +Definition get_time_ns (_:unit) : Z := 0. +(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*) + +Definition eq_bit (x : bitU) (y : bitU) : bool := + match x, y with + | B0, B0 => true + | B1, B1 => true + | BU, BU => true + | _,_ => false + end. + +Require Import Zeuclid. +Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}. +apply existT with (x := ZEuclid.modulo m n). +constructor. +destruct H. +assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } +rewrite <- H at 3. +lapply (ZEuclid.mod_always_pos m n); omega. +Qed. + +(* Override the more general version *) + +Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. +Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 72b7e8da..9425c0ff 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -8,7 +8,7 @@ function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = match (t, __RISCV_read(addr, width, aq, rl, res)) { (Instruction, None()) => MemException(E_Fetch_Access_Fault), (Data, None()) => MemException(E_Load_Access_Fault), @@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) -- cgit v1.2.3 From 3001c5dbdfbd060500df141d8112af5c1021f347 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 13:52:50 +0100 Subject: Guarded clauses rewrite: variable patterns subsume enums Prevents redundant clauses. --- src/rewrites.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/rewrites.ml b/src/rewrites.ml index 825073b4..aee57977 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2 | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) -> if id1 = id2 then Some [] - else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound && - Env.lookup_id aid2 (env_of_annot annot2) = Unbound - then Some [(id2,id1)] else None + else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound + then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound + then Some [(id2,id1)] + else Some [] + else None | P_id id1, _ -> if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2 -- cgit v1.2.3 From 0fc1d90ebc7b6bda46e593893dc92acad896ae90 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 16:24:49 +0100 Subject: RISC-V: mult_range is ill-typed, use mult_atom instead --- riscv/prelude.sail | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 131162ec..5bc5be13 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -276,14 +276,14 @@ overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} overload negate = {negate_range, negate_int, negate_real} -val mult_range = {ocaml: "mult", lem: "integerMult"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) +val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n * 'm) val mult_int = {ocaml: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real -overload operator * = {mult_range, mult_int, mult_real} +overload operator * = {mult_atom, mult_int, mult_real} val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real @@ -496,7 +496,3 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = let v64 : bits(64) = EXTS(v) in (v64 >> shift)[31..0] - -/* Copied from arith.sail. */ -val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n * 'm) -- cgit v1.2.3 From 1f3253c106e40cbfe6ecd79b281b45abf708663b Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 16:25:18 +0100 Subject: Add constraints to RISC-V duopod, makefile rules --- riscv/Makefile | 4 ++++ riscv/riscv_duopod.sail | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/riscv/Makefile b/riscv/Makefile index 5093c41e..6499fe7d 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -81,9 +81,12 @@ COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail riscv.v riscv_types.v: $(SAIL_SRCS) $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS) +riscv_duopod.v riscv_duopod_types.v: prelude.sail riscv_duopod.sail + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv_duopod -coq_lib riscv_extras $^ %.vo: %.v coqc $(COQ_LIBS) $< riscv.vo: riscv_types.vo riscv_extras.vo +riscv_duopod.vo: riscv_duopod_types.vo riscv_extras.vo # we exclude prelude.sail here, most code there should move to sail lib LOC_FILES:=$(SAIL_SRCS) main.sail @@ -98,5 +101,6 @@ clean: -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml -rm -f platform_main.native platform coverage.native -rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v + -rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v -Holmake cleanAll ocamlbuild -clean diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail index ff1e4065..0a5a7f8c 100644 --- a/riscv/riscv_duopod.sail +++ b/riscv/riscv_duopod.sail @@ -5,7 +5,7 @@ type xlen_t = bits(64) type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) -val zeros : forall 'n. atom('n) -> bits('n) +val zeros : forall 'n, 'n >= 0. atom('n) -> bits('n) function zeros n = replicate_bits(0b0, n) val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} @@ -35,7 +35,7 @@ overload X = {rX, wX} /* Accessors for memory */ -val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr : forall 'n, 'n >= 0. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} function MEMr (addr, width) = match __RISCV_read(addr, width, false, false, false) { Some(v) => v, None() => zeros(8 * width) } -- cgit v1.2.3 From 616b770c1fef06b9b5322d0dfde729594abd279a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 16:50:38 +0100 Subject: Coq: drop redundant final wildcard clauses Deals with pattern matches generated from mappings, plus the occasional error. --- src/rewrites.ml | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/src/rewrites.ml b/src/rewrites.ml index aee57977..47c7e923 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4048,7 +4048,15 @@ let rewrite_defs_realise_mappings (Defs defs) = Assumes that guards, vector patterns, etc have been rewritten already, and the scattered functions have been merged. Will add escape effect where a default is needed, so effects will - need recalculated afterwards. *) + need recalculated afterwards. + + Also detects and removes redundant wildcard patterns at the end of the match. + (We could do more, but this is sufficient to deal with the code generated by + the mappings rewrites.) + + Note: if this naive implementation turns out to be too slow or buggy, we + could look at implementing Maranget JFP 17(3), 2007. + *) let opt_coq_warn_nonexhaustive = ref false @@ -4266,12 +4274,38 @@ let process_pexp env = raise (Reporting_basic.err_unreachable l "Guarded pattern should have been rewritten away") +(* We do some minimal redundancy checking to remove bogus wildcard patterns here *) +let check_cases process is_wild loc_of cases = + let rec aux rps acc = function + | [] -> acc, rps + | [p] when is_wild p && match rps with [] -> true | _ -> false -> + let () = Reporting_basic.print_err false false + (loc_of p) "Match checking" "Redundant wildcard clause" in + acc, [] + | h::t -> aux (process rps h) (h::acc) t + in + let cases, rps = aux [RP_any] [] cases in + List.rev cases, rps + +let pexp_is_wild = function + | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true + | _ -> false + +let pexp_loc = function + | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l + | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l + +let funcl_is_wild = function + | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp + +let funcl_loc (FCL_aux (_,(l,_))) = l + let rewrite_case (e,ann) = match e with | E_case (e1,cases) -> begin let env = env_of_annot ann in - let rps = List.fold_left (process_pexp env) [RP_any] cases in + let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in match rps with | [] -> E_aux (E_case (e1,cases),ann) | (example::_) -> @@ -4299,7 +4333,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = in let env = env_of_annot fcl_ann in let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in - let rps = List.fold_left process_funcl [RP_any] fcls in + let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) -> FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann)) fcls in -- cgit v1.2.3 From a3c66eb5bc5d98a8ce400e5c391e7d9db940c3a7 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 17:24:54 +0100 Subject: Coq: more strings for RISC-V --- lib/coq/Sail2_string.v | 27 +++++++++++++++++++++++---- riscv/riscv_extras.v | 4 ++-- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index 8bd7f0a6..9ca9cb67 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -7,10 +7,29 @@ Definition string_startswith s expected := let prefix := String.substring 0 (String.length expected) s in generic_eq prefix expected. -Definition string_drop s n := - let n := Z.to_nat n in +Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) := + let n := Z.to_nat (projT1 n) in String.substring n (String.length s - n) s. -Definition string_length s := Z.of_nat (String.length s). +Definition string_length s : {n : Z & ArithFact (n >= 0)} := + build_ex (Z.of_nat (String.length s)). -Definition string_append := String.append. \ No newline at end of file +Definition string_append := String.append. + +(* TODO: maybe_int_of_prefix, maybe_int_of_string *) + +Fixpoint n_leading_spaces (s:string) : nat := + match s with + | EmptyString => 0 + | String " " t => S (n_leading_spaces t) + | _ => 0 + end. + +Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) := + Some (tt, build_ex (Z.of_nat (n_leading_spaces s))). + +Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) := + match n_leading_spaces s with + | O => None + | S n => Some (tt, build_ex (Z.of_nat (S n))) + end. \ No newline at end of file diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v index a3cb3fb9..3f1fe7e0 100644 --- a/riscv/riscv_extras.v +++ b/riscv/riscv_extras.v @@ -124,9 +124,9 @@ Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. Definition elf_entry (_:unit) : Z := 0. (*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*) -(*Definition print_bits msg bs := prerr_endline (msg ^ (string_of_bits bs)) +Definition print_bits {n} msg (bs : mword n) := prerr_endline (msg ++ (string_of_bits bs)). -val get_time_ns : unit -> integer*) +(*val get_time_ns : unit -> integer*) Definition get_time_ns (_:unit) : Z := 0. (*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*) -- cgit v1.2.3 From 342cd6a5a02b0478d37f8cc25410106d2846d5b2 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 13 Aug 2018 18:05:21 +0100 Subject: More RISC-V built-in type constraints --- riscv/prelude.sail | 10 +++++----- riscv/riscv_mem.sail | 2 +- riscv/riscv_platform.sail | 4 ++-- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 5bc5be13..8636bda6 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -64,11 +64,11 @@ function def_spc_backwards s = () val def_spc_matches_prefix = "opt_spc_matches_prefix" : string -> option((unit, nat)) -val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool -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 eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> 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 eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 9425c0ff..7268e9cc 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 7ab83aa6..6e3dee93 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -85,7 +85,7 @@ let MSIP_BASE : xlenbits = 0x0000000000000000 let MTIMECMP_BASE : xlenbits = 0x0000000000004000 let MTIME_BASE : xlenbits = 0x000000000000bff8 -val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} function clint_load(addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ @@ -224,7 +224,7 @@ function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. b function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) -function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = +function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = if within_clint(addr, width) then clint_load(addr, width) else if within_htif_readable(addr, width) & (1 <= 'n) -- cgit v1.2.3