diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 6 | ||||
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 28 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 114 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 19 | ||||
| -rw-r--r-- | lib/reverse_endianness.sail | 32 | ||||
| -rw-r--r-- | lib/sail.c | 24 | ||||
| -rw-r--r-- | lib/sail.h | 2 | ||||
| -rw-r--r-- | lib/string.sail | 2 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 9 |
9 files changed, 225 insertions, 11 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index d04c7988..7c002e1c 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -82,7 +82,7 @@ overload shr_int = {_shr32, _shr_int} val tdiv_int = { ocaml: "tdiv_int", interpreter: "tdiv_int", - lem: "integerDiv_t", + lem: "tdiv_int", c: "tdiv_int", coq: "Z.quot" } : (int, int) -> int @@ -91,7 +91,7 @@ val tdiv_int = { val tmod_int = { ocaml: "tmod_int", interpreter: "tmod_int", - lem: "integerMod_t", + lem: "tmod_int", c: "tmod_int", coq: "Z.rem" } : (int, int) -> nat @@ -100,7 +100,7 @@ val abs_int = { smt : "abs", ocaml: "abs_int", interpreter: "abs_int", - lem: "abs_int", + lem: "integerAbs", c: "abs_int", coq: "Z.abs" } : int -> int diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 9b5888c7..739a22d0 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -499,5 +499,33 @@ Definition set_slice_int len n lo (v : mword len) : Z := (int_of_mword true (update_subrange_vec_dec bs hi lo v)) else n. +(* Variant of bitvector slicing for the ARM model with few constraints *) +Definition slice {m} (v : mword m) lo len `{ArithFact (0 <= len)} : mword len := + if sumbool_of_bool (orb (len =? 0) (lo <? 0)) + then zeros len + else + if sumbool_of_bool (lo + len - 1 >=? m) + then if sumbool_of_bool (lo <? m) + then zero_extend (subrange_vec_dec v (m - 1) lo) len + else zeros len + else autocast (subrange_vec_dec v (lo + len - 1) lo). + +(* +Lemma slice_is_ok m (v : mword m) lo len + (H1 : 0 <= lo) (H2 : 0 < len) (H3: lo + len < m) : + slice v lo len = autocast (subrange_vec_dec v (lo + len - 1) lo). +unfold slice. +destruct (sumbool_of_bool _). +* exfalso. + unbool_comparisons. + omega. +* destruct (sumbool_of_bool _). + + exfalso. + unbool_comparisons. + omega. + + f_equal. + f_equal. +*) + Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt. Definition print_bits {a} (s : string) (bs : mword a) : unit := tt. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 17d79830..fc97fcc6 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -385,6 +385,7 @@ Qed. Inductive bitU := B0 | B1 | BU. Scheme Equality for bitU. +Definition eq_bit := bitU_beq. Instance Decidable_eq_bit : forall (x y : bitU), Decidable (x = y) := Decidable_eq_from_dec bitU_eq_dec. @@ -1351,9 +1352,51 @@ end; (* We may have uncovered more conjunctions *) repeat match goal with H:and _ _ |- _ => destruct H end. +Ltac generalize_embedded_proofs := + repeat match goal with H:context [?X] |- _ => + match type of X with ArithFact _ => + generalize dependent X + end + end; + intros. + +Lemma iff_equal_l {T:Type} {P:Prop} {x:T} : (x = x <-> P) -> P. +tauto. +Qed. +Lemma iff_equal_r {T:Type} {P:Prop} {x:T} : (P <-> x = x) -> P. +tauto. +Qed. + +Lemma iff_known_l {P Q : Prop} : P -> P <-> Q -> Q. +tauto. +Qed. +Lemma iff_known_r {P Q : Prop} : P -> Q <-> P -> Q. +tauto. +Qed. + +Ltac clean_up_props := + repeat match goal with + (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *) + | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H + | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H + | H:context[true = false] |- _ => rewrite truefalse in H + | H:context[false = true] |- _ => rewrite falsetrue in H + | H1:?P <-> False, H2:context[?Q] |- _ => constr_eq P Q; rewrite -> H1 in H2 + | H1:False <-> ?P, H2:context[?Q] |- _ => constr_eq P Q; rewrite <- H1 in H2 + | H1:?P, H2:?Q <-> ?R |- _ => constr_eq P Q; apply (iff_known_l H1) in H2 + | H1:?P, H2:?R <-> ?Q |- _ => constr_eq P Q; apply (iff_known_r H1) in H2 + | H:context[_ \/ False] |- _ => rewrite or_False_r in H + | H:context[False \/ _] |- _ => rewrite or_False_l in H + (* omega doesn't cope well with extra "True"s in the goal. + Check that they actually appear because setoid_rewrite can fill in evars. *) + | |- context[True /\ _] => setoid_rewrite True_left + | |- context[_ /\ True] => setoid_rewrite True_right + end; + remove_unnecessary_casesplit. Ltac prepare_for_solver := (*dump_context;*) + generalize_embedded_proofs; clear_irrelevant_defns; clear_non_Z_bool_defns; autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *) @@ -1372,10 +1415,8 @@ Ltac prepare_for_solver := filter_disjunctions; Z_if_to_or; clear_irrelevant_bindings; - (* omega doesn't cope well with extra "True"s in the goal. - Check that they actually appear because setoid_rewrite can fill in evars. *) - repeat match goal with |- context[True /\ _] => setoid_rewrite True_left end; - repeat match goal with |- context[_ /\ True] => setoid_rewrite True_right end. + subst; + clean_up_props. Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x). constructor. @@ -1595,6 +1636,8 @@ Lemma Z_compare_eq_gt : Eq = Gt -> False. congruence. Qed. Lemma Z_compare_gt_lt : Gt = Lt -> False. congruence. Qed. Lemma Z_compare_gt_eq : Gt = Eq -> False. congruence. Qed. Ltac z_comparisons := + (* Don't try terms with variables - reduction may be expensive *) + match goal with |- context[?x] => is_var x; fail 1 | |- _ => idtac end; solve [ exact eq_refl | exact Z_compare_lt_eq @@ -1605,14 +1648,48 @@ Ltac z_comparisons := | exact Z_compare_gt_eq ]. +(* Try to get the linear arithmetic solver to do booleans. *) + +Lemma b2z_true x : x = true <-> Z.b2z x = 1. +destruct x; compute; split; congruence. +Qed. + +Lemma b2z_false x : x = false <-> Z.b2z x = 0. +destruct x; compute; split; congruence. +Qed. + +Lemma b2z_tf x : 0 <= Z.b2z x <= 1. +destruct x; simpl; omega. +Qed. + +Ltac solve_bool_with_Z := + subst; + rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *; + (* I did try phrasing these as rewrites, but Coq was oddly reluctant to use them *) + repeat match goal with + | H:?x = ?x <-> _ |- _ => apply iff_equal_l in H + | H:_ <-> ?x = ?x |- _ => apply iff_equal_r in H + end; + repeat match goal with + | H:context [?v = true] |- _ => is_var v; rewrite (b2z_true v) in * + | |- context [?v = true] => is_var v; rewrite (b2z_true v) in * + | H:context [?v = false] |- _ => is_var v; rewrite (b2z_false v) in * + | |- context [?v = false] => is_var v; rewrite (b2z_false v) in * + end; + repeat match goal with + | _:context [Z.b2z ?v] |- _ => generalize (b2z_tf v); generalize dependent (Z.b2z v) + | |- context [Z.b2z ?v] => generalize (b2z_tf v); generalize dependent (Z.b2z v) + end; + intros; + lia. + (* Redefine this to add extra solver tactics *) Ltac sail_extra_tactic := fail. Ltac main_solver := solve - [ match goal with |- (?x ?y) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) y) end - | apply ArithFact_mword; assumption + [ apply ArithFact_mword; assumption | z_comparisons | omega with Z (* Try sail hints before dropping the existential *) @@ -1639,6 +1716,7 @@ Ltac main_solver := | _:(@eq Z ?x _) \/ (@eq Z ?x _) \/ _, _:@eq Z ?y (ZEuclid.div ?x _) |- context[?y] => is_var x; aux y end (* Booleans - and_boolMP *) + | solve_bool_with_Z | simple_ex_iff | ex_iff_solve | drop_bool_exists; solve [eauto using iff_refl, or_iff_cong, and_iff_cong | intuition] @@ -1691,11 +1769,21 @@ Ltac simple_omega := H := projT1 _ |- _ => clearbody H end; omega. +Ltac solve_unknown := + match goal with |- (ArithFact (?x ?y)) => + is_evar x; + idtac "Warning: unknown constraint"; + let t := type of y in + unify x (fun (_ : t) => True); + exact (Build_ArithFact _ I) + end. + Ltac solve_arithfact := (* Attempt a simple proof first to avoid lengthy preparation steps (especially as the large proof terms can upset subsequent proofs). *) intros; (* To solve implications for derive_m *) -try (exact trivial_range); +try solve_unknown; +match goal with |- ArithFact (?x <= ?x <= ?x) => try (exact trivial_range) | _ => idtac end; try fill_in_evar_eq; try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end; (* Trying reflexivity will fill in more complex metavariable examples than @@ -2224,6 +2312,18 @@ simpl. auto with zarith. Qed. +Definition vec_concat {T m n} (v : vec T m) (w : vec T n) : vec T (m + n). +refine (existT _ (projT1 v ++ projT1 w) _). +destruct v. +destruct w. +simpl. +unfold length_list in *. +rewrite <- e, <- e0. +rewrite app_length. +rewrite Nat2Z.inj_add. +reflexivity. +Defined. + Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat. revert l. induction n. diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index 5e20fc71..53ee1ef8 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -133,6 +133,13 @@ function place_slice_signed(m,xs,i,l,shift) = { sail_shiftleft(sext_slice(m, xs, i, l), shift) } +val place_subrange_signed : forall 'n 'm, 'n >= 0 & 'm >= 0. + (implicit('m), bits('n), int, int, int) -> bits('m) effect pure + +function place_subrange_signed(m,xs,i,j,shift) = { + place_slice_signed(m, xs, i, i-j+1, shift) +} + /* This has different names in the aarch64 prelude (UInt) and the other preludes (unsigned). To avoid variable name clashes, we redeclare it here with a suitably awkward name. */ @@ -183,4 +190,16 @@ function zext_ones(n, m) = { sail_shiftright(v, n - m) } + +val vector_update_subrange_from_subrange : forall 'n1 's1 'e1 'n2 's2 'e2, + 0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 < 'n2 & 's1 - 'e1 == 's2 - 'e2. + (implicit('n1), bits('n1), int('s1), int('e1), bits('n2), int('s2), int('e2)) -> bits('n1) + +function vector_update_subrange_from_subrange(n,v1,s1,e1,v2,s2,e2) = { + let xs = sail_shiftright(v2 & slice_mask(e2,s2-e2+1), e2) in + let xs = sail_shiftleft(extzv(n, xs), e1) in + let ys = v1 & not_vec(slice_mask(e1,s1-e1+1)) in + xs | ys +} + $endif diff --git a/lib/reverse_endianness.sail b/lib/reverse_endianness.sail new file mode 100644 index 00000000..ff75f6c3 --- /dev/null +++ b/lib/reverse_endianness.sail @@ -0,0 +1,32 @@ +$ifndef _REVERSE_ENDIANNESS +$define _REVERSE_ENDIANNESS + +$ifdef _DEFAULT_DEC + +$include <vector_dec.sail> + +/* reverse_endianness function set up to ensure it generates good SMT +definitions. The concat/extract pattern may be less efficient in other +backends where these are not primitive operations. */ + +val reverse_endianness : forall 'n, 'n in {8, 16, 32, 64, 128}. bits('n) -> bits('n) + +function reverse_endianness(xs) = { + let len = length(xs); + if len == 8 then { + xs + } else if len == 16 then { + xs[7 .. 0] @ xs[15 .. 8] + } else if len == 32 then { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] + } else if len == 64 then { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56] + } else { + xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56] + @ xs[71 .. 64] @ xs[79 .. 72] @ xs[87 .. 80] @ xs[95 .. 88] @ xs[103 .. 96] @ xs[111 .. 104] @ xs[119 .. 112] @ xs[127 .. 120] + } +} + +$endif + +$endif @@ -767,6 +767,16 @@ void length_lbits(sail_int *rop, const lbits op) mpz_set_ui(*rop, op.len); } +void count_leading_zeros(sail_int *rop, const lbits op) +{ + if (mpz_cmp_ui(*op.bits, 0) == 0) { + mpz_set_ui(*rop, op.len); + } else { + size_t bits = mpz_sizeinbase(*op.bits, 2); + mpz_set_ui(*rop, op.len - bits); + } +} + bool eq_bits(const lbits op1, const lbits op2) { assert(op1.len == op2.len); @@ -1091,6 +1101,20 @@ void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2) } } +void arith_shiftr(lbits *rop, const lbits op1, const sail_int op2) +{ + rop->len = op1.len; + mp_bitcnt_t shift_amt = mpz_get_ui(op2); + mp_bitcnt_t sign_bit = op1.len - 1; + mpz_fdiv_q_2exp(*rop->bits, *op1.bits, shift_amt); + if(mpz_tstbit(*op1.bits, sign_bit) != 0) { + /* */ + for(; shift_amt > 0; shift_amt--) { + mpz_setbit(*rop->bits, sign_bit - shift_amt + 1); + } + } +} + void shiftl(lbits *rop, const lbits op1, const sail_int op2) { rop->len = op1.len; @@ -262,6 +262,7 @@ fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m); fbits fast_sign_extend2(const sbits op, const uint64_t m); void length_lbits(sail_int *rop, const lbits op); +void count_leading_zeros(sail_int *rop, const lbits op); bool eq_bits(const lbits op1, const lbits op2); bool EQUAL(lbits)(const lbits op1, const lbits op2); @@ -330,6 +331,7 @@ void shift_bits_right_arith(lbits *rop, const lbits op1, const lbits op2); void shiftl(lbits *rop, const lbits op1, const sail_int op2); void shiftr(lbits *rop, const lbits op1, const sail_int op2); +void arith_shiftr(lbits *rop, const lbits op1, const sail_int op2); void reverse_endianness(lbits*, lbits); diff --git a/lib/string.sail b/lib/string.sail index 87e4da57..120600ca 100644 --- a/lib/string.sail +++ b/lib/string.sail @@ -9,7 +9,7 @@ overload operator == = {eq_string} infixl 9 ^-^ -val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string +val concat_str = {coq: "String.append", lem: "stringAppend", _: "concat_str"} : (string, string) -> string val "dec_str" : int -> string diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 965b236e..959044a1 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -37,6 +37,15 @@ val vector_length = { overload length = {bitvector_length, vector_length} +val count_leading_zeros = "count_leading_zeros" : forall 'N , 'N >= 1. bits('N) -> {'n, 0 <= 'n <= 'N . atom('n)} +/* +function count_leading_zeros x = { + foreach (i from ('N - 1) to 0 by 1 in dec) + if [x[i]] == 0b1 then return 'N - i - 1; + return 'N; +} +*/ + val "print_bits" : forall 'n. (string, bits('n)) -> unit val "prerr_bits" : forall 'n. (string, bits('n)) -> unit |