From c764daadc0e7138173ddb0895298dae846a7d8b6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 5 Jun 2019 15:45:32 +0100 Subject: Coq: generalize proof terms before main solver Ensures that dependencies in proofs don't affect rewriting. --- lib/coq/Sail2_values.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 17d79830..be9a214b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1351,9 +1351,17 @@ 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. 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 *) -- cgit v1.2.3 From a71a3672443495a34b90790ce7f0f135cfdf601f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 5 Jun 2019 17:10:54 +0100 Subject: Coq: exploit arithmetic solver for some mixed integer/bool problems. --- lib/coq/Sail2_values.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index be9a214b..03df40d2 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1613,6 +1613,36 @@ 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 : Z.b2z x = 0 \/ Z.b2z x = 1. +destruct x; auto. +Qed. + +Ltac solve_bool_with_Z := + subst; + rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *; + 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; + omega. + (* Redefine this to add extra solver tactics *) Ltac sail_extra_tactic := fail. @@ -1647,6 +1677,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] -- cgit v1.2.3 From 1ad5bb9ea7b4462c0ec07b0f6021f6f228834eb5 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 6 Jun 2019 15:31:00 +0100 Subject: Add arith_shiftr to C and OCaml libraries --- lib/sail.c | 14 ++++++++++++++ lib/sail.h | 1 + 2 files changed, 15 insertions(+) (limited to 'lib') diff --git a/lib/sail.c b/lib/sail.c index 5530b462..e9c6ca37 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -1091,6 +1091,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; diff --git a/lib/sail.h b/lib/sail.h index b50a5a4c..1a123cf4 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -330,6 +330,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); -- cgit v1.2.3 From 110bef3571a77fd8f1059827ea0bb29935ed785d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 6 Jun 2019 16:27:06 +0100 Subject: Fix tdiv_int and tmod_int bindings for Lem Also rename them for uniformity with other backends. --- lib/arith.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/arith.sail b/lib/arith.sail index d04c7988..63c3168c 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 -- cgit v1.2.3 From d9862ba2019df1d197bcba3ce85f7fa3ba8576b0 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 6 Jun 2019 17:05:41 +0100 Subject: Coq: tweak bool to Z to use less memory --- lib/coq/Sail2_values.v | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 03df40d2..b3e7ab9d 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1623,13 +1623,25 @@ Lemma b2z_false x : x = false <-> Z.b2z x = 0. destruct x; compute; split; congruence. Qed. -Lemma b2z_tf x : Z.b2z x = 0 \/ Z.b2z x = 1. -destruct x; auto. +Lemma b2z_tf x : 0 <= Z.b2z x <= 1. +destruct x; simpl; omega. +Qed. + +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. 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 * @@ -1641,7 +1653,7 @@ Ltac solve_bool_with_Z := | |- context [Z.b2z ?v] => generalize (b2z_tf v); generalize dependent (Z.b2z v) end; intros; - omega. + lia. (* Redefine this to add extra solver tactics *) -- cgit v1.2.3 From ac95efaf75a17481e9a1c3936f97ebab2c86b8e1 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 6 Jun 2019 18:03:25 +0100 Subject: Coq: more aggressive rewriting before solving Solves some ARM model constraints much more quickly --- lib/coq/Sail2_values.v | 47 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 36 insertions(+), 11 deletions(-) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index b3e7ab9d..94f93736 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1359,6 +1359,40 @@ Ltac generalize_embedded_proofs := 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; @@ -1380,10 +1414,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. @@ -1627,13 +1659,6 @@ Lemma b2z_tf x : 0 <= Z.b2z x <= 1. destruct x; simpl; omega. Qed. -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. - Ltac solve_bool_with_Z := subst; rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *; -- cgit v1.2.3 From 9a367b2bfed76b0f2ac6db26ea0408227ad93230 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 11 Jun 2019 11:11:12 +0100 Subject: Coq: add concatenation operator for polymorphic vectors --- lib/coq/Sail2_values.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 94f93736..bd22371a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -2300,6 +2300,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. -- cgit v1.2.3 From 4b83ad134a472159f730a015187f036104ff35fd Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 12 Jun 2019 17:48:05 +0100 Subject: Fix Lem binding for abs_int --- lib/arith.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/arith.sail b/lib/arith.sail index 63c3168c..7c002e1c 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -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 -- cgit v1.2.3 From 54a08099f2360372a1e94f9ed0489a1dc89351af Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 13 Jun 2019 18:01:24 +0100 Subject: Coq: add eq_bit built-in --- lib/coq/Sail2_values.v | 1 + 1 file changed, 1 insertion(+) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index bd22371a..e152fb67 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. -- cgit v1.2.3 From 2dd28164e40241a2117142fbb197c967740f196d Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 17 Jun 2019 14:25:01 +0100 Subject: Implement a count_leading_zeros builtin for ocaml and c. This may be a slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends. --- lib/sail.c | 10 ++++++++++ lib/sail.h | 1 + lib/vector_dec.sail | 2 ++ 3 files changed, 13 insertions(+) (limited to 'lib') diff --git a/lib/sail.c b/lib/sail.c index e9c6ca37..7fc45714 100644 --- a/lib/sail.c +++ b/lib/sail.c @@ -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); diff --git a/lib/sail.h b/lib/sail.h index 1a123cf4..eddf6e41 100644 --- a/lib/sail.h +++ b/lib/sail.h @@ -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); diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index de63c1a1..909f3898 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -37,6 +37,8 @@ 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)} + val "print_bits" : forall 'n. (string, bits('n)) -> unit val "prerr_bits" : forall 'n. (string, bits('n)) -> unit -- cgit v1.2.3 From 7f4a1bd529fc120ad86a28d05571903805d92c9e Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 17 Jun 2019 14:35:03 +0100 Subject: Add sail implementation of count_leading_zeros. We could use this for backends where the builtin isn't supported but sail support for this is currently a bit broken (will use sail version when it shouldn't e.g. for smt). --- lib/vector_dec.sail | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'lib') diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 909f3898..dce6fb8a 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -38,6 +38,13 @@ 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 -- cgit v1.2.3 From 061c7da3c0629d5fc6cc4a9a91bf4b251b61863d Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 18 Jun 2019 16:57:44 +0100 Subject: Monomorphisation improvements for aarch64_small - additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!) --- lib/mono_rewrites.sail | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'lib') 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 -- cgit v1.2.3 From 1c0c0df14031ba707bd8eb4cbb71c15180de4367 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 20 Jun 2019 18:06:15 +0100 Subject: Coq: avoid some unnecessary reduction in the constraint solver --- lib/coq/Sail2_values.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e152fb67..1bec7c3b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1636,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 @@ -1772,7 +1774,7 @@ 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); +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 -- cgit v1.2.3 From c90c1309a21886f8772c0c65184d0593bbc482c4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 21 Jun 2019 16:46:18 +0100 Subject: Coq: better handling of unknown constraints Move the tactic forward so that preprocessing can't try silly things, simpl to get rid of embedded proofs. --- lib/coq/Sail2_values.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 1bec7c3b..243fb3d6 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1689,8 +1689,7 @@ 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 *) @@ -1774,6 +1773,7 @@ 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 match goal with |- (ArithFact (?x ?y)) => is_evar x; idtac "Warning: unknown constraint"; simpl; exact (Build_ArithFact _ (I : (fun _ => True) y)) end; 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; -- cgit v1.2.3 From f493e3f3d43b9e410b21bf9cecb04f968dff9a20 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 21 Jun 2019 18:10:39 +0100 Subject: Coq: even more robust handling of unknown goals --- lib/coq/Sail2_values.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 243fb3d6..fc97fcc6 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1769,11 +1769,20 @@ 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 match goal with |- (ArithFact (?x ?y)) => is_evar x; idtac "Warning: unknown constraint"; simpl; exact (Build_ArithFact _ (I : (fun _ => True) y)) end; +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; -- cgit v1.2.3 From a97acdb92bce7c13e9731254bc9dc66671d6f806 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 27 Jun 2019 14:29:43 +0100 Subject: Coq: less constrained version of slice for ARM model --- lib/coq/Sail2_operators_mwords.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'lib') 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 =? m) + then if sumbool_of_bool (lo + +/* 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 -- cgit v1.2.3 From 1504c287da8186c2c5c0df65f460aeaa152cf986 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 4 Jul 2019 15:32:27 +0100 Subject: Add coq builtin for concat_str (copied from mips prelude). --- lib/string.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') 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 -- cgit v1.2.3