diff options
34 files changed, 1167 insertions, 421 deletions
@@ -28,8 +28,15 @@ lib/hol/sail-heap # Coq *.vo +*.vok +*.vos *.glob .*.aux +/lib/coq/.nia.cache + +# Isabelle + +/lib/isabelle/output # location specific things @@ -42,6 +49,7 @@ lib/hol/sail-heap /src/jib.ml /src/manifest.ml +/test/sailtest.pyc /test/typecheck/rtpass*/ /test/typecheck/tests.xml /test/lem/Out_lemmas.thy @@ -49,6 +57,19 @@ lib/hol/sail-heap /test/lem/out_types.lem /test/*/tests.xml /test/riscv/tests/*.iout +/test/smt/*.out +/test/smt/*.smt2 +/test/c/*.c +/test/c/*.result +/test/c/*.iresult +/test/c/*.oresult +/test/c/*.bin +/test/c/*_ocaml +/test/c/_sbuild* +/test/mono/Out_lemmas.thy +/test/mono/log +/test/mono/test.cmi +/test/mono/test.cmo /language/*.pdf /language/*.uo @@ -62,6 +83,11 @@ lib/hol/sail-heap /language/*.dvi /language/*.ps +/aarch64_small/ArmV8_lemmas.thy +/aarch64_small/armV8.lem +/aarch64_small/armV8.smt_model +/aarch64_small/armV8_types.lem + /aarch64/Aarch64.thy /aarch64/Aarch64Auxiliary.thy /aarch64/Aarch64_extras.thy @@ -8,4 +8,4 @@ S src/gen_lib/** S src/lem_interp/** S src/test/** B src/_build/** -PKG num str unix uint zarith linksem lem omd linenoise base64 yojson +PKG num str unix uint zarith linksem lem omd linenoise base64 yojson pprint diff --git a/lib/arith.sail b/lib/arith.sail index 58f25bbc..d57fd559 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -56,19 +56,21 @@ A common idiom in asl is to take two bits of an opcode and convert in into a var let elsize = shl_int(8, UInt(size)) ``` THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` + +Similarly, we define shifts of 32 and 1 (i.e., powers of two). */ val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} : forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)} -/*! -Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` -*/ val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} : forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)} +val _shl1 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} : + forall 'n, 0 <= 'n <= 3. (int(1), int('n)) -> {'m, 'm in {1, 2, 4, 8}. int('m)} + val _shl_int = "shl_int" : (int, int) -> int -overload shl_int = {_shl8, _shl32, _shl_int} +overload shl_int = {_shl1, _shl8, _shl32, _shl_int} val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} diff --git a/lib/coq/Makefile b/lib/coq/Makefile index d16191cb..806b0ff0 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,10 +1,10 @@ -BBV_DIR?=../../../bbv +BBV_DIR?=../../../bbv/src/bbv CORESRC=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_state_lifting.v Sail2_string.v Sail2_real.v PROOFSRC=Sail2_values_lemmas.v Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v SRC=$(CORESRC) $(PROOFSRC) -COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv +COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv TARGETS=$(SRC:.v=.vo) diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 98b7d077..848cd042 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -96,6 +96,14 @@ lemma PrePost_readS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value (f s)) lemma PrePost_updateS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value ()) (f s)) (updateS f) P" unfolding PrePost_def updateS_def returnS_def by auto +lemma PrePost_read_regS[intro, PrePost_atomI]: + "PrePost (\<lambda>s. P (Value (read_from reg (regstate s))) s) (read_regS reg) P" + unfolding read_regS_def by (rule PrePost_readS) + +lemma PrePost_write_regS[intro, PrePost_atomI]: + "PrePost (\<lambda>s. P (Value ()) (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) P" + unfolding write_regS_def by (rule PrePost_updateS) + lemma PrePost_if: assumes "b \<Longrightarrow> PrePost P f Q" and "\<not>b \<Longrightarrow> PrePost P g Q" shows "PrePost P (if b then f else g) Q" @@ -311,6 +319,14 @@ lemma PrePostE_readS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q (f s) s) ( lemma PrePostE_updateS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q () (f s)) (updateS f) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) +lemma PrePostE_read_regS[PrePostE_atomI, intro]: + "PrePostE (\<lambda>s. Q (read_from reg (regstate s)) s) (read_regS reg) Q E" + unfolding read_regS_def by (rule PrePostE_readS) + +lemma PrePostE_write_regS[PrePostE_atomI, intro]: + "PrePostE (\<lambda>s. Q () (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) Q E" + unfolding write_regS_def by (rule PrePostE_updateS) + lemma PrePostE_if_branch[PrePostE_compositeI]: assumes "b \<Longrightarrow> PrePostE Pf f Q E" and "\<not>b \<Longrightarrow> PrePostE Pg g Q E" shows "PrePostE (if b then Pf else Pg) (if b then f else g) Q E" diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 8be5cc6b..8fbcf093 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -122,22 +122,22 @@ lemma liftState_write_mem[liftState_simp]: by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp split: option.splits) -lemma liftState_read_reg_readS: +lemma liftState_read_reg: assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)" - shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \<circ> regstate)" + shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg" proof fix s :: "'a sequential_state" obtain rv v where "get_regval' (name reg) (regstate s) = Some rv" and "of_regval reg rv \<equiv> Some v" and "read_from reg (regstate s) = v" using assms unfolding bind_eq_Some_conv by blast - then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \<circ> regstate) s" + then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s" by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def) qed -lemma liftState_write_reg_updateS: +lemma liftState_write_reg: assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)" - shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))" - using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS) + shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v" + using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS write_regS_def) lemma liftState_iter_aux[liftState_simp]: shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs" diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 81d42663..0702b374 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -66,6 +66,12 @@ function slice_zeros_concat (xs, i, l, l') = { sail_shiftleft(extzv(l + l', xs), l') } +val subrange_zeros_concat : forall 'n 'hi 'lo 'q, 'n >= 0 & 'hi - 'lo + 1 + 'q >= 0. + (bits('n), atom('hi), atom('lo), atom('q)) -> bits('hi - 'lo + 1 + 'q) effect pure + +function subrange_zeros_concat (xs, hi, lo, l') = + slice_zeros_concat(xs, lo, hi - lo + 1, l') + /* Assumes initial vectors are of equal size */ val subrange_subrange_eq : forall 'n, 'n >= 0. @@ -103,13 +109,19 @@ function place_slice(m,xs,i,l,shift) = { } val set_slice_zeros : forall 'n, 'n >= 0. - (atom('n), bits('n), int, int) -> bits('n) effect pure + (implicit('n), bits('n), int, int) -> bits('n) effect pure function set_slice_zeros(n, xs, i, l) = { let ys : bits('n) = slice_mask(n, i, l) in xs & not_vec(ys) } +val set_subrange_zeros : forall 'n, 'n >= 0. + (implicit('n), bits('n), int, int) -> bits('n) effect pure + +function set_subrange_zeros(n, xs, hi, lo) = + set_slice_zeros(n, xs, lo, hi - lo + 1) + val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bits('n), int, int) -> bits('m) effect pure @@ -118,6 +130,11 @@ function zext_slice(m,xs,i,l) = { extzv(m, xs) } +val zext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (implicit('m), bits('n), int, int) -> bits('m) effect pure + +function zext_subrange(m, xs, i, j) = zext_slice(m, xs, j, i - j + 1) + val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bits('n), int, int) -> bits('m) effect pure @@ -126,6 +143,11 @@ function sext_slice(m,xs,i,l) = { extsv(m, xs) } +val sext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0. + (implicit('m), bits('n), int, int) -> bits('m) effect pure + +function sext_subrange(m, xs, i, j) = sext_slice(m, xs, j, i - j + 1) + val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), bits('n), int, int, int) -> bits('m) effect pure @@ -202,4 +224,13 @@ function vector_update_subrange_from_subrange(n,v1,s1,e1,v2,s2,e2) = { xs | ys } +val vector_update_subrange_from_integer_subrange : forall 'n1 's1 'e1 's2 'e2, + 0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 & 's1 - 'e1 == 's2 - 'e2. + (implicit('n1), bits('n1), int('s1), int('e1), int, int('s2), int('e2)) -> bits('n1) + +function vector_update_subrange_from_integer_subrange(n1, v1, s1, e1, i, s2, e2) = { + let v2 : bits('n1) = get_slice_int(n1, i, e2) in + vector_update_subrange_from_subrange(n1, v1, s1, e1, v2, s2 - e2, 0) +} + $endif diff --git a/lib/smt.sail b/lib/smt.sail index 93fe0827..2e72e791 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -23,7 +23,7 @@ val emod_int = { val abs_int_atom = { ocaml: "abs_int", interpreter: "abs_int", - lem: "abs_int", + lem: "integerAbs", c: "abs_int", coq: "abs_with_eq" } : forall 'n. int('n) -> int(abs('n)) diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 2a9e96f0..32443560 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -146,6 +146,7 @@ overload operator + = {add_bits, add_bits_int} val sub_bits = { ocaml: "sub_vec", + interpreter: "sub_vec", lem: "sub_vec", c: "sub_bits", coq: "sub_vec" @@ -230,7 +231,7 @@ val get_slice_int = "get_slice_int" : forall 'w. (int('w), int, int) -> bits('w) val set_slice_int = "set_slice_int" : forall 'w. (int('w), int, int, bits('w)) -> int val set_slice_bits = "set_slice" : forall 'n 'm. - (int('n), int('m), bits('n), int, bits('m)) -> bits('n) + (implicit('n), int('m), bits('n), int, bits('m)) -> bits('n) /*! converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$. diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index 00b3d192..c190cffc 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -663,6 +663,10 @@ let const_props target defs ref_vars = | "or_bool", ([E_aux (E_lit (L_aux (L_true, _)), _) as e_true; _] | [_; E_aux (E_lit (L_aux (L_true, _)), _) as e_true]) -> e_true + | _, [E_aux (E_vector [], _); e'] + | _, [e'; E_aux (E_vector [], _)] + when is_overload_of (mk_id "append") -> + e' | _, _ when List.for_all Constant_fold.is_constant args -> const_fold exp | _, [arg] when is_overload_of (mk_id "__size") -> @@ -733,6 +737,10 @@ let const_props target defs ref_vars = (Reporting.print_err lit_l "Monomorphisation" "Unexpected kind of literal for var match"; GiveUp) end + | E_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)), P_vector _ -> + let mk_bitlit lit = E_aux (E_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in + let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in + check_exp_pat (E_aux (E_vector lits', (l, annot))) pat | E_lit _, _ -> (Reporting.print_err l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) @@ -744,6 +752,7 @@ let const_props target defs ref_vars = if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var -> DoesMatch ([var, e],[]) + | _, P_aux (P_wild, _) -> DoesMatch ([],[]) | _ -> GiveUp) es ps in let final = List.fold_left (fun acc m -> match acc, m with | _, GiveUp -> GiveUp @@ -755,6 +764,10 @@ let const_props target defs ref_vars = (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) | _ -> final) + | E_vector _, P_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)) -> + let mk_bitlit lit = P_aux (P_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in + let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in + check_exp_pat exp (P_aux (P_vector lits', (l, annot))) | E_vector _, _ -> (Reporting.print_err l "Monomorphisation" "Unexpected kind of pattern for vector literal"; GiveUp) @@ -779,6 +792,24 @@ let const_props target defs ref_vars = | _ -> GiveUp in let check_pat = check_exp_pat exp0 in + let add_ksubst_synonyms env' ksubst = + (* The type checker sometimes automatically generates kid synonyms, e.g. + in let 'datasize = ... in ... it binds both 'datasize and '_datasize. + If we subsitute one, we also want to substitute the other. + In order to find synonyms, we consult the environment after the + bind (see findpat_generic below). *) + let get_synonyms (kid, nexp) = + let rec synonyms_of_nc nc = match unaux_constraint nc with + | NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var (kid2), _)) + when Kid.compare kid kid1 = 0 -> + [(kid2, nexp)] + | NC_and _ -> List.concat (List.map synonyms_of_nc (constraint_conj nc)) + | _ -> [] + in + List.concat (List.map synonyms_of_nc (Env.get_constraints env')) + in + ksubst @ List.concat (List.map get_synonyms ksubst) + in let rec findpat_generic description assigns = function | [] -> (Reporting.print_err l "Monomorphisation" ("Failed to find a case for " ^ description); None) @@ -791,7 +822,9 @@ let const_props target defs ref_vars = kbindings_union ksubsts (kbindings_from_list ksubst) in let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in match guard with - | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst) + | E_lit (L_aux (L_true,_)) -> + let ksubst = add_ksubst_synonyms (env_of exp) ksubst in + Some (exp,vsubst,ksubst) | E_lit (L_aux (L_false,_)) -> findpat_generic description assigns tl | _ -> None end @@ -800,7 +833,9 @@ let const_props target defs ref_vars = | (Pat_aux (Pat_exp (p,exp),_))::tl -> match check_pat p with | DoesNotMatch -> findpat_generic description assigns tl - | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst) + | DoesMatch (subst,ksubst) -> + let ksubst = add_ksubst_synonyms (env_of exp) ksubst in + Some (exp,subst,ksubst) | GiveUp -> None in findpat_generic (string_of_exp exp0) assigns cases diff --git a/src/constraint.ml b/src/constraint.ml index 74f3ec69..3ceb0aae 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -230,6 +230,7 @@ type smt_result = Unknown | Sat | Unsat module DigestMap = Map.Make(Digest) let known_problems = ref (DigestMap.empty) +let known_uniques = ref (DigestMap.empty) let load_digests_err () = let in_chan = open_in_bin "z3_problems" in @@ -241,6 +242,10 @@ let load_digests_err () = | 0 -> known_problems := DigestMap.add digest Unknown !known_problems | 1 -> known_problems := DigestMap.add digest Sat !known_problems | 2 -> known_problems := DigestMap.add digest Unsat !known_problems + | 3 -> known_uniques := DigestMap.add digest None !known_uniques + | 4 -> + let solution = input_binary_int in_chan in + known_uniques := DigestMap.add digest (Some solution) !known_uniques | _ -> assert false end; load () @@ -254,14 +259,21 @@ let load_digests () = let save_digests () = let out_chan = open_out_bin "z3_problems" in - let output digest result = + let output_problem digest result = Digest.output out_chan digest; match result with | Unknown -> output_byte out_chan 0 | Sat -> output_byte out_chan 1 | Unsat -> output_byte out_chan 2 in - DigestMap.iter output !known_problems; + DigestMap.iter output_problem !known_problems; + let output_solution digest result = + Digest.output out_chan digest; + match result with + | None -> output_byte out_chan 3 + | Some i -> output_byte out_chan 4; output_binary_int out_chan i + in + DigestMap.iter output_solution !known_uniques; close_out out_chan let kopt_pair kopt = (kopt_kid kopt, unaux_kind (kopt_kind kopt)) @@ -344,16 +356,17 @@ let call_smt l constraints = Profile.finish_smt t; result -let solve_smt l constraints var = +let solve_smt_file l constraints = let vars = kopts_of_constraint constraints |> KOptSet.elements |> List.map kopt_pair |> List.fold_left (fun m (k, v) -> KBindings.add k v m) KBindings.empty in - let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in - let smt_var = pp_sexpr (smt_var var) in + smtlib_of_constraints ~get_model:true l vars constraints +let call_smt_solve l smt_file smt_vars var = + let smt_var = pp_sexpr (smt_vars var) in if !opt_smt_verbose then prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file) else (); @@ -389,6 +402,10 @@ let solve_smt l constraints var = with | Not_found -> None +let solve_smt l constraints var = + let smt_file, smt_vars = solve_smt_file l constraints in + call_smt_solve l smt_file smt_vars var + let solve_all_smt l constraints var = let rec aux results = let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in @@ -402,10 +419,24 @@ let solve_all_smt l constraints var = aux [] let solve_unique_smt l constraints var = - match solve_smt l constraints var with - | Some result -> - begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with - | Unsat -> Some result - | _ -> None - end - | None -> None + let smt_file, smt_vars = solve_smt_file l constraints in + let digest = Digest.string (smt_file ^ pp_sexpr (smt_vars var)) in + match DigestMap.find_opt digest !known_uniques with + | Some (Some result) -> Some (Big_int.of_int result) + | Some (None) -> None + | None -> + match call_smt_solve l smt_file smt_vars var with + | Some result -> + begin match call_smt l (nc_and constraints (nc_neq (nconstant result) (nvar var))) with + | Unsat -> + if Big_int.less_equal Big_int.zero result && Big_int.less result (Big_int.pow_int_positive 2 30) then + known_uniques := DigestMap.add digest (Some (Big_int.to_int result)) !known_uniques + else (); + Some result + | _ -> + known_uniques := DigestMap.add digest None !known_uniques; + None + end + | None -> + known_uniques := DigestMap.add digest None !known_uniques; + None diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem index 69bf0852..9e1f20c0 100644 --- a/src/gen_lib/sail2_values.lem +++ b/src/gen_lib/sail2_values.lem @@ -35,15 +35,27 @@ let power_int_nat l r = integerPow l r let power_int_int l r = integerPow l (nat_of_int r) let negate_int i = integerNegate i let min_int l r = integerMin l r -let max_int l r = integerMax l r +let max_int l r = integerMax l r*) -let add_real l r = realAdd l r -let sub_real l r = realMinus l r -let mult_real l r = realMult l r -let div_real l r = realDiv l r -let negate_real r = realNegate r -let abs_real r = realAbs r -let power_real b e = realPowInteger b e*) +let inline add_real l r = realAdd l r +let inline sub_real l r = realMinus l r +let inline mult_real l r = realMult l r +let inline div_real l r = realDiv l r +let inline neg_real r = realNegate r +let inline abs_real r = realAbs r +let inline real_power b e = realPowInteger b e +let inline sqrt_real r = realSqrt r + +let inline eq_real l r = realEq l r +let inline lt_real l r = realLess l r +let inline gt_real l r = realLessEqual l r +let inline lteq_real l r = realGreater l r +let inline gteq_real l r = realGreaterEqual l r + +let inline to_real i = realFromInteger i + +let inline round_down r = realFloor r +let inline round_up r = realCeiling r val print_endline : string -> unit let print_endline _ = () @@ -464,6 +476,44 @@ let show_bitlist_prefix c bs = let show_bitlist bs = show_bitlist_prefix #'0' bs +val hex_char : natural -> char + +let hex_char n = + match n with + | 0 -> #'0' + | 1 -> #'1' + | 2 -> #'2' + | 3 -> #'3' + | 4 -> #'4' + | 5 -> #'5' + | 6 -> #'6' + | 7 -> #'7' + | 8 -> #'8' + | 9 -> #'9' + | 10 -> #'A' + | 11 -> #'B' + | 12 -> #'C' + | 13 -> #'D' + | 14 -> #'E' + | 15 -> #'F' + | _ -> failwith "hex_char: not a hexadecimal digit" + end + +val hex_str_aux : natural -> list char -> list char + +let rec hex_str_aux n acc = + if n = 0 then acc else + hex_str_aux (n div 16) (hex_char (n mod 16) :: acc) + +declare {isabelle} termination_argument hex_str_aux = automatic + +val hex_str : integer -> string + +let hex_str i = + if i < 0 then failwith "hex_str: negative" else + if i = 0 then "0x0" else + "0x" ^ toString (hex_str_aux (naturalFromInteger (abs i)) []) + (*** List operations *) let inline (^^) = append_list diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index a299d7b9..26509a69 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -287,6 +287,8 @@ let smt_conversion ctx from_ctyp to_ctyp x = force_size ctx n ctx.lint_size x | CT_lint, CT_lbits _ -> Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x]) + | CT_fint n, CT_lbits _ -> + Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); force_size ctx (lbits_size ctx) n x]) | CT_lbits _, CT_fbits (n, _) -> unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x])) | CT_fbits (n, _), CT_fbits (m, _) -> @@ -960,6 +962,11 @@ let builtin_add_bits_int ctx v1 v2 ret_ctyp = | CT_fbits (n, _), CT_lint, CT_fbits (o, _) when n = o -> Fn ("bvadd", [smt_cval ctx v1; force_size ctx o ctx.lint_size (smt_cval ctx v2)]) + | CT_lbits _, CT_fint n, CT_lbits _ when n < lbits_size ctx -> + let smt1 = smt_cval ctx v1 in + let smt2 = force_size ctx (lbits_size ctx) n (smt_cval ctx v2) in + Fn ("Bits", [Fn ("len", [smt1]); Fn ("bvadd", [Fn ("contents", [smt1]); smt2])]) + | _ -> builtin_type_error ctx "add_bits_int" [v1; v2] (Some ret_ctyp) let builtin_sub_bits_int ctx v1 v2 ret_ctyp = @@ -1129,6 +1136,20 @@ let builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp = let smt5 = Fn ("concat", [bvzero (n - m - pos); Fn ("concat", [smt_cval ctx v5; bvzero pos])]) in Fn ("bvor", [Fn ("bvand", [smt_cval ctx v3; mask]); smt5]) + (* set_slice_bits(len, slen, x, pos, y) = + let mask = slice_mask(len, pos, slen) in + (x AND NOT(mask)) OR ((unsigned_size(len, y) << pos) AND mask) *) + | CT_constant n', _, CT_fbits (n, _), _, CT_lbits _, CT_fbits (n'', _) + when Big_int.to_int n' = n && n'' = n -> + let pos = bvzeint ctx (lbits_size ctx) v4 in + let slen = bvzeint ctx ctx.lbits_index v2 in + let mask = Fn ("bvshl", [bvmask ctx slen; pos]) in + let smt3 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v3) in + let smt3' = Fn ("bvand", [smt3; Fn ("bvnot", [mask])]) in + let smt5 = Fn ("contents", [smt_cval ctx v5]) in + let smt5' = Fn ("bvand", [Fn ("bvshl", [smt5; pos]); mask]) in + Extract (n - 1, 0, Fn ("bvor", [smt3'; smt5'])) + | _ -> builtin_type_error ctx "set_slice" [v1; v2; v3; v4; v5] (Some ret_ctyp) let builtin_compare_bits fn ctx v1 v2 ret_ctyp = @@ -1877,11 +1898,14 @@ let smt_instr ctx = Reporting.unreachable l __POS__ "Register reference write should be re-written by now" | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) -> - begin match id with - | Name (id, _) | Global (id, _) when IdSet.mem id ctx.preserved -> + begin match id, cval with + | (Name (id, _) | Global (id, _)), _ when IdSet.mem id ctx.preserved -> [preserve_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] - | _ -> + | _, V_lit (VL_undefined, _) -> + (* Declare undefined variables as arbitrary but fixed *) + [declare_const ctx id ctyp] + | _, _ -> [define_const ctx id ctyp (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))] end diff --git a/src/monomorphise.ml b/src/monomorphise.ml index e328cce1..f4d0aa56 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -81,6 +81,16 @@ let kbindings_union s1 s2 = | (Some x), _ -> Some x | _, _ -> None) s1 s2 +let ids_in_exp exp = + let open Rewriter in + fold_exp { + (pure_exp_alg IdSet.empty IdSet.union) with + e_id = IdSet.singleton; + lEXP_id = IdSet.singleton; + lEXP_memory = (fun (id,s) -> List.fold_left IdSet.union (IdSet.singleton id) s); + lEXP_cast = (fun (_,id) -> IdSet.singleton id) + } exp + let make_vector_lit sz i = let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in let s = String.init sz f in @@ -95,6 +105,12 @@ let tabulate f n = let make_vectors sz = tabulate (make_vector_lit sz) (Big_int.shift_left (Big_int.of_int 1) sz) +let is_inc_vec typ = + try + let (_, ord, _) = vector_typ_args_of typ in + is_order_inc ord + with _ -> false + let rec cross = function | [] -> failwith "cross" | [(x,l)] -> List.map (fun y -> [(x,y)]) l @@ -138,6 +154,29 @@ let extract_set_nc env l var nc = let re nc = NC_aux (nc,l) in match nc with | NC_set (id,is) when KidSet.mem id vars -> Some (is,re NC_true) + | NC_equal (Nexp_aux (Nexp_var id,_), Nexp_aux (Nexp_constant n,_)) + when KidSet.mem id vars -> + Some ([n], re NC_true) + (* Turn (i <= 'v & 'v <= j & ...) into set constraint ('v in {i..j}) *) + | NC_and (NC_aux (NC_bounded_le (Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_var kid, _)), _) as nc1, nc2) + when KidSet.mem kid vars -> + let aux2 () = match aux expanded nc2 with + | Some (is, nc2') -> Some (is, re (NC_and (nc1, nc2'))) + | None -> None + in + begin match constraint_conj nc2 with + | NC_aux (NC_bounded_le (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant n', _)), _) :: ncs + when KidSet.mem kid' vars -> + let len = Big_int.succ (Big_int.sub n' n) in + if Big_int.less_equal Big_int.zero len && Big_int.less_equal len (Big_int.of_int size_set_limit) then + let elem i = Big_int.add n (Big_int.of_int i) in + let is = List.init (Big_int.to_int len) elem in + if aux expanded (List.fold_left nc_and nc_true ncs) <> None then + raise (Reporting.err_general l ("Multiple set constraints for " ^ string_of_kid var)) + else Some (is, nc_full) + else aux2 () + | _ -> aux2 () + end | NC_and (nc1,nc2) -> (match aux expanded nc1, aux expanded nc2 with | None, None -> None @@ -232,6 +271,10 @@ and contains_exist_arg (A_aux (arg,_)) = -> false | A_typ typ -> contains_exist typ +let is_number typ = match destruct_numeric typ with + | Some _ -> true + | None -> false + let rec size_nvars_nexp (Nexp_aux (ne,_)) = match ne with | Nexp_var v -> [v] @@ -550,6 +593,8 @@ let stop_at_false_assertions e = end | E_assert (e1,_) when exp_false e1 -> ea, Some (typ_of_annot ann) + | E_throw e -> + ea, Some (typ_of_annot ann) | _ -> ea, None in fst (exp e) @@ -1015,8 +1060,8 @@ let split_defs target all_errors splits env defs = if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> let exp' = Spec_analysis.nexp_subst_exp ksubsts e in - let exp' = subst_exp ref_vars substs ksubsts exp' in let exp' = apply_pat_choices pchoices exp' in + let exp' = subst_exp ref_vars substs ksubsts exp' in let exp' = stop_at_false_assertions exp' in Pat_aux (Pat_exp (pat', map_exp exp'),l)) patsubsts @@ -1035,11 +1080,11 @@ let split_defs target all_errors splits env defs = if check_split_size patsubsts (pat_loc p) then List.map (fun (pat',substs,pchoices,ksubsts) -> let exp1' = Spec_analysis.nexp_subst_exp ksubsts e1 in - let exp1' = subst_exp ref_vars substs ksubsts exp1' in let exp1' = apply_pat_choices pchoices exp1' in + let exp1' = subst_exp ref_vars substs ksubsts exp1' in let exp2' = Spec_analysis.nexp_subst_exp ksubsts e2 in - let exp2' = subst_exp ref_vars substs ksubsts exp2' in let exp2' = apply_pat_choices pchoices exp2' in + let exp2' = subst_exp ref_vars substs ksubsts exp2' in let exp2' = stop_at_false_assertions exp2' in Pat_aux (Pat_when (pat', map_exp exp1', map_exp exp2'),l)) patsubsts @@ -1102,7 +1147,9 @@ let split_defs target all_errors splits env defs = List.map (fun fcl' -> SD_aux (SD_funcl fcl', annot)) (map_funcl fcl) | _ -> [sd] in - let map_def d = + let num_defs = List.length defs in + let map_def idx d = + Util.progress "Monomorphising " (string_of_int idx ^ "/" ^ string_of_int num_defs) idx num_defs; match d with | DEF_type _ | DEF_spec _ @@ -1123,10 +1170,11 @@ let split_defs target all_errors splits env defs = Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should have been rewritten before now" in - Defs (List.concat (List.map map_def defs)) + Defs (List.concat (List.mapi map_def defs)) in - let defs'' = map_locs splits defs' in - !no_errors_happened, defs'' + let (Defs defs'') = map_locs splits defs' in + Util.progress "Monomorphising " "done" (List.length defs'') (List.length defs''); + !no_errors_happened, (Defs defs'') @@ -1289,10 +1337,24 @@ let replace_type env typ = ("replace_type: Unsupported type " ^ string_of_typ typ)) -let rewrite_size_parameters env (Defs defs) = +let rewrite_size_parameters target type_env (Defs defs) = let open Rewriter in let open Util in + let const_prop_exp exp = + let ref_vars = Constant_propagation.referenced_vars exp in + let substs = (Bindings.empty, KBindings.empty) in + let assigns = Bindings.empty in + fst (Constant_propagation.const_prop target (Defs defs) ref_vars substs assigns exp) + in + let const_prop_pexp pexp = + let (pat, guard, exp, a) = destruct_pexp pexp in + construct_pexp (pat, guard, const_prop_exp exp, a) + in + let const_prop_funcl (FCL_aux (FCL_Funcl (id, pexp), a)) = + FCL_aux (FCL_Funcl (id, const_prop_pexp pexp), a) + in + let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pexp),(l,ann))) = let pat,guard,exp,pannot = destruct_pexp pexp in let env = env_of_annot (l,ann) in @@ -1332,31 +1394,52 @@ let rewrite_size_parameters env (Defs defs) = print_endline ("Nexp map for " ^ string_of_id id); List.iter (fun (nexp, i) -> print_endline (" " ^ string_of_nexp nexp ^ " -> " ^ string_of_int i)) nexp_list in *) - let parameters_for tannot = - match destruct_tannot tannot with - | Some (env,typ,_) -> - begin match Env.base_typ_of env typ with - | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) - when not (is_nexp_constant size) -> - begin - match NexpMap.find size nexp_map with - | i -> IntSet.singleton i - | exception Not_found -> - (* Look for equivalent nexps, but only in consistent type env *) - if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else - match List.find (fun (nexp,i) -> - prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with - | _, i -> IntSet.singleton i - | exception Not_found -> IntSet.empty + let parameters_for e tannot = + let parameters_for_nexp env size = + match solve_unique env size with + | Some _ -> IntSet.empty + | None -> + match NexpMap.find size nexp_map with + | i -> IntSet.singleton i + | exception Not_found -> + (* Look for equivalent nexps, but only in consistent type env *) + if prove __POS__ env (NC_aux (NC_false,Unknown)) then IntSet.empty else + match List.find (fun (nexp,i) -> + prove __POS__ env (NC_aux (NC_equal (nexp,size),Unknown))) nexp_list with + | _, i -> IntSet.singleton i + | exception Not_found -> IntSet.empty + in + let parameters_for_typ = + match destruct_tannot tannot with + | Some (env,typ,_) -> + begin match Env.base_typ_of env typ with + | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), [A_aux (A_nexp size,_);_]),_) + when not (is_nexp_constant size) -> + parameters_for_nexp env size + | _ -> IntSet.empty end - | _ -> IntSet.empty - end - | None -> IntSet.empty + | None -> IntSet.empty + in + let parameters_for_exp = match e with + | E_app (id, args) when Bindings.mem id fsizes -> + let add_arg (i, s) arg = + if IntSet.mem i (fst (Bindings.find id fsizes)) then + try match destruct_numeric (typ_of arg) with + | Some ([], _, nexp) -> + (i + 1, IntSet.union s (parameters_for_nexp env nexp)) + | _ -> (i + 1, s) + with _ -> (i + 1, s) + else (i + 1, s) + in + snd (List.fold_left add_arg (0, IntSet.empty) args) + | _ -> IntSet.empty + in + IntSet.union parameters_for_typ parameters_for_exp in let parameters_to_rewrite = fst (fold_pexp { (compute_exp_alg IntSet.empty IntSet.union) with - e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for annot),E_aux (e,(l,annot))) + e_aux = (fun ((s,e),(l,annot)) -> IntSet.union s (parameters_for e annot),E_aux (e,(l,annot))) } pexp) in let new_nexps = NexpSet.of_list (List.map fst @@ -1437,27 +1520,62 @@ in *) in let rewrite_letbind = fold_letbind { id_exp_alg with e_app = rewrite_e_app } in let rewrite_exp = fold_exp { id_exp_alg with e_app = rewrite_e_app } in + let replace_funtype id typ = + match Bindings.find id fn_sizes with + | to_change,_ when not (IntSet.is_empty to_change) -> + begin match typ with + | Typ_aux (Typ_fn (ts,t2,eff),l2) -> + Typ_aux (Typ_fn (mapat (replace_type type_env) to_change ts,t2,eff),l2) + | _ -> replace_type type_env typ + end + | _ -> typ + | exception Not_found -> typ + in + let type_env' = + let update_val_spec id _ env = + let (tq, typ) = Env.get_val_spec_orig id env in + Env.update_val_spec id (tq, replace_funtype id typ) env + in + Bindings.fold update_val_spec fn_sizes type_env + in let rewrite_def = function | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) -> + let funcls = List.map rewrite_funcl funcls in + (* Check whether we have ended up with itself('n) expressions where 'n + is not constant. If so, try and see if constant propagation can + resolve those variable expressions. In many cases the monomorphisation + pass will already have performed constant propagation, but it does not + for functions where it does not perform splits.*) + let check_funcl (FCL_aux (FCL_Funcl (id, pexp), (l, _)) as funcl) = + let has_nonconst_sizes = + let check_cast (typ, _) = + match unaux_typ typ with + | Typ_app (itself, [A_aux (A_nexp nexp, _)]) + | Typ_exist (_, _, Typ_aux (Typ_app (itself, [A_aux (A_nexp nexp, _)]), _)) + when string_of_id itself = "itself" -> + not (is_nexp_constant nexp) + | _ -> false + in + fold_pexp { (pure_exp_alg false (||)) with e_cast = check_cast } pexp + in + if has_nonconst_sizes then + (* Constant propagation requires a fully type-annotated AST, + so re-check the function clause *) + let (tq, typ) = Env.get_val_spec id type_env' in + let env = add_typquant l tq type_env' in + const_prop_funcl (Type_check.check_funcl env funcl typ) + else funcl + in + let funcls = List.map check_funcl funcls in (* TODO rewrite tannopt? *) - DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,empty_tannot))) + DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,empty_tannot))) | DEF_val lb -> DEF_val (rewrite_letbind lb) | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec -> - begin - match Bindings.find id fn_sizes with - | to_change,_ when not (IntSet.is_empty to_change) -> - let typschm = match typschm with - | TypSchm_aux (TypSchm_ts (tq,typ),l) -> - let typ = match typ with - | Typ_aux (Typ_fn (ts,t2,eff),l2) -> - Typ_aux (Typ_fn (mapat (replace_type env) to_change ts,t2,eff),l2) - | _ -> replace_type env typ - in TypSchm_aux (TypSchm_ts (tq,typ),l) - in - DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,empty_tannot))) - | _ -> spec - | exception Not_found -> spec - end + let typschm = match typschm with + | TypSchm_aux (TypSchm_ts (tq, typ),l) -> + TypSchm_aux (TypSchm_ts (tq, replace_funtype id typ), l) + in + DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), a)) -> DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewrite_exp exp), a)) | def -> def @@ -1631,9 +1749,19 @@ let string_of_dep = function (* If a callee uses a type variable as a size, does it need to be split in the current function, or is it also a parameter? (Note that there may be multiple calls, so more than one parameter can be involved) *) -type call_dep = - | InFun of dependencies - | Parents of CallerKidSet.t +type call_dep = { + in_fun : dependencies option; + parents : CallerKidSet.t; +} + +let empty_call_dep = { + in_fun = None; + parents = CallerKidSet.empty; +} + +let in_fun_call_dep deps = { in_fun = Some deps; parents = CallerKidSet.empty } + +let parents_call_dep cks = { in_fun = None; parents = cks } (* Result of analysing the body of a function. The split field gives the arguments to split based on the body alone, the extra_splits @@ -1693,17 +1821,16 @@ let dep_bindings_merge a1 a2 = let dep_kbindings_merge a1 a2 = KBindings.merge (opt_merge dmerge) a1 a2 +let call_dep_merge k d1 d2 = { + in_fun = opt_merge dmerge k d1.in_fun d2.in_fun; + parents = CallerKidSet.union d1.parents d2.parents +} + let call_kid_merge k x y = match x, y with | None, x -> x | x, None -> x - | Some (InFun deps), Some (Parents _) - | Some (Parents _), Some (InFun deps) - -> Some (InFun deps) - | Some (InFun deps), Some (InFun deps') - -> Some (InFun (dmerge deps deps')) - | Some (Parents fns), Some (Parents fns') - -> Some (Parents (CallerKidSet.union fns fns')) + | Some d1, Some d2 -> Some (call_dep_merge k d1 d2) let call_arg_merge k args args' = match args, args' with @@ -1871,11 +1998,11 @@ and deps_of_typ_arg l fn_id env arg_deps (A_aux (aux, _)) = match aux with | A_nexp (Nexp_aux (Nexp_var kid,_)) when List.exists (fun k -> Kid.compare kid k == 0) env.top_kids -> - Parents (CallerKidSet.singleton (fn_id,kid)) - | A_nexp nexp -> InFun (deps_of_nexp l env.kid_deps arg_deps nexp) - | A_order _ -> InFun dempty - | A_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ) - | A_bool nc -> InFun (deps_of_nc env.kid_deps nc) + parents_call_dep (CallerKidSet.singleton (fn_id,kid)) + | A_nexp nexp -> in_fun_call_dep (deps_of_nexp l env.kid_deps arg_deps nexp) + | A_order _ -> in_fun_call_dep dempty + | A_typ typ -> in_fun_call_dep (deps_of_typ l env.kid_deps arg_deps typ) + | A_bool nc -> in_fun_call_dep (deps_of_nc env.kid_deps nc) let mk_subrange_pattern vannot vstart vend = let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in @@ -1942,6 +2069,37 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps = (match mk_subrange_pattern vannot vstart vend with | Some mk_pat -> check_dep id mk_pat | None -> None) + (* TODO: Aborted attempt at considering bitvector concatenations when + refining dependencies. Needs corresponding support in constant + propagation to work. *) + (* | E_app (append, [vec1; vec2]) + when is_id (env_of exp) (Id "append") append -> + (* If the expression is a concatenation resulting in a small enough bitvector, + perform a (total) case split on the sub-vectors *) + let vec_len v = try Util.option_map Big_int.to_int (get_constant_vec_len (env_of exp) v) with _ -> None in + let pow2 n = Big_int.pow_int (Big_int.of_int 2) n in + let size_set len1 len2 = Big_int.mul (pow2 len1) (pow2 len2) in + begin match (vec_len (typ_of exp), vec_len (typ_of vec1), vec_len (typ_of vec2)) with + | (Some len, Some len1, Some len2) + when Big_int.less_equal (size_set len1 len2) (Big_int.of_int size_set_limit) -> + let recur = refine_dependency env in + (* Create pexps with dummy bodies (ignored by the recursive call) *) + let mk_pexps len = + let mk_pexp lit = + let (_, ord, _) = vector_typ_args_of (typ_of exp) in + let tannot = mk_tannot (env_of exp) (bitvector_typ (nint len) ord) no_effect in + let pat = P_aux (P_lit lit, (Generated l, tannot)) in + let exp = E_aux (E_lit (mk_lit L_unit), (Generated l, empty_tannot)) in + Pat_aux (Pat_exp (pat, exp), (Generated l, empty_tannot)) + in + List.map mk_pexp (make_vectors len) + in + begin match (recur vec1 (mk_pexps len1), recur vec2 (mk_pexps len2)) with + | (Some deps1, Some deps2) -> Some (dmerge deps1 deps2) + | _ -> None + end + | _ -> None + end *) | _ -> None let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = @@ -1950,7 +2108,9 @@ let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) = | None -> let is_equal kid = try - prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + if Env.get_typ_var kid typ_env = K_int then + prove __POS__ typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown)) + else false with _ -> false in match ne with @@ -2072,7 +2232,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = let rdep,r' = if Id.compare fn_id id == 0 then let bad = Unknown (l,"Recursive call of " ^ string_of_id id) in - let kid_deps = KBindings.map (fun _ -> InFun bad) kid_deps in + let kid_deps = KBindings.map (fun _ -> in_fun_call_dep bad) kid_deps in bad, { empty with split_on_call = Bindings.singleton id kid_deps } else dempty, { empty with split_on_call = Bindings.singleton id kid_deps } in @@ -2489,6 +2649,8 @@ let rec sets_from_assert e = match nc with | NC_and (nc1,nc2) -> merge_set_asserts_by_kid (sets_from_nc nc1) (sets_from_nc nc2) | NC_set (kid,is) -> KBindings.singleton kid (l,is) + | NC_equal (Nexp_aux (Nexp_var kid,_), Nexp_aux (Nexp_constant n,_)) -> + KBindings.singleton kid (l, [n]) | NC_or _ -> (match set_from_nc_or nc_full with | Some (kid, is) -> KBindings.singleton kid (l,is) @@ -2532,11 +2694,12 @@ let print_set_assertions set_assertions = let print_result r = let _ = print_endline (" splits: " ^ string_of_argsplits r.split) in let print_kbinding kid dep = - let s = match dep with - | InFun dep -> "InFun " ^ string_of_dep dep - | Parents cks -> string_of_callerkidset cks + let s1 = match dep.in_fun with + | Some dep -> "InFun " ^ string_of_dep dep + | None -> "" in - let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s) in + let s2 = string_of_callerkidset dep.parents in + let _ = print_endline (" " ^ string_of_kid kid ^ ": " ^ s1 ^ "; " ^ s2) in () in let print_binding id kdep = @@ -2557,7 +2720,7 @@ let print_result r = let analyse_funcl debug tenv constants (FCL_aux (FCL_Funcl (id,pexp),(l,_))) = let _ = if debug > 2 then print_endline (string_of_id id) else () in let pat,guard,body,_ = destruct_pexp pexp in - let (tq,_) = Env.get_val_spec id tenv in + let (tq,_) = Env.get_val_spec_orig id tenv in let set_assertions = find_set_assertions body in let _ = if debug > 2 then print_set_assertions set_assertions in let aenv = initial_env id l tq pat body set_assertions constants in @@ -2598,11 +2761,17 @@ let argset_to_list splits = List.map argelt l let analyse_defs debug env (Defs defs) = - let def (globals,r) d = + let def (idx,globals,r) d = + begin match d with + | DEF_fundef fd -> + Util.progress "Analysing " (string_of_id (id_of_fundef fd)) idx (List.length defs) + | _ -> () + end; let globals,r' = analyse_def debug env globals d in - globals, merge r r' + idx + 1, globals, merge r r' in - let _,r = List.fold_left def (Bindings.empty,empty) defs in + let _,_,r = List.fold_left def (0,Bindings.empty,empty) defs in + let _ = Util.progress "Analysing " "done" (List.length defs) (List.length defs) in (* Resolve the interprocedural dependencies *) @@ -2616,8 +2785,12 @@ let analyse_defs debug env (Defs defs) = match Bindings.find id r.split_on_call with | kid_deps -> begin match KBindings.find kid kid_deps with - | InFun deps -> separate_deps deps - | Parents fns -> CallerKidSet.fold add_kid fns (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + | call_dep -> + let (splits, extras, fails) = match call_dep.in_fun with + | Some deps -> separate_deps deps + | None -> (ArgSplits.empty, ExtraSplits.empty, Failures.empty) + in + CallerKidSet.fold add_kid call_dep.parents (splits, extras, fails) | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty end | exception Not_found -> ArgSplits.empty,ExtraSplits.empty,Failures.empty @@ -2705,14 +2878,22 @@ let is_constant = function | E_aux (E_lit _,_) -> true | _ -> false -let is_constant_vec_typ env typ = +let get_constant_vec_len ?solve:(solve=false) env typ = let typ = Env.base_typ_of env typ in match destruct_bitvector env typ with | Some (size,_) -> - (match nexp_simp size with - | Nexp_aux (Nexp_constant _,_) -> true - | _ -> false) - | _ -> false + begin match nexp_simp size with + | Nexp_aux (Nexp_constant i,_) -> Some i + | nexp when solve -> solve_unique env nexp + | _ -> None + end + | _ -> None + +let is_constant_vec_typ env typ = (get_constant_vec_len env typ <> None) + +let is_zeros env id = + is_id env (Id "Zeros") id || is_id env (Id "zeros") id || + is_id env (Id "sail_zeros") id (* We have to add casts in here with appropriate length information so that the type checker knows the expected return types. *) @@ -2721,10 +2902,7 @@ let rec rewrite_app env typ (id,args) = let is_append = is_id env (Id "append") in let is_subrange = is_id env (Id "vector_subrange") in let is_slice = is_id env (Id "slice") in - let is_zeros id = - is_id env (Id "Zeros") id || is_id env (Id "zeros") id || - is_id env (Id "sail_zeros") id - in + let is_zeros id = is_zeros env id in let is_ones id = is_id env (Id "Ones") id || is_id env (Id "ones") id || is_id env (Id "sail_ones") id in let is_zero_extend = @@ -2734,6 +2912,21 @@ let rec rewrite_app env typ (id,args) = in let is_truncate = is_id env (Id "truncate") id in let mk_exp e = E_aux (e, (Unknown, empty_tannot)) in + let rec is_zeros_exp e = match unaux_exp e with + | E_app (zeros, [_]) when is_zeros zeros -> true + | E_lit (L_aux ((L_bin s | L_hex s), _)) -> + List.for_all (fun c -> c = '0') (Util.string_to_list s) + | E_cast (_, e) -> is_zeros_exp e + | _ -> false + in + let rec get_zeros_exp_len e = match unaux_exp e with + | E_app (zeros, [len]) when is_zeros zeros -> Some len + | E_cast (_, e) -> get_zeros_exp_len e + | _ -> + match get_constant_vec_len (env_of e) (typ_of e) with + | Some i -> Some (mk_exp (E_lit (L_aux (L_num i, Unknown)))) + | None -> None + in let try_cast_to_typ (E_aux (e,(l, _)) as exp) = let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in match size with @@ -2749,12 +2942,13 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (append, [e1; E_aux (E_app (subrange1, - [vector1; start1; end1]),_)]),_); + [vector1; start1; end1]),_) as sub1]),_); E_aux (E_app (subrange2, - [vector2; start2; end2]),_)] + [vector2; start2; end2]),_) as sub2] when is_append append && is_subrange subrange1 && is_subrange subrange2 && is_constant_vec_typ env (typ_of e1) && - not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && + not (is_constant_vec_typ env (typ_of sub1) || is_constant_vec_typ env (typ_of sub2)) -> 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 begin @@ -2782,6 +2976,7 @@ let rec rewrite_app env typ (id,args) = [vector2; start2; length2]),_)] when is_append append && is_slice slice1 && is_slice slice2 && is_constant_vec_typ env (typ_of e1) && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && 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 @@ -2804,28 +2999,33 @@ let rec rewrite_app env typ (id,args) = end (* variable-slice @ zeros *) - | [E_aux (E_app (slice1, [vector1; start1; len1]),_); - E_aux (E_app (zeros2, [len2]),_)] - when is_slice slice1 && is_zeros zeros2 && - not (is_constant start1 && is_constant len1 && is_constant len2) -> - try_cast_to_typ - (mk_exp (E_app (mk_id "place_slice", [vector1; start1; len1; len2]))) + | [E_aux (E_app (op, [vector1; start1; len1]),_) as exp1; zeros_exp] + when (is_slice op || is_subrange op) && is_zeros_exp zeros_exp + && is_bitvector_typ (typ_of vector1) + && not (is_constant_vec_typ env (typ_of exp1) && is_constant_vec_typ env (typ_of zeros_exp)) -> + let op' = if is_subrange op then "place_subrange" else "place_slice" in + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> try_cast_to_typ (mk_exp (E_app (mk_id op', [vector1; start1; len1; zlen]))) + | None -> E_app (id, args) + end (* ones @ zeros *) - | [E_aux (E_app (ones1, [len1]), _); - E_aux (E_app (zeros2, [len2]), _)] - when is_ones ones1 && is_zeros zeros2 && - not (is_constant len1 && is_constant len2) -> - try_cast_to_typ - (mk_exp (E_app (mk_id "slice_mask", [len2; len1]))) + | [E_aux (E_app (ones1, [len1]), _); zeros_exp] + when is_ones ones1 && is_zeros_exp zeros_exp && + not (is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> try_cast_to_typ (mk_exp (E_app (mk_id "slice_mask", [zlen; len1]))) + | None -> E_app (id, args) + end (* variable-range @ variable-range *) | [E_aux (E_app (subrange1, - [vector1; start1; end1]),_); + [vector1; start1; end1]),_) as exp1; E_aux (E_app (subrange2, - [vector2; start2; end2]),_)] + [vector2; start2; end2]),_) as exp2] when is_subrange subrange1 && is_subrange subrange2 && - not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && + not (is_constant_vec_typ env (typ_of exp1) || is_constant_vec_typ env (typ_of exp2)) -> try_cast_to_typ (E_aux (E_app (mk_id "subrange_subrange_concat", [vector1; start1; end1; vector2; start2; end2]), @@ -2837,29 +3037,40 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (slice2, [vector2; start2; length2]),_)] when is_slice slice1 && is_slice slice2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant length1 || is_constant length2) -> try_cast_to_typ (E_aux (E_app (mk_id "slice_slice_concat", [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot))) (* variable-slice @ local-var *) - | [E_aux (E_app (slice1, - [vector1; start1; length1]),_); + | [(E_aux (E_app (op, + [vector1; start1; length1]),_) as exp1); (E_aux (E_id _,_) as vector2)] - when is_slice slice1 && not (is_constant length1) -> - let start2 = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in + when (is_slice op || is_subrange op) && is_bitvector_typ (typ_of vector1) && + not (is_constant_vec_typ env (typ_of exp1)) -> + let op' = if is_subrange op then "subrange_subrange_concat" else "slice_slice_concat" in + let zero = mk_exp (E_lit (mk_lit (L_num Big_int.zero))) in + let one = mk_exp (E_lit (mk_lit (L_num (Big_int.of_int 1)))) in let length2 = mk_exp (E_app (mk_id "length", [vector2])) in + let indices2 = + if is_subrange op then + [mk_exp (E_app_infix (length2, mk_id "-", one)); zero] + else + [zero; length2] + in 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 (mk_id op', + [vector1; start1; length1; vector2] @ indices2),(Unknown,empty_tannot))) | [E_aux (E_app (append1, [e1; - E_aux (E_app (slice1, [vector1; start1; length1]),_)]),_); + (E_aux (E_app (op, [vector1; start1; length1]),_) as slice1)]),_); E_aux (E_app (zeros1, [length2]),_)] - when is_append append1 && is_slice slice1 && is_zeros zeros1 && - is_constant_vec_typ env (typ_of e1) && - not (is_constant length1 || is_constant length2) -> + when is_append append1 && (is_slice op || is_subrange op) && is_zeros zeros1 && + is_constant_vec_typ env (typ_of e1) && is_bitvector_typ (typ_of vector1) && + not (is_constant_vec_typ env (typ_of slice1) || is_constant length2) -> + let op' = mk_id (if is_subrange op then "subrange_zeros_concat" else "slice_zeros_concat") in 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 begin @@ -2870,14 +3081,14 @@ let rec rewrite_app env typ (id,args) = (E_aux (E_app (mk_id "append", [e1; E_aux (E_cast (midtyp, - E_aux (E_app (mk_id "slice_zeros_concat", + E_aux (E_app (op', [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", + E_aux (E_app (op', [vector1; start1; length1; length2]),(Unknown,empty_tannot))]), (Unknown,empty_tannot))) end @@ -2895,6 +3106,22 @@ let rec rewrite_app env typ (id,args) = | _ -> E_app (id,args) + else if is_id env (Id "vector_update_subrange") id then + match args with + | [vec1; start1; end1; (E_aux (E_app (subrange2, [vec2; start2; end2]), _) as e2)] + when is_subrange subrange2 && not (is_constant_vec_typ env (typ_of e2)) -> + let op = + if is_number (typ_of vec2) then "vector_update_subrange_from_integer_subrange" else + "vector_update_subrange_from_subrange" + in + try_cast_to_typ (E_aux (E_app (mk_id op, [vec1; start1; end1; vec2; start2; end2]), (Unknown, empty_tannot))) + + | [vec1; start1; end1; (E_aux (E_app (zeros, _), _) as e2)] + when is_zeros zeros && not (is_constant_vec_typ env (typ_of e2)) -> + try_cast_to_typ (E_aux (E_app (mk_id "set_subrange_zeros", [vec1; start1; end1]), (Unknown, empty_tannot))) + + | _ -> E_app (id, args) + else if is_id env (Id "eq_bits") id || is_id env (Id "neq_bits") id then (* variable-range == variable_range *) let wrap e = @@ -2908,6 +3135,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (subrange2, [vector2; start2; end2]),_)] when is_subrange subrange1 && is_subrange subrange2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) -> wrap (E_app (mk_id "subrange_subrange_eq", [vector1; start1; end1; vector2; start2; end2])) @@ -2916,6 +3144,7 @@ let rec rewrite_app env typ (id,args) = E_aux (E_app (slice2, [vector2; len2; start2]),_)] when is_slice slice1 && is_slice slice2 && + is_bitvector_typ (typ_of vector1) && is_bitvector_typ (typ_of vector2) && not (is_constant len1 && is_constant start1 && is_constant len2 && is_constant start2) -> let upper start len = mk_exp (E_app_infix (start, mk_id "+", @@ -2924,20 +3153,22 @@ let rec rewrite_app env typ (id,args) = in wrap (E_app (mk_id "subrange_subrange_eq", [vector1; upper start1 len1; start1; vector2; upper start2 len2; start2])) - | [E_aux (E_app (slice1, [vector1; start1; len1]), _); + | [(E_aux (E_app (op, [vector1; start1; len1]), _) as e1); E_aux (E_app (zeros2, _), _)] - when is_slice slice1 && is_zeros zeros2 && not (is_constant len1) -> - wrap (E_app (mk_id "is_zeros_slice", [vector1; start1; len1])) + when (is_slice op || is_subrange op) && is_zeros zeros2 + && not (is_constant_vec_typ env (typ_of e1)) && is_bitvector_typ (typ_of vector1) -> + let op' = if is_subrange op then "is_zero_subrange" else "is_zeros_slice" in + wrap (E_app (mk_id op', [vector1; start1; len1])) | _ -> E_app (id,args) else if is_id env (Id "IsZero") id then match args with | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when (is_id env (Id "vector_subrange") subrange1) && + when (is_id env (Id "vector_subrange") subrange1) && is_bitvector_typ (typ_of vector1) && not (is_constant_range (start1,end1)) -> E_app (mk_id "is_zero_subrange", [vector1; start1; end1]) | [E_aux (E_app (slice1, [vector1; start1; len1]),_)] - when (is_slice slice1) && + when (is_slice slice1) && is_bitvector_typ (typ_of vector1) && not (is_constant len1) -> E_app (mk_id "is_zeros_slice", [vector1; start1; len1]) | _ -> E_app (id,args) @@ -2945,55 +3176,59 @@ let rec rewrite_app env typ (id,args) = else if is_id env (Id "IsOnes") id then match args with | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when is_id env (Id "vector_subrange") subrange1 && + when is_id env (Id "vector_subrange") subrange1 && is_bitvector_typ (typ_of vector1) && not (is_constant_range (start1,end1)) -> E_app (mk_id "is_ones_subrange", [vector1; start1; end1]) | [E_aux (E_app (slice1, [vector1; start1; len1]),_)] - when is_slice slice1 && not (is_constant len1) -> + when is_slice slice1 && not (is_constant len1) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "is_ones_slice", [vector1; start1; len1]) | _ -> E_app (id,args) else if is_zero_extend || is_truncate then let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with - | [E_aux (E_app (append1, - [E_aux (E_app (subrange1, [vector1; start1; end1]), _); - (E_aux (E_app (zeros1, [len1]),_) | - E_aux (E_cast (_,E_aux (E_app (zeros1, [len1]),_)),_)) - ]),_)] - when is_subrange subrange1 && is_zeros zeros1 && is_append append1 - -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", length_arg @ [vector1; start1; end1; len1]))) + | [E_aux (E_app (append1, [E_aux (E_app (subrange1, [vector1; start1; end1]), _); zeros_exp]),_)] + when is_subrange subrange1 && is_zeros_exp zeros_exp && is_append append1 && is_bitvector_typ (typ_of vector1) -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> + try_cast_to_typ (rewrap (E_app (mk_id "place_subrange", length_arg @ [vector1; start1; end1; zlen]))) + | None -> E_app (id, args) + end - | [E_aux (E_app (append1, - [vector1; - (E_aux (E_app (zeros1, [length2]),_) | - E_aux (E_cast (_, E_aux (E_app (zeros1, [length2]),_)),_)) - ]),_)] - when is_constant_vec_typ env (typ_of vector1) && is_zeros zeros1 && is_append append1 - -> let (vector1, start1, length1) = - match vector1 with - | E_aux (E_app (slice1, [vector1; start1; length1]), _) -> - (vector1, start1, length1) - | _ -> - let (length1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of vector1)) in - (vector1, mk_exp (E_lit (mk_lit (L_num (Big_int.zero)))), mk_exp (E_sizeof length1)) - in - try_cast_to_typ (rewrap (E_app (mk_id "place_slice", length_arg @ [vector1; start1; length1; length2]))) + | [E_aux (E_app (append1, [vector1; zeros_exp]),_)] + when is_constant_vec_typ env (typ_of vector1) && is_zeros_exp zeros_exp && is_append append1 -> + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> + let (vector1, start1, length1) = + match vector1 with + | E_aux (E_app (slice1, [vector1; start1; length1]), _) -> + (vector1, start1, length1) + | _ -> + let (length1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of vector1)) in + (vector1, mk_exp (E_lit (mk_lit (L_num (Big_int.zero)))), mk_exp (E_sizeof length1)) + in + try_cast_to_typ (rewrap (E_app (mk_id "place_slice", length_arg @ [vector1; start1; length1; zlen]))) + | None -> E_app (id, args) + end (* If we've already rewritten to slice_slice_concat or subrange_subrange_concat, we can just drop the zero extension because those functions can do it themselves *) - | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice"),_) as op, args),_))),_)] + | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice" | Id "place_subrange"),_) as op, args),_))),_)] -> try_cast_to_typ (rewrap (E_app (op, length_arg @ args))) - | [E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice"),_) as op, args),_)] + | [E_aux (E_app (Id_aux ((Id "slice_slice_concat" | Id "subrange_subrange_concat" | Id "place_slice" | Id "place_subrange"),_) as op, args),_)] -> try_cast_to_typ (rewrap (E_app (op, length_arg @ args))) | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "zext_slice", length_arg @ [vector1; start1; length1]))) + | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_)] + when is_subrange subrange1 && not (is_constant hi1 && is_constant lo1) && is_bitvector_typ (typ_of vector1) -> + try_cast_to_typ (rewrap (E_app (mk_id "zext_subrange", length_arg @ [vector1; hi1; lo1]))) + | [E_aux (E_app (ones, [len1]),_)] when is_ones ones -> try_cast_to_typ (rewrap (E_app (mk_id "zext_ones", length_arg @ [len1]))) @@ -3005,7 +3240,7 @@ let rec rewrite_app env typ (id,args) = | [E_aux (E_app (zeros, [len1]),_)] | [E_aux (E_cast (_, E_aux (E_app (zeros, [len1]),_)), _)] when is_zeros zeros -> - try_cast_to_typ (rewrap (E_app (id, length_arg))) + try_cast_to_typ (rewrap (E_app (zeros, length_arg))) | _ -> E_app (id,args) @@ -3013,31 +3248,32 @@ let rec rewrite_app env typ (id,args) = let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in match List.filter (fun arg -> not (is_number (typ_of arg))) args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> try_cast_to_typ (rewrap (E_app (mk_id "sext_slice", length_arg @ [vector1; start1; length1]))) - | [E_aux (E_app (append, - [E_aux (E_app (subrange1, [vector1; start1; end1]), _); - (E_aux (E_app (zeros2, [len2]), _) | - E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) - ]), _)] - when is_append append && is_subrange subrange1 && is_zeros zeros2 && - not (is_constant len2) -> - E_app (mk_id "place_subrange_signed", length_arg @ [vector1; start1; end1; len2]) - - | [E_aux (E_app (append, - [E_aux (E_app (slice1, [vector1; start1; len1]), _); - (E_aux (E_app (zeros2, [len2]), _) | - E_aux (E_cast (_, E_aux (E_app (zeros2, [len2]), _)),_)) - ]), _)] - when is_append append && is_slice slice1 && is_zeros zeros2 && - not (is_constant len1 && is_constant len2) -> - E_app (mk_id "place_slice_signed", length_arg @ [vector1; start1; len1; len2]) + | [E_aux (E_app (subrange1, [vector1; hi1; lo1]),_) as exp1] + when is_subrange subrange1 && not (is_constant_vec_typ env (typ_of exp1)) + && is_bitvector_typ (typ_of vector1) -> + try_cast_to_typ (rewrap (E_app (mk_id "sext_subrange", length_arg @ [vector1; hi1; lo1]))) + + | [E_aux (E_app (append, [E_aux (E_app (op, [vector1; start1; len1]), _); zeros_exp]), _)] + when is_append append && (is_slice op || is_subrange op) && is_zeros_exp zeros_exp + && is_bitvector_typ (typ_of vector1) + && not (is_constant len1 && is_constant_vec_typ env (typ_of zeros_exp)) -> + let op' = if is_subrange op then "place_subrange_signed" else "place_slice_signed" in + begin match get_zeros_exp_len zeros_exp with + | Some zlen -> E_app (mk_id op', length_arg @ [vector1; start1; len1; zlen]) + | None -> E_app (id, args) + end | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "place_slice"),_), args),_))),_)] | [E_aux (E_app (Id_aux ((Id "place_slice"),_), args),_)] -> try_cast_to_typ (rewrap (E_app (mk_id "place_slice_signed", length_arg @ args))) + | [E_aux (E_cast (_, (E_aux (E_app (Id_aux ((Id "place_subrange"),_), args),_))),_)] + | [E_aux (E_app (Id_aux ((Id "place_subrange"),_), args),_)] + -> try_cast_to_typ (rewrap (E_app (mk_id "place_subrange_signed", length_arg @ args))) + (* If the original had a length, keep it *) (* | [E_aux (E_app (slice1, [vector1; start1; length1]),_);length2] when is_slice slice1 && not (is_constant length1) -> @@ -3064,24 +3300,65 @@ let rec rewrite_app env typ (id,args) = else if is_id env (Id "UInt") id || is_id env (Id "unsigned") id then match args with | [E_aux (E_app (slice1, [vector1; start1; length1]),_)] - when is_slice slice1 && not (is_constant length1) -> + when is_slice slice1 && not (is_constant length1) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "unsigned_slice", [vector1; start1; length1]) | [E_aux (E_app (subrange1, [vector1; start1; end1]),_)] - when is_subrange subrange1 && not (is_constant_range (start1,end1)) -> + when is_subrange subrange1 && not (is_constant_range (start1,end1)) && is_bitvector_typ (typ_of vector1) -> E_app (mk_id "unsigned_subrange", [vector1; start1; end1]) + | [E_aux (E_app (append, [vector1; zeros2]), _)] + when is_append append && is_zeros_exp zeros2 && not (is_constant_vec_typ env (typ_of zeros2)) -> + begin match get_zeros_exp_len zeros2 with + | Some len -> + E_app (mk_id "shl_int", [E_aux (E_app (id, [vector1]), (Unknown, empty_tannot)); len]) + | None -> E_app (id, args) + end + | _ -> E_app (id,args) - else if is_id env (Id "__SetSlice_bits") id then + else if is_id env (Id "__SetSlice_bits") id || is_id env (Id "SetSlice") id then match args with | [len; slice_len; vector; start; E_aux (E_app (zeros, _), _)] - when is_zeros zeros -> + when is_zeros zeros && is_bitvector_typ (typ_of vector) -> E_app (mk_id "set_slice_zeros", [len; vector; start; slice_len]) | _ -> E_app (id, args) + else if is_id env (Id "Replicate") id then + let length_arg = List.filter (fun arg -> is_number (typ_of arg)) args in + match List.filter (fun arg -> not (is_number (typ_of arg))) args with + | [E_aux (E_lit (L_aux (L_bin "0", _)), _)] -> + E_app (mk_id "sail_zeros", length_arg) + | [E_aux (E_lit (L_aux (L_bin "1", _)), _)] -> + E_app (mk_id "sail_ones", length_arg) + | _ -> E_app (id, args) + + (* Turn constant-length subranges into slices, making the constant length more explicit, + e.g. turning x[i+1 .. i] into slice(x, i, 2) *) + else if is_subrange id then + match get_constant_vec_len ~solve:true env typ, args with + | Some i, [vector1; start1; end1] + when is_bitvector_typ (typ_of vector1) && not (is_constant start1 && is_constant end1) -> + let inc = is_inc_vec (typ_of vector1) in + let low = if inc then start1 else end1 in + let exp' = rewrap (E_app (mk_id "slice", [vector1; low; mk_exp (E_lit (mk_lit (L_num i)))])) in + E_cast (bitvector_typ (nconstant i) (if inc then inc_ord else dec_ord), exp') + | _, _ -> E_app (id, args) + + (* Rewrite (v[x .. y] + i) to (v + (i << y))[x .. y], which is more amenable to further rewriting *) + else if is_id env (Id "add_bits_int") id then + match args with + | [E_aux (E_app (subrange1, [vec1; start1; end1]), a) as exp1; exp2] + when is_subrange subrange1 && is_bitvector_typ (typ_of vec1) + && not (is_constant_vec_typ env (typ_of exp1)) -> + let low = if is_inc_vec (typ_of vec1) then start1 else end1 in + let exp2' = mk_exp (E_app (mk_id "shl_int", [exp2; low])) in + let vec1' = E_aux (E_app (id, [vec1; exp2']), a) in + E_app (subrange1, [vec1'; start1; end1]) + | _ -> E_app (id, args) + else E_app (id,args) -let rewrite_aux = function +let rec rewrite_aux = function | E_app (id,args), (l, tannot) -> begin match destruct_tannot tannot with | Some (env, ty, _) -> @@ -3094,13 +3371,36 @@ let rewrite_aux = function annot when is_id (env_of_annot annot) (Id "vector_subrange") subrange2 && not (is_constant_range (start1, end1)) -> + let typ2 = Env.base_typ_of (env_of_annot annot) (typ_of vector2) in + let op = + if is_number typ2 then "vector_update_subrange_from_integer_subrange" else + "vector_update_subrange_from_subrange" + in E_aux (E_assign (LEXP_aux (LEXP_id id1,(l_id1,empty_tannot)), - E_aux (E_app (mk_id "vector_update_subrange_from_subrange", [ + E_aux (E_app (mk_id op, [ E_aux (E_id id1,(Generated l_id1,empty_tannot)); start1; end1; vector2; start2; end2]),(Unknown,empty_tannot))), (l_assign, empty_tannot)) - | exp,annot -> E_aux (exp,annot) + | E_assign (LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id1, annot1), start1, end1), _), + E_aux (E_app (zeros, _), _)), annot + when is_zeros (env_of_annot annot) zeros -> + let lhs = LEXP_aux (LEXP_id id1, annot1) in + let rhs = E_aux (E_app (mk_id "set_subrange_zeros", [E_aux (E_id id1, annot1); start1; end1]), annot1) in + E_aux (E_assign (lhs, rhs), annot) + | (E_let (LB_aux (LB_val (P_aux ((P_id id | P_typ (_, P_aux (P_id id, _))), _), + (E_aux (E_app (subrange1, [vec1; start1; end1]), _) as exp1)), _), + exp2) as e_aux), annot + when is_id (env_of_annot annot) (Id "vector_subrange") subrange1 + && not (is_constant_vec_typ (env_of_annot annot) (typ_of exp1))-> + let open Spec_analysis in + let depends1 = ids_in_exp exp1 in + let assigned2 = IdSet.union (assigned_vars exp2) (bound_vars exp2) in + if IdSet.is_empty (IdSet.inter depends1 assigned2) then rewrite_exp (subst id exp1 exp2) else + E_aux (e_aux, annot) + | e_aux, annot -> E_aux (e_aux, annot) + +and rewrite_exp exp = Rewriter.fold_exp { Rewriter.id_exp_alg with e_aux = rewrite_aux } exp let mono_rewrite defs = let open Rewriter in @@ -3253,16 +3553,6 @@ let make_bitvector_cast_cast cast_name top_env env quant_kids src_typ target_typ let _,_,f = make_bitvector_cast_fns cast_name top_env env quant_kids src_typ target_typ in f -let ids_in_exp exp = - let open Rewriter in - fold_exp { - (pure_exp_alg IdSet.empty IdSet.union) with - e_id = IdSet.singleton; - lEXP_id = IdSet.singleton; - lEXP_memory = (fun (id,s) -> List.fold_left IdSet.union (IdSet.singleton id) s); - lEXP_cast = (fun (_,id) -> IdSet.singleton id) - } exp - let make_bitvector_env_casts top_env env quant_kids insts exp = let mk_cast var typ exp = (make_bitvector_cast_let "bitvector_cast_in" env top_env quant_kids typ (subst_kids_typ insts typ)) var exp in let mk_assign_in var typ = @@ -3387,7 +3677,7 @@ let rec extract (E_aux (e,_)) = 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 add_bitvector_casts global_env (Defs defs) = let rewrite_body id quant_kids top_env ret_typ exp = let rewrite_aux (e,ann) = match e with @@ -3451,20 +3741,45 @@ let add_bitvector_casts (Defs defs) = let rec aux = function | [] -> [] | (E_aux (E_assert (assert_exp,msg),ann) as h)::t -> - let insts = extract assert_exp in - begin match insts with - | [] -> h::(aux t) - | _ -> - let t' = aux t in - let et = E_aux (E_block t',ann) in - let env = env_of h in - let insts = List.fold_left (fun insts (kid,i) -> - KBindings.add kid (nconstant i) insts) KBindings.empty insts in - let et = make_bitvector_env_casts env (env_of et) quant_kids insts et in - let src_typ = subst_kids_typ insts result_typ in - let et = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ et in - - [h; et] + (* Check the assertion for constraints that instantiate kids *) + let is_known_kid kid = KBindings.mem kid (Env.get_typ_vars env) in + let is_int_kid kid = try Env.get_typ_var kid env = K_int with _ -> false in + begin match Type_check.assert_constraint env true assert_exp with + | Some nc when KidSet.for_all is_known_kid (tyvars_of_constraint nc) -> + (* If the type checker can extract constraints from the assertion + for pre-existing kids (not for those that are bound by the + assertion itself), then look at the environment after the + assertion to extract kid instantiations. *) + let env_post = Env.add_constraint nc env in + let check_inst kid insts = + (* First check if the given kid already had a fixed value previously. *) + let rec nc_fixes_kid nc = match unaux_constraint nc with + | NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant _, _)) -> + Kid.compare kid kid' = 0 + | NC_and (_, _) -> List.exists nc_fixes_kid (constraint_conj nc) + | _ -> false + in + if List.exists nc_fixes_kid (Env.get_constraints env) then + insts + else + (* Otherwise ask the solver for a new, unique value *) + match solve_unique env_post (nvar kid) with + | Some n -> KBindings.add kid (nconstant n) insts + | None -> insts + | exception _ -> insts + in + let kids = KidSet.filter is_int_kid (tyvars_of_constraint nc) in + let insts = KidSet.fold check_inst (tyvars_of_constraint nc) KBindings.empty in + if KBindings.is_empty insts then h :: (aux t) else begin + (* Propagate new instantiations and insert casts *) + let t' = aux t in + let et = E_aux (E_block t',ann) in + let et = make_bitvector_env_casts env env_post quant_kids insts et in + let src_typ = subst_kids_typ insts result_typ in + let et = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ et in + [h; et] + end + | _ -> h :: (aux t) end | h::t -> h::(aux t) in E_aux (E_block (aux es),ann) @@ -3476,9 +3791,8 @@ let add_bitvector_casts (Defs defs) = e_aux = rewrite_aux } exp in let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),((l,_) as fcl_ann))) = - let fcl_env = env_of_annot fcl_ann in - let (tq,typ) = Env.get_val_spec_orig id fcl_env in - let fun_env = add_typquant l tq fcl_env in + let (tq,typ) = Env.get_val_spec_orig id global_env in + let fun_env = List.fold_right (Env.add_typ_var l) (quant_kopts tq) global_env in let quant_kids = List.map kopt_kid (List.filter is_int_kopt (quant_kopts tq)) in let ret_typ = match typ with @@ -3490,6 +3804,13 @@ let add_bitvector_casts (Defs defs) = in let pat,guard,body,annot = destruct_pexp pexp in let body = rewrite_body id quant_kids fun_env ret_typ body in + (* Cast function arguments, if necessary *) + let add_constraint insts = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid,_), nexp), _) -> KBindings.add kid nexp insts + | _ -> insts + in + let insts = List.fold_left add_constraint KBindings.empty (Env.get_constraints (env_of body)) in + let body = make_bitvector_env_casts fun_env (env_of body) quant_kids insts body in (* Also add a cast around the entire function clause body, if necessary *) let body = make_bitvector_cast_exp "bitvector_cast_out" fun_env quant_kids (fill_in_type (env_of body) (typ_of body)) ret_typ body @@ -3497,13 +3818,15 @@ let add_bitvector_casts (Defs defs) = let pexp = construct_pexp (pat,guard,body,annot) in FCL_aux (FCL_Funcl (id,pexp),fcl_ann) in - let rewrite_def = function - | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann)) -> + let rewrite_def idx = function + | DEF_fundef (FD_aux (FD_function (r,t,e,fcls),fd_ann) as fd) -> + Util.progress "Adding casts " (string_of_id (id_of_fundef fd)) idx (List.length defs); DEF_fundef (FD_aux (FD_function (r,t,e,List.map rewrite_funcl fcls),fd_ann)) | d -> d in specs_required := IdSet.empty; - let defs = List.map rewrite_def defs in + let defs = List.mapi rewrite_def defs in + let _ = Util.progress "Adding casts " "done" (List.length defs) (List.length defs) in let l = Generated Unknown in let Defs cast_specs,_ = (* TODO: use default/relevant order *) @@ -3789,6 +4112,6 @@ let monomorphise target opts splits defs = in defs let add_bitvector_casts = BitvectorSizeCasts.add_bitvector_casts -let rewrite_atoms_to_singletons defs = +let rewrite_atoms_to_singletons target defs = let defs, env = Type_check.check Type_check.initial_env defs in - AtomToItself.rewrite_size_parameters env defs + AtomToItself.rewrite_size_parameters target env defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 39d89461..f8a17494 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -69,7 +69,7 @@ val mono_rewrites : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs (* Add casts across case splits *) -val add_bitvector_casts : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) -val rewrite_atoms_to_singletons : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_atoms_to_singletons : string -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/parser.mly b/src/parser.mly index 6a579b7a..70f6f225 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1493,3 +1493,5 @@ defs: file: | defs Eof { $1 } + | Eof + { (Defs []) } diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 993934f5..b18541a3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -95,9 +95,9 @@ let rec fix_id remove_tick name = match name with | "with" | "check" | "field" - | "LT" - | "GT" - | "EQ" + | "LT" | "lt" | "lteq" + | "GT" | "gt" | "gteq" + | "EQ" | "eq" | "neq" | "integer" -> name ^ "'" | _ -> @@ -362,46 +362,63 @@ let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = lem_nexps_of_typ typ |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp)) -let replace_typ_size ctxt env (Typ_aux (t,a)) = +let rec replace_typ_size ctxt env (Typ_aux (t, a) as typ) = + let rewrap t = Typ_aux (t, a) in + let recur = replace_typ_size ctxt env in match t with - | Typ_app (Id_aux (Id "bitvector",_) as id, [A_aux (A_nexp size,_);ord]) -> - begin - let mk_typ nexp = - Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord]),a)) - in - match Type_check.solve_unique env size with - | Some n -> mk_typ (nconstant n) - | None -> - let is_equal nexp = - prove __POS__ 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 + | Typ_tup typs -> + begin match Util.option_all (List.map recur typs) with + | Some typs' -> Some (rewrap (Typ_tup typs')) + | None -> None end - (* - | Typ_app (Id_aux (Id "vector",_) as id, [A_aux (A_nexp size,_);ord;typ']) -> - begin - let mk_typ nexp = - Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) - in - match Type_check.solve_unique env size with - | Some n -> mk_typ (nconstant n) + | Typ_app (id, args) when contains_t_pp_var ctxt typ -> + begin match Util.option_all (List.map (replace_typ_arg_size ctxt env) args) with + | Some args' -> Some (rewrap (Typ_app (id, args'))) + | None -> None + end + | Typ_app _ -> Some typ + | Typ_id _ -> Some typ + | Typ_fn (argtyps, rtyp, eff) -> + begin match (Util.option_all (List.map recur argtyps), recur rtyp) with + | (Some argtyps', Some rtyp') -> Some (rewrap (Typ_fn (argtyps', rtyp', eff))) + | _ -> None + end + | Typ_var kid -> + let is_kid nexp = Nexp.compare nexp (nvar kid) = 0 in + if NexpSet.exists is_kid ctxt.bound_nexps then Some typ else None + | Typ_exist (kids, nc, typ) -> + begin match recur typ with + | Some typ' -> Some (rewrap (Typ_exist (kids, nc, typ'))) + | None -> None + end + | Typ_internal_unknown + | Typ_bidir (_, _, _) -> None +and replace_typ_arg_size ctxt env (A_aux (ta, a) as targ) = + let rewrap ta = A_aux (ta, a) in + match ta with + | A_nexp nexp -> + begin match Type_check.solve_unique env nexp with + | Some n -> Some (rewrap (A_nexp (nconstant n))) | None -> - let is_equal nexp = - prove __POS__ 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 + let is_equal nexp' = + prove __POS__ env (NC_aux (NC_equal (nexp,nexp'),Parse_ast.Unknown)) + in + match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp' -> Some (rewrap (A_nexp nexp')) | exception Not_found -> None end - *) - | _ -> None + | A_typ typ -> + begin match replace_typ_size ctxt env typ with + | Some typ' -> Some (rewrap (A_typ typ')) + | None -> None + end + | A_order _ | A_bool _ -> Some targ let make_printable_type ctxt env typ = if contains_t_pp_var ctxt typ then - match replace_typ_size ctxt env typ with - | None -> None - | Some typ -> Some typ + try replace_typ_size ctxt env (Env.expand_synonyms env typ) with + | _ -> None else Some typ let doc_tannot_lem ctxt env eff typ = @@ -529,8 +546,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) -> (* Isabelle does not seem to like type-annotated tuple patterns; it gives a syntax error. Avoid this by annotating the tuple elements instead *) - let doc_elem typ pat = - doc_pat_lem ctxt true (add_p_typ typ pat) in + let env = env_of_pat pa in + let doc_elem typ pat = doc_pat_lem ctxt true (add_p_typ env typ pat) in parens (separate comma_sp (List.map2 doc_elem typs pats)) | P_typ(typ,p) -> let doc_p = doc_pat_lem ctxt true p in @@ -901,7 +918,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_record tid env -> tid | _ -> raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + anglebars (space ^^ doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps) ^^ space) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = @@ -1367,8 +1384,11 @@ let doc_fun_body_lem ctxt exp = then align (string "catch_early_return" ^//^ parens (doc_exp)) else doc_exp -let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = - let typ = typ_of_annot annot in +let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), ((l, _) as annot))) = + let (tq, typ) = + try Env.get_val_spec_orig id type_env with + | _ -> raise (unreachable l __POS__ ("Could not get val-spec of " ^ string_of_id id)) + in let arg_typs = match typ with | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl") @@ -1377,7 +1397,7 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) = let ctxt = { early_ret = contains_early_return exp; bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ); - top_env = env_of_annot annot } in + top_env = type_env } in let pats, bind = untuple_args_pat pat arg_typs in let patspp = separate_map space (doc_pat_lem ctxt true) pats in let _ = match guard with @@ -1398,20 +1418,20 @@ module StringSet = Set.Make(String) (* Strictly speaking, Lem doesn't support multiple clauses for a single function joined by "and", although it has worked for Isabelle before. However, all the funcls should have been merged by the merge_funcls rewrite now. *) -let doc_fundef_rhs_lem (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) = - separate_map (hardline ^^ string "and ") doc_funcl_lem funcls +let doc_fundef_rhs_lem type_env (FD_aux(FD_function(r, typa, efa, funcls),fannot) as fd) = + separate_map (hardline ^^ string "and ") (doc_funcl_lem type_env) funcls -let doc_mutrec_lem = function +let doc_mutrec_lem type_env = function | [] -> failwith "DEF_internal_mutrec with empty function list" | fundefs -> string "let rec " ^^ - separate_map (hardline ^^ string "and ") doc_fundef_rhs_lem fundefs + separate_map (hardline ^^ string "and ") (doc_fundef_rhs_lem type_env) fundefs -let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = +let rec doc_fundef_lem type_env (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = match fcls with | [] -> failwith "FD_function with empty function list" | FCL_aux (FCL_Funcl(id, pexp),annot) :: _ - when not (Env.is_extern id (env_of_annot annot) "lem") -> + when not (Env.is_extern id type_env "lem") -> (* Output "rec" modifier if function calls itself. Mutually recursive functions are handled separately by doc_mutrec_lem. *) let is_funcl_rec = @@ -1422,7 +1442,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = pexp in let doc_rec = if is_funcl_rec then [string "rec"] else [] in - separate space ([string "let"] @ doc_rec @ [doc_fundef_rhs_lem fd]) + separate space ([string "let"] @ doc_rec @ [doc_fundef_rhs_lem type_env fd]) | _ -> empty @@ -1523,8 +1543,8 @@ let rec doc_def_lem type_env def = | DEF_reg_dec dec -> group (doc_dec_lem dec) | DEF_default df -> empty - | DEF_fundef fdef -> group (doc_fundef_lem fdef) ^/^ hardline - | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline + | DEF_fundef fdef -> group (doc_fundef_lem type_env fdef) ^/^ hardline + | DEF_internal_mutrec fundefs -> doc_mutrec_lem type_env fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, _), _) as lbind) -> group (doc_let_lem empty_ctxt lbind) ^/^ hardline | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" diff --git a/src/rewriter.ml b/src/rewriter.ml index 62870083..3b68f493 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -91,6 +91,17 @@ let lookup_generated_kid env kid = let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) +let rec is_src_typ typ = + match typ with + | Typ_aux (Typ_tup typs, l) -> List.for_all is_src_typ typs + | _ -> + match destruct_exist typ with + | Some (kopts, nc, typ') -> + let declared_kids = KidSet.of_list (List.map kopt_kid kopts) in + let unused_kids = KidSet.diff declared_kids (tyvars_of_typ typ') in + KidSet.is_empty unused_kids && KidSet.is_empty (generated_kids typ) + | None -> KidSet.is_empty (generated_kids typ) + let resolve_generated_kids env typ = let subst_kid kid typ = subst_kid typ_subst kid (lookup_generated_kid env kid) typ in KidSet.fold subst_kid (generated_kids typ) typ @@ -99,21 +110,31 @@ let rec remove_p_typ = function | P_aux (P_typ (typ, pat), _) -> remove_p_typ pat | pat -> pat -let add_p_typ typ (P_aux (paux, annot) as pat) = - let typ' = resolve_generated_kids (env_of_pat pat) typ in - if KidSet.is_empty (generated_kids typ') then - P_aux (P_typ (typ', remove_p_typ pat), annot) - else pat +let add_p_typ env typ (P_aux (paux, annot) as pat) = + let typ' = resolve_generated_kids env typ in + if is_src_typ typ' then P_aux (P_typ (typ', remove_p_typ pat), annot) else pat let rec remove_e_cast = function | E_aux (E_cast (_, exp), _) -> remove_e_cast exp | exp -> exp -let add_e_cast typ (E_aux (eaux, annot) as exp) = - let typ' = resolve_generated_kids (env_of exp) typ in - if KidSet.is_empty (generated_kids typ') then - E_aux (E_cast (typ', remove_e_cast exp), annot) - else exp +let add_e_cast env typ (E_aux (eaux, annot) as exp) = + let typ' = resolve_generated_kids env typ in + if is_src_typ typ' then E_aux (E_cast (typ', remove_e_cast exp), annot) else exp + +let add_typs_let env ltyp rtyp exp = + let aux pat lhs rhs = + let pat' = add_p_typ env ltyp pat in + (pat', lhs, rhs) + in + match exp with + | E_aux (E_let (LB_aux (LB_val (pat, lhs), lba), rhs), a) -> + let (pat', lhs', rhs') = aux pat lhs rhs in + E_aux (E_let (LB_aux (LB_val (pat', lhs'), lba), rhs'), a) + | E_aux (E_internal_plet (pat, lhs, rhs), a) -> + let (pat', lhs', rhs') = aux pat lhs rhs in + E_aux (E_internal_plet (pat', lhs', rhs'), a) + | _ -> exp let rec small (E_aux (exp,_)) = match exp with | E_id _ diff --git a/src/rewriter.mli b/src/rewriter.mli index 85f00453..f61bcc66 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -231,9 +231,11 @@ val pure_exp_alg : 'b -> ('b -> 'b -> 'b) -> val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot -val add_p_typ : typ -> tannot pat -> tannot pat +val add_p_typ : Env.t -> typ -> 'a pat -> 'a pat -val add_e_cast : typ -> tannot exp -> tannot exp +val add_e_cast : Env.t -> typ -> 'a exp -> 'a exp + +val add_typs_let : Env.t -> typ -> typ -> 'a exp -> 'a exp val effect_of_pexp : tannot pexp -> effect diff --git a/src/rewrites.ml b/src/rewrites.ml index 48ea78ae..35659bb4 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -385,7 +385,7 @@ let remove_vector_concat_pat pat = let id_pat = match typ_opt with - | Some typ -> add_p_typ typ (P_aux (P_id child,cannot)) + | Some typ -> add_p_typ env typ (P_aux (P_id child,cannot)) | None -> P_aux (P_id child,cannot) in let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in (letbind, @@ -716,6 +716,26 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_wild -> if is_irrefutable_pattern pat1 then Some [] else None | _ -> None +let vector_string_to_bits_pat (L_aux (lit, _) as l_aux) (l, tannot) = + let bit_annot = match destruct_tannot tannot with + | Some (env, _, _) -> mk_tannot env bit_typ no_effect + | None -> empty_tannot + in + begin match lit with + | L_hex _ | L_bin _ -> P_aux (P_vector (List.map (fun p -> P_aux (P_lit p, (l, bit_annot))) (vector_string_to_bit_list l_aux)), (l, tannot)) + | lit -> P_aux (P_lit l_aux, (l, tannot)) + end + +let vector_string_to_bits_exp (L_aux (lit, _) as l_aux) (l, tannot) = + let bit_annot = match destruct_tannot tannot with + | Some (env, _, _) -> mk_tannot env bit_typ no_effect + | None -> empty_tannot + in + begin match lit with + | L_hex _ | L_bin _ -> E_aux (E_vector (List.map (fun p -> E_aux (E_lit p, (l, bit_annot))) (vector_string_to_bit_list l_aux)), (l, tannot)) + | lit -> E_aux (E_lit l_aux, (l, tannot)) + end + (* A simple check for pattern disjointness; used for optimisation in the guarded pattern rewrite step *) let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = @@ -729,6 +749,14 @@ let rec disjoint_pat env (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) | P_id id, _ when id_is_unbound id env -> false | _, P_id id when id_is_unbound id env -> false | P_id id1, P_id id2 -> Id.compare id1 id2 <> 0 + | P_lit (L_aux ((L_bin _ | L_hex _), _) as lit), _ -> + disjoint_pat env (vector_string_to_bits_pat lit (Unknown, empty_tannot)) pat2 + | _, P_lit (L_aux ((L_bin _ | L_hex _), _) as lit) -> + disjoint_pat env pat1 (vector_string_to_bits_pat lit (Unknown, empty_tannot)) + | P_lit (L_aux (L_num n1, _)), P_lit (L_aux (L_num n2, _)) -> + not (Big_int.equal n1 n2) + | P_lit (L_aux (l1, _)), P_lit (L_aux (l2, _)) -> + l1 <> l2 | P_app (id1, args1), P_app (id2, args2) -> Id.compare id1 id2 <> 0 || List.exists2 (disjoint_pat env) args1 args2 | P_vector pats1, P_vector pats2 @@ -1221,21 +1249,13 @@ let rewrite_defs_vector_string_pats_to_bit_list env = let rewrite_p_aux (pat, (annot : tannot annot)) = let env = env_of_annot annot in match pat with - | P_lit (L_aux (lit, l) as l_aux) -> - begin match lit with - | L_hex _ | L_bin _ -> P_aux (P_vector (List.map (fun p -> P_aux (P_lit p, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l_aux)), annot) - | lit -> P_aux (P_lit l_aux, annot) - end + | P_lit lit -> vector_string_to_bits_pat lit annot | pat -> (P_aux (pat, annot)) in let rewrite_e_aux (exp, (annot : tannot annot)) = let env = env_of_annot annot in match exp with - | E_lit (L_aux (lit, l) as l_aux) -> - begin match lit with - | L_hex _ | L_bin _ -> E_aux (E_vector (List.map (fun e -> E_aux (E_lit e, (l, mk_tannot env bit_typ no_effect))) (vector_string_to_bit_list l_aux)), annot) - | lit -> E_aux (E_lit l_aux, annot) - end + | E_lit lit -> vector_string_to_bits_exp lit annot | exp -> (E_aux (exp, annot)) in let pat_alg = { id_pat_alg with p_aux = rewrite_p_aux } in @@ -1556,7 +1576,7 @@ let rewrite_defs_early_return env (Defs defs) = let eff = effect_of_annot tannot in let tannot' = mk_tannot env typ (union_effects eff (mk_effect [BE_escape])) in let exp' = match Env.get_ret_typ env with - | Some typ -> add_e_cast typ exp + | Some typ -> add_e_cast env typ exp | None -> exp in E_aux (E_app (mk_id "early_return", [exp']), (l, tannot')) | _ -> full_exp in @@ -2067,35 +2087,36 @@ let rewrite_vector_concat_assignments env defs = match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len | _ -> (Big_int.of_int 1) - else (Big_int.of_int 1) in + else (Big_int.of_int 1) + in let next i step = if is_order_inc ord then (Big_int.sub (Big_int.add i step) (Big_int.of_int 1), Big_int.add i step) - else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) in + else (Big_int.add (Big_int.sub i step) (Big_int.of_int 1), Big_int.sub i step) + in let i = match nexp_simp start with - | (Nexp_aux (Nexp_constant i, _)) -> i - | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) in + | (Nexp_aux (Nexp_constant i, _)) -> i + | _ -> if is_order_inc ord then Big_int.zero else Big_int.of_int (List.length lexps - 1) + in let l = gen_loc (fst annot) in - let exp' = - if small exp then strip_exp exp - else mk_exp (E_id (mk_id "split_vec")) in + let vec_id = mk_id "split_vec" in + let exp' = if small exp then strip_exp exp else mk_exp (E_id vec_id) in let lexp_to_exp (i, exps) lexp = let (j, i') = next i (len lexp) in let i_exp = mk_exp (E_lit (mk_lit (L_num i))) in let j_exp = mk_exp (E_lit (mk_lit (L_num j))) in let sub = mk_exp (E_vector_subrange (exp', i_exp, j_exp)) in - (i', exps @ [sub]) in + (i', exps @ [sub]) + in let (_, exps) = List.fold_left lexp_to_exp (i, []) lexps in - let tup = mk_exp (E_tuple exps) in - let lexp = LEXP_aux (LEXP_tup (List.map strip_lexp lexps), (l, ())) in - let e_aux = - if small exp then mk_exp (E_assign (lexp, tup)) - else mk_exp ( - E_let ( - mk_letbind (mk_pat (P_id (mk_id "split_vec"))) (strip_exp exp), - mk_exp (E_assign (lexp, tup)))) in + let assign lexp exp = mk_exp (E_assign (strip_lexp lexp, exp)) in + let block = mk_exp (E_block (List.map2 assign lexps exps)) in + let full_exp = + if small exp then block else + mk_exp (E_let (mk_letbind (mk_pat (P_id vec_id)) (strip_exp exp), block)) + in begin - try check_exp env e_aux unit_typ with + try check_exp env full_exp unit_typ with | Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) end @@ -2114,14 +2135,12 @@ let rewrite_tuple_assignments env defs = let env = env_of_annot annot in match e_aux with | E_assign (LEXP_aux (LEXP_tup lexps, _), exp) -> - (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *) let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in let block = mk_exp (E_block (List.mapi block_assign lexps)) in - let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) - (strip_exp exp) - in - let let_exp = mk_exp (E_let (letbind, block)) in + let pat = mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids)) in + let exp' = add_e_cast env (typ_of exp) exp in + let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in begin try check_exp env let_exp unit_typ with | Type_error (_, l, err) -> @@ -2162,9 +2181,11 @@ let rewrite_defs_remove_blocks env = let l = get_loc_exp v in let env = env_of v in let typ = typ_of v in - let wild = add_p_typ typ (annot_pat P_wild l env typ) in + let wild = annot_pat P_wild l env typ in let e_aux = E_let (annot_letbind (unaux_pat wild, v) l env typ, body) in - fix_eff_exp (annot_exp e_aux l env (typ_of body)) in + fix_eff_exp (annot_exp e_aux l env (typ_of body)) + |> add_typs_let env typ (typ_of body) + in let rec f l = function | [] -> E_aux (E_lit (L_aux (L_unit,gen_loc l)), (simple_annot l unit_typ)) @@ -2195,19 +2216,20 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp = | Some (env, typ, eff) when is_unit_typ typ -> let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in let body_typ = try typ_of body with _ -> unit_typ in - let wild = add_p_typ (typ_of v) (annot_pat P_wild l env (typ_of v)) in + let wild = annot_pat P_wild l env typ in let lb = fix_eff_lb (annot_letbind (unaux_pat wild, v) l env unit_typ) in fix_eff_exp (annot_exp (E_let (lb, body)) l env body_typ) + |> add_typs_let env typ body_typ | Some (env, typ, eff) -> let id = fresh_id "w__" l in - let pat = add_p_typ (typ_of v) (annot_pat (P_id id) l env (typ_of v)) in + let pat = annot_pat (P_id id) l env typ in let lb = fix_eff_lb (annot_letbind (unaux_pat pat, v) l env typ) in let body = body (annot_exp (E_id id) l env typ) in fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body)) + |> add_typs_let env typ (typ_of body) | None -> raise (Reporting.err_unreachable l __POS__ "no type information") - let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list -> 'a exp) : 'a exp = match l with | [] -> k [] @@ -2244,9 +2266,9 @@ let rewrite_defs_letbind_effects env = and n_pexp : 'b. bool -> 'a pexp -> ('a pexp -> 'b) -> 'b = fun newreturn pexp k -> match pexp with | Pat_aux (Pat_exp (pat,exp),annot) -> - k (fix_eff_pexp (Pat_aux (Pat_exp (pat,n_exp_term newreturn exp), annot))) + k (fix_eff_pexp (Pat_aux (Pat_exp (pat, n_exp_term newreturn exp), annot))) | Pat_aux (Pat_when (pat,guard,exp),annot) -> - k (fix_eff_pexp (Pat_aux (Pat_when (pat,n_exp_term newreturn guard,n_exp_term newreturn exp), annot))) + k (fix_eff_pexp (Pat_aux (Pat_when (pat, n_exp_term newreturn guard, n_exp_term newreturn exp), annot))) and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp = mapCont (n_pexp newreturn) pexps k @@ -2300,15 +2322,15 @@ let rewrite_defs_letbind_effects env = and n_lexpL (lexps : 'a lexp list) (k : 'a lexp list -> 'a exp) : 'a exp = mapCont n_lexp lexps k - and n_exp_term (newreturn : bool) (exp : 'a exp) : 'a exp = + and n_exp_term ?cast:(cast=false) (newreturn : bool) (exp : 'a exp) : 'a exp = let (E_aux (_,(l,tannot))) = exp in let exp = if newreturn then (* let typ = try typ_of exp with _ -> unit_typ in *) - let exp = add_e_cast (typ_of exp) exp in + let exp = if cast then add_e_cast (env_of exp) (typ_of exp) exp else exp in annot_exp (E_internal_return exp) l (env_of exp) (typ_of exp) - else - exp in + else exp + in (* n_exp_term forces an expression to be translated into a form "let .. let .. let .. in EXP" where EXP has no effect and does not update variables *) @@ -2331,8 +2353,8 @@ let rewrite_defs_letbind_effects env = (* Leave effectful operands of Boolean "and"/"or" in place to allow short-circuiting. *) let newreturn = effectful l || effectful r in - let l = n_exp_term newreturn l in - let r = n_exp_term newreturn r in + let l = n_exp_term ~cast:true newreturn l in + let r = n_exp_term ~cast:true newreturn r in k (rewrap (E_app (op_bool, [l; r]))) | E_app (id,exps) -> n_exp_nameL exps (fun exps -> @@ -2351,7 +2373,8 @@ let rewrite_defs_letbind_effects env = let newreturn = effectful exp2 || effectful exp3 in let exp2 = n_exp_term newreturn exp2 in let exp3 = n_exp_term newreturn exp3 in - k (rewrap (E_if (exp1,exp2,exp3))) in + k (rewrap (E_if (exp1,exp2,exp3))) + in if value exp1 then e_if (n_exp_term false exp1) else n_exp_name exp1 e_if | E_for (id,start,stop,by,dir,body) -> n_exp_name start (fun start -> @@ -2365,7 +2388,7 @@ let rewrite_defs_letbind_effects env = | Measure_aux (Measure_some exp,l) -> Measure_aux (Measure_some (n_exp_term false exp),l) in - let cond = n_exp_term (effectful cond) cond in + let cond = n_exp_term ~cast:true (effectful cond) cond in let body = n_exp_term (effectful body) body in k (rewrap (E_loop (loop,measure,cond,body))) | E_vector exps -> @@ -2437,7 +2460,7 @@ let rewrite_defs_letbind_effects env = | E_assert (exp1,exp2) -> n_exp_name exp1 (fun exp1 -> n_exp_name exp2 (fun exp2 -> - k (rewrap (E_assert (exp1,exp2))))) + k (rewrap (E_assert (exp1, exp2))))) | E_var (lexp,exp1,exp2) -> n_lexp lexp (fun lexp -> n_exp exp1 (fun exp1 -> @@ -2505,7 +2528,7 @@ let rewrite_defs_internal_lets env = let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with | LEXP_id id -> P_aux (P_id id, annot) - | LEXP_cast (typ, id) -> add_p_typ typ (P_aux (P_id id, annot)) + | LEXP_cast (typ, id) -> add_p_typ (env_of_annot annot) typ (P_aux (P_id id, annot)) | LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot) | _ -> raise (Reporting.err_unreachable l __POS__ "unexpected local lexp") in @@ -2524,7 +2547,7 @@ let rewrite_defs_internal_lets env = | LEXP_aux (_,lexp_annot') -> lexp_annot' | exception _ -> lannot) in - let rhs = add_e_cast ltyp (rhs exp) in + let rhs = add_e_cast (env_of exp) ltyp (rhs exp) in E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs), annot), body) | LB_aux (LB_val (pat,exp'),annot') -> if effectful exp' @@ -2536,7 +2559,7 @@ let rewrite_defs_internal_lets env = | LEXP_aux (LEXP_id id, annot) -> (P_id id, annot) | LEXP_aux (LEXP_cast (typ, id), annot) -> - (unaux_pat (add_p_typ typ (P_aux (P_id id, annot))), annot) + (unaux_pat (add_p_typ (env_of_annot annot) typ (P_aux (P_id id, annot))), annot) | _ -> failwith "E_var with unexpected lexp" in if effectful exp1 then E_internal_plet (P_aux (paux, annot), exp1, exp2) @@ -2566,7 +2589,7 @@ let fold_typed_guards env guards = | g :: gs -> List.fold_left (fun g g' -> annot_exp (E_app (mk_id "and_bool", [g; g'])) Parse_ast.Unknown env bool_typ) g gs -let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (l, _)) as pexp) = +let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) = let guards = ref [] in match pexp_aux with @@ -2576,13 +2599,13 @@ let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (l, _)) as pexp) = match !guards with | [] -> pexp | gs -> - let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp) end | Pat_when (pat, guard, exp) -> begin let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in - let unchecked_pexp = mk_pexp ~loc:l (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in check_case (env_of_pat pat) (typ_of_pat pat) unchecked_pexp (typ_of exp) end @@ -3334,22 +3357,24 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let tuple_exp = function | [] -> annot_exp (E_lit (mk_lit L_unit)) l env unit_typ | [e] -> e - | es -> annot_exp (E_tuple es) l env (tuple_typ (List.map typ_of es)) in + | es -> annot_exp (E_tuple es) l env (tuple_typ (List.map typ_of es)) + in let tuple_pat = function | [] -> annot_pat P_wild l env unit_typ | [pat] -> let typ = typ_of_pat pat in - add_p_typ typ pat + add_p_typ env typ pat | pats -> let typ = tuple_typ (List.map typ_of_pat pats) in - add_p_typ typ (annot_pat (P_tup pats) l env typ) in + add_p_typ env typ (annot_pat (P_tup pats) l env typ) + in let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars = match expaux with | E_let (lb,exp) -> let exp = add_vars overwrite exp vars in - E_aux (E_let (lb,exp),swaptyp (typ_of exp) annot) + E_aux (E_let (lb,exp), swaptyp (typ_of exp) annot) | E_var (lexp,exp1,exp2) -> let exp2 = add_vars overwrite exp2 vars in E_aux (E_var (lexp,exp1,exp2), swaptyp (typ_of exp2) annot) @@ -3358,7 +3383,11 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = E_aux (E_internal_plet (pat,exp1,exp2), swaptyp (typ_of exp2) annot) | E_internal_return exp2 -> let exp2 = add_vars overwrite exp2 vars in - E_aux (E_internal_return exp2,swaptyp (typ_of exp2) annot) + E_aux (E_internal_return exp2, swaptyp (typ_of exp2) annot) + | E_cast (typ, exp) -> + let (E_aux (expaux, annot) as exp) = add_vars overwrite exp vars in + let typ' = typ_of exp in + add_e_cast (env_of exp) typ' (E_aux (expaux, swaptyp typ' annot)) | _ -> (* after rewrite_defs_letbind_effects there cannot be terms that have effects/update local variables in "tail-position": check n_exp_term @@ -3367,6 +3396,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let lb = LB_aux (LB_val (P_aux (P_wild, annot), exp), annot) in let exp' = tuple_exp vars in E_aux (E_let (lb, exp'), swaptyp (typ_of exp') annot) + |> add_typs_let env (typ_of exp) (typ_of exp') else tuple_exp (exp :: vars) in let mk_var_exps_pats l env ids = @@ -3378,7 +3408,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = exp, P_aux (P_id id, a)) |> List.split in - let rewrite used_vars (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (paux,(pl,pannot)) as pat) = + let rec rewrite used_vars (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (paux,(pl,pannot)) as pat) = let env = env_of_annot annot in let overwrite = match paux with | P_wild | P_typ (_, P_aux (P_wild, _)) -> true @@ -3417,11 +3447,15 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = in let lvar_nc = nc_and (nc_lteq (nvar lower_kid) (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) (nvar upper_kid)) in let lvar_typ = mk_typ (Typ_exist (List.map (mk_kopt K_int) [lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in - let lvar_pat = unaux_pat (add_p_typ lvar_typ (annot_pat (P_var ( + let lvar_pat = unaux_pat (annot_pat (P_var ( annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)), - TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in + TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ) + in let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in - let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in + let body = + fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) + |> add_typs_let env lvar_typ (typ_of exp4) + in (* If lower > upper, the loop body never gets executed, and the type checker might not be able to prove that the initial value exp1 satisfies the constraints on the loop variable. @@ -3521,7 +3555,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | E_assign (lexp,vexp) -> let mk_id_pat id = let typ = lvar_typ (Env.lookup_id id env) in - add_p_typ typ (annot_pat (P_id id) pl env typ) + add_p_typ env typ (annot_pat (P_id id) pl env typ) in if effectful exp then Same_vars (E_aux (E_assign (lexp,vexp),annot)) @@ -3531,7 +3565,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let pat = annot_pat (P_id id) pl env (typ_of vexp) in Added_vars (vexp, mk_id_pat id) | LEXP_aux (LEXP_cast (typ,id),annot) -> - let pat = add_p_typ typ (annot_pat (P_id id) pl env (typ_of vexp)) in + let pat = add_p_typ env typ (annot_pat (P_id id) pl env (typ_of vexp)) in Added_vars (vexp,pat) | LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) -> let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in @@ -3545,6 +3579,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let pat = annot_pat (P_id id) pl env (typ_of vexp) in Added_vars (vexp,pat) | _ -> Same_vars (E_aux (E_assign (lexp,vexp),annot))) + | E_cast (typ, exp) -> + begin match rewrite used_vars exp pat with + | Added_vars (exp', pat') -> + Added_vars (add_e_cast (env_of exp') (typ_of exp') exp', pat') + | Same_vars (exp') -> + Same_vars (E_aux (E_cast (typ, exp'), annot)) + end | _ -> (* after rewrite_defs_letbind_effects this expression is pure and updates no variables: check n_exp_term and where it's used. *) @@ -3565,7 +3606,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | LEXP_aux (LEXP_id id, _) -> P_id id, typ_of v | LEXP_aux (LEXP_cast (typ, id), _) -> - unaux_pat (add_p_typ typ (annot_pat (P_id id) l env (typ_of v))), typ + unaux_pat (add_p_typ env typ (annot_pat (P_id id) l env (typ_of v))), typ | _ -> raise (Reporting.err_unreachable l __POS__ "E_var with a lexp that is not a variable") in @@ -3579,6 +3620,9 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = rewrite_var_updates exp' | E_internal_plet (pat,v,body) -> failwith "rewrite_var_updates: E_internal_plet shouldn't be introduced yet" + | E_cast (typ, exp) -> + let exp' = rewrite_var_updates exp in + E_aux (E_cast (typ, exp'), annot) (* There are no other expressions that have effects or variable updates in "tail-position": check the definition nexp_term and where it is used. *) | _ -> exp @@ -3714,7 +3758,7 @@ let rewrite_defs_remove_superfluous_returns env = let add_opt_cast typopt1 typopt2 annot exp = match typopt1, typopt2 with - | Some typ, _ | _, Some typ -> add_e_cast typ exp + | Some typ, _ | _, Some typ -> add_e_cast (env_of exp) typ exp | None, None -> exp in @@ -3765,11 +3809,11 @@ let rewrite_defs_remove_superfluous_returns env = let rewrite_defs_remove_e_assign env (Defs defs) = let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs - [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars"); - ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); - ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars"); - ("while#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars"); - ("until#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars")]))) in + [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("until#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out"); + ("while#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out"); + ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in let rewrite_exp _ e = replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in rewrite_defs_base @@ -4752,6 +4796,36 @@ let rec move_loop_measures (Defs defs) = in Defs (List.rev rev_defs) +let rewrite_toplevel_consts target type_env (Defs defs) = + let istate = Constant_fold.initial_state (Defs defs) type_env in + let subst consts exp = + let open Rewriter in + let used_ids = fold_exp { (pure_exp_alg IdSet.empty IdSet.union) with e_id = IdSet.singleton } exp in + let subst_ids = IdSet.filter (fun id -> Bindings.mem id consts) used_ids in + IdSet.fold (fun id -> subst id (Bindings.find id consts)) subst_ids exp + in + let rewrite_def (revdefs, consts) = function + | DEF_val (LB_aux (LB_val (pat, exp), a) as lb) -> + begin match unaux_pat pat with + | P_id id | P_typ (_, P_aux (P_id id, _)) -> + let exp' = Constant_fold.rewrite_exp_once target istate (subst consts exp) in + if Constant_fold.is_constant exp' then + try + let exp' = infer_exp (env_of exp') (strip_exp exp') in + let pannot = (pat_loc pat, mk_tannot (env_of_pat pat) (typ_of exp') no_effect) in + let pat' = P_aux (P_typ (typ_of exp', P_aux (P_id id, pannot)), pannot) in + let consts' = Bindings.add id exp' consts in + (DEF_val (LB_aux (LB_val (pat', exp'), a)) :: revdefs, consts') + with + | _ -> (DEF_val lb :: revdefs, consts) + else (DEF_val lb :: revdefs, consts) + | _ -> (DEF_val lb :: revdefs, consts) + end + | def -> (def :: revdefs, consts) + in + let (revdefs, _) = List.fold_left rewrite_def ([], Bindings.empty) defs in + Defs (List.rev revdefs) + let opt_mono_rewrites = ref false let opt_mono_complex_nexps = ref true @@ -4851,10 +4925,10 @@ let all_rewrites = [ ("mapping_builtins", Basic_rewriter rewrite_defs_mapping_patterns); ("mono_rewrites", Basic_rewriter mono_rewrites); ("toplevel_nexps", Basic_rewriter rewrite_toplevel_nexps); + ("toplevel_consts", String_rewriter (fun target -> Basic_rewriter (rewrite_toplevel_consts target))); ("monomorphise", String_rewriter (fun target -> Basic_rewriter (monomorphise target))); - ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); - ("add_bitvector_casts", Basic_rewriter (fun _ -> Monomorphise.add_bitvector_casts)); - ("atoms_to_singletons", Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons)); + ("atoms_to_singletons", String_rewriter (fun target -> (Basic_rewriter (fun _ -> Monomorphise.rewrite_atoms_to_singletons target)))); + ("add_bitvector_casts", Basic_rewriter Monomorphise.add_bitvector_casts); ("remove_impossible_int_cases", Basic_rewriter Constant_propagation.remove_impossible_int_cases); ("const_prop_mutrec", String_rewriter (fun target -> Basic_rewriter (Constant_propagation_mutrec.rewrite_defs target))); ("make_cases_exhaustive", Basic_rewriter MakeExhaustive.rewrite); @@ -4902,17 +4976,18 @@ let rewrites_lem = [ ("mono_rewrites", []); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); + ("toplevel_consts", [String_arg "lem"; If_mwords_arg]); ("toplevel_nexps", [If_mono_arg]); ("monomorphise", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); ("add_bitvector_casts", [If_mwords_arg]); - ("atoms_to_singletons", [If_mono_arg]); + ("atoms_to_singletons", [String_arg "lem"; If_mono_arg]); ("recheck_defs", [If_mwords_arg]); ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); @@ -4953,8 +5028,8 @@ let rewrites_coq = [ ("vector_string_pats_to_bit_list", []); ("remove_not_pats", []); ("remove_impossible_int_cases", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); @@ -5002,8 +5077,8 @@ let rewrites_ocaml = [ ("mapping_builtins", []); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []); ("remove_not_pats", []); ("remove_vector_concat", []); @@ -5026,7 +5101,7 @@ let rewrites_c = [ ("recheck_defs", [If_mono_arg]); ("toplevel_nexps", [If_mono_arg]); ("monomorphise", [String_arg "c"; If_mono_arg]); - ("atoms_to_singletons", [If_mono_arg]); + ("atoms_to_singletons", [String_arg "c"; If_mono_arg]); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); ("vector_string_pats_to_bit_list", []); @@ -5034,10 +5109,8 @@ let rewrites_c = [ ("remove_vector_concat", []); ("remove_bitvector_pats", []); ("pattern_literals", [Literal_arg "all"]); - ("vector_concat_assignments", []); ("tuple_assignments", []); ("vector_concat_assignments", []); - ("tuple_assignments", []); ("simple_assignments", []); ("exp_lift_assign", []); ("merge_function_clauses", []); @@ -5052,8 +5125,8 @@ let rewrites_interpreter = [ ("pat_string_append", []); ("mapping_builtins", []); ("undefined", [Bool_arg false]); - ("vector_concat_assignments", []); ("tuple_assignments", []); + ("vector_concat_assignments", []); ("simple_assignments", []) ] diff --git a/src/sail.ml b/src/sail.ml index 772d8564..34fffd2e 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -653,4 +653,5 @@ let _ = try with Reporting.Fatal_error e -> Reporting.print_error e; Interactive.opt_suppress_banner := true; + if !opt_memo_z3 then Constraint.save_digests () else (); if !Interactive.opt_interactive then () else exit 1 diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 4814554b..542ecaae 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -602,11 +602,11 @@ let top_sort_defs (Defs defs) = let assigned_vars exp = - fst (Rewriter.fold_exp - { (Rewriter.compute_exp_alg IdSet.empty IdSet.union) with - Rewriter.lEXP_id = (fun id -> IdSet.singleton id, LEXP_id id); - Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id, LEXP_cast (ty,id)) } - exp) + (Rewriter.fold_exp + { (Rewriter.pure_exp_alg IdSet.empty IdSet.union) with + Rewriter.lEXP_id = (fun id -> IdSet.singleton id); + Rewriter.lEXP_cast = (fun (ty,id) -> IdSet.singleton id) } + exp) let assigned_vars_in_fexps fes = List.fold_left @@ -633,6 +633,14 @@ let rec assigned_vars_in_lexp (LEXP_aux (le,_)) = | LEXP_field (le,_) -> assigned_vars_in_lexp le | LEXP_deref e -> assigned_vars e +let bound_vars exp = + let open Rewriter in + let pat_alg = { + (pure_pat_alg IdSet.empty IdSet.union) with + p_id = IdSet.singleton; + p_as = (fun (ids, id) -> IdSet.add id ids) + } in + fold_exp { (pure_exp_alg IdSet.empty IdSet.union) with pat_alg = pat_alg } exp let pat_id_is_variable env id = match Type_check.Env.lookup_id id env with diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 8586ac15..41ab9b6c 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -84,9 +84,10 @@ val assigned_vars_in_fexps : 'a fexp list -> IdSet.t val assigned_vars_in_pexp : 'a pexp -> IdSet.t val assigned_vars_in_lexp : 'a lexp -> IdSet.t -(** Variable bindings in patterns *) +(** Variable bindings in patterns and expressions *) val pat_id_is_variable : env -> id -> bool val bindings_from_pat : tannot pat -> id list +val bound_vars : 'a exp -> IdSet.t val equal_kids_ncs : kid -> n_constraint list -> KidSet.t val equal_kids : env -> kid -> KidSet.t diff --git a/src/state.ml b/src/state.ml index 478a3fd5..8d487d3e 100644 --- a/src/state.ml +++ b/src/state.ml @@ -410,12 +410,12 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id' = remove_trailing_underscores id in separate_map hardline string [ "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = readS (" ^ id' ^ " \\<circ> regstate)\""; - " by (auto simp: liftState_read_reg_readS register_defs)"; + " \"\\<lbrakk>read_reg " ^ id ^ "_ref\\<rbrakk>\\<^sub>S = read_regS " ^ id ^ "_ref\""; + " by (intro liftState_read_reg) (auto simp: register_defs)"; ""; "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; - " \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; - " by (auto simp: liftState_write_reg_updateS register_defs)" + " \"\\<lbrakk>write_reg " ^ id ^ "_ref v\\<rbrakk>\\<^sub>S = write_regS " ^ id ^ "_ref v\""; + " by (intro liftState_write_reg) (auto simp: register_defs)" ] in string "abbreviation liftS (\"\\<lbrakk>_\\<rbrakk>\\<^sub>S\") where \"liftS \\<equiv> liftState (get_regval, set_regval)\"" ^^ diff --git a/src/type_check.ml b/src/type_check.ml index 73cb8a57..e471f33d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3663,18 +3663,18 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = let inferred_exp2 = infer_exp env exp2 in let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in - let (len, check) = match ord with + let (slice_len, check) = match ord with | Ord_aux (Ord_inc, _) -> (nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)), - nc_lteq nexp1 nexp2) + nc_and (nc_and (nc_lteq (nint 0) nexp1) (nc_lteq nexp1 nexp2)) (nc_lt nexp2 len)) | Ord_aux (Ord_dec, _) -> (nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)), - nc_gteq nexp1 nexp2) + nc_and (nc_and (nc_lteq (nint 0) nexp2) (nc_lteq nexp2 nexp1)) (nc_lt nexp1 len)) | Ord_aux (Ord_var _, _) -> typ_error env l "Slice assignment to bitvector with variable indexing order unsupported" in if !opt_no_lexp_bounds_check || prove __POS__ env check then - annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord) + annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ slice_len ord) else typ_raise env l (Err_lexp_bounds (check, Env.get_locals env, Env.get_constraints env)) | _ -> typ_error env l "Cannot assign slice of non vector type" @@ -3882,7 +3882,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | Measure_aux (Measure_some exp,l) -> Measure_aux (Measure_some (crule check_exp env exp int_typ),l) in - let checked_body = crule check_exp (add_opt_constraint (assert_constraint env true checked_cond) env) body unit_typ in + let nc = match loop_type with + | While -> assert_constraint env true checked_cond + | Until -> None + in + let checked_body = crule check_exp (add_opt_constraint nc env) body unit_typ in annot_exp (E_loop (loop_type, checked_measure, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin diff --git a/src/type_check.mli b/src/type_check.mli index fba5575a..ff839f50 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -319,6 +319,8 @@ val infer_lexp : Env.t -> unit lexp -> tannot lexp val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp +val check_funcl : Env.t -> 'a funcl -> typ -> tannot funcl + val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t diff --git a/test/c/run_tests.py b/test/c/run_tests.py index ff9aa952..28a4d28d 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -21,12 +21,12 @@ def test_c(name, c_opts, sail_opts, valgrind): tests[filename] = os.fork() if tests[filename] == 0: step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) - step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename)) - step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) + step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}.bin'.format(c_opts, basename, sail_dir, sail_dir, basename)) + step('./{}.bin 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: - step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) - step('rm {}.c {} {}.result'.format(basename, basename, basename)) + step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}.bin".format(basename), expected_status = 1 if basename == "exception" else 0) + step('rm {}.c {}.bin {}.result'.format(basename, basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -62,7 +62,7 @@ def test_interpreter(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename)) + step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename)) step('diff {}.iresult {}.expect'.format(basename, basename)) step('rm {}.iresult'.format(basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) @@ -79,11 +79,11 @@ def test_ocaml(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename)) - step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) + step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {}_ocaml {}'.format(basename, basename, filename)) + step('./{}_ocaml 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) step('rm -r _sbuild_{}'.format(basename)) - step('rm {}.oresult {}'.format(basename, basename)) + step('rm {}.oresult {}_ocaml'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index db73580f..da6bce69 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -5,7 +5,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" SAILDIR="$DIR/../.." TYPECHECKTESTSDIR="$DIR/../typecheck/pass" EXTRATESTSDIR="$DIR/pass" -BBVDIR="$DIR/../../../bbv/theories" +BBVDIR="$DIR/../../../bbv/src/bbv" RED='\033[0;31m' GREEN='\033[0;32m' diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail index 0501cf1e..4540f1a5 100644 --- a/test/mono/itself_rewriting.sail +++ b/test/mono/itself_rewriting.sail @@ -1,5 +1,6 @@ $include <smt.sail> $include <flow.sail> +$include <arith.sail> default Order dec type bits ('n : Int) = bitvector('n, dec) val operator & = "and_bool" : (bool, bool) -> bool @@ -67,10 +68,43 @@ function willsplit(x) = { shadowed(n); } +val execute : forall 'datasize. int('datasize) -> unit + +function execute(datasize) = { + let x : bits('datasize) = replicate_bits(0b1, datasize); + () +} + +val test_execute : unit -> unit + +function test_execute() = { + let exp = 4; + let 'datasize = shl_int(1, exp); + execute(datasize) +} + +val transitive_itself : forall 'n. int('n) -> unit + +function transitive_itself(n) = { + needs_size_in_guard(n); + () +} + +val transitive_split : bool -> unit + +function transitive_split(x) = { + let n = if x then 8 else 16; + transitive_itself(n); +} + val run : unit -> unit effect {escape} function run () = { assert(true); /* To force us into the monad */ + test_execute(); willsplit(true); willsplit(false); -}
\ No newline at end of file + transitive_itself(16); + transitive_split(true); + transitive_split(false); +} diff --git a/test/typecheck/pass/floor_pow2.sail b/test/typecheck/pass/floor_pow2.sail new file mode 100644 index 00000000..fa8680cf --- /dev/null +++ b/test/typecheck/pass/floor_pow2.sail @@ -0,0 +1,17 @@ +$include <arith.sail> + +val "pow2" : forall 'n, 'n >= 0. int('n) -> int(2 ^ 'n) + +val floor_pow2 : forall ('x : Int), 'x >= 0. int('x) -> int + +function floor_pow2 x = { + if x == 0 then { + return(0); + } else { + n : {'n, 'n >= 1. int('n)} = 1; + while x >= pow2(n) do { + n = n + 1 + }; + return(pow2(n - 1)) + } +} diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect index 90166904..8854282d 100644 --- a/test/typecheck/pass/reg_32_64/v2.expect +++ b/test/typecheck/pass/reg_32_64/v2.expect @@ -1,13 +1,11 @@ Type error: -[[96mreg_32_64/v2.sail[0m]:21:18-22 +[[96mreg_32_64/v2.sail[0m]:21:2-15 21[96m |[0m (*R)['d .. 0] = data - [91m |[0m [91m^--^[0m - [91m |[0m Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data - [91m |[0m Coercion failed because: - [91m |[0m Mismatched argument types in subtype check + [91m |[0m [91m^-----------^[0m + [91m |[0m Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64) [91m |[0m This error was caused by: [91m |[0m [[96mreg_32_64/v2.sail[0m]:21:2-15 [91m |[0m 21[96m |[0m (*R)['d .. 0] = data [91m |[0m [91m |[0m [91m^-----------^[0m - [91m |[0m [91m |[0m Mismatched argument types in subtype check + [91m |[0m [91m |[0m Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64) [91m |[0m diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail new file mode 100644 index 00000000..6d63f2e8 --- /dev/null +++ b/test/typecheck/pass/repeat_constraint.sail @@ -0,0 +1,9 @@ +$include <flow.sail> + +val main : unit -> unit + +function main() = { + repeat { + _not_prove(constraint(false)); + } until (false); +} diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect new file mode 100644 index 00000000..9d561e11 --- /dev/null +++ b/test/typecheck/pass/repeat_constraint/v1.expect @@ -0,0 +1,6 @@ +Type error: +[[96mrepeat_constraint/v1.sail[0m]:7:4-29 +7[96m |[0m _prove(constraint(false)); + [91m |[0m [91m^-----------------------^[0m + [91m |[0m Cannot prove false + [91m |[0m diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail new file mode 100644 index 00000000..5dd2f513 --- /dev/null +++ b/test/typecheck/pass/repeat_constraint/v1.sail @@ -0,0 +1,9 @@ +$include <flow.sail> + +val main : unit -> unit + +function main() = { + repeat { + _prove(constraint(false)); + } until (false); +} |