diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Makefile | 2 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 10 | ||||
| -rw-r--r-- | lib/coq/Sail2_string.v | 35 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 36 | ||||
| -rw-r--r-- | lib/hol/.gitignore | 19 | ||||
| -rw-r--r-- | lib/isabelle/.gitignore | 2 | ||||
| -rw-r--r-- | lib/mono_rewrites.sail | 3 |
7 files changed, 89 insertions, 18 deletions
diff --git a/lib/coq/Makefile b/lib/coq/Makefile index 97869e3c..99321aae 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,6 +1,6 @@ BBV_DIR=../../../bbv/theories -SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v +SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index c98e2926..0b3a2cd8 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -115,3 +115,13 @@ let rec untilM vars cond body = write_reg r1 r1_v >> write_reg r2 r2_v*) *) + +(* If we need to build an existential after a monadic operation, assume that + we can do it entirely from the type. *) + +Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall x, ArithFact (P x)} : monad rv {x : T & ArithFact (P x)} e := + x >>= fun y => returnm (existT _ y (H y)). + +Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e := + x >>= fun y => returnm (projT1 y). + diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v new file mode 100644 index 00000000..9ca9cb67 --- /dev/null +++ b/lib/coq/Sail2_string.v @@ -0,0 +1,35 @@ +Require Import Sail2_values. + +Definition string_sub (s : string) (start : Z) (len : Z) : string := + String.substring (Z.to_nat start) (Z.to_nat len) s. + +Definition string_startswith s expected := + let prefix := String.substring 0 (String.length expected) s in + generic_eq prefix expected. + +Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) := + let n := Z.to_nat (projT1 n) in + String.substring n (String.length s - n) s. + +Definition string_length s : {n : Z & ArithFact (n >= 0)} := + build_ex (Z.of_nat (String.length s)). + +Definition string_append := String.append. + +(* TODO: maybe_int_of_prefix, maybe_int_of_string *) + +Fixpoint n_leading_spaces (s:string) : nat := + match s with + | EmptyString => 0 + | String " " t => S (n_leading_spaces t) + | _ => 0 + end. + +Definition opt_spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) := + Some (tt, build_ex (Z.of_nat (n_leading_spaces s))). + +Definition spc_matches_prefix s : option (unit * {n : Z & ArithFact (n >= 0)}) := + match n_leading_spaces s with + | O => None + | S n => Some (tt, build_ex (Z.of_nat (S n))) + end.
\ No newline at end of file diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 0ce6134f..7766e6af 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -21,7 +21,7 @@ Lemma use_ArithFact {P} `(ArithFact P) : P. apply fact. Defined. -Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} := +Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := existT _ n H. Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. @@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <> Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y)) }. destruct (eqdec x y); simpl; split; congruence. -Qed. +Defined. + +Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := + Decidable_eq_from_dec String.string_dec. (* Project away range constraints in comparisons *) @@ -935,6 +938,11 @@ end. Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end. Ltac clear_non_Z_defns := repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end. +Ltac clear_irrelevant_defns := +repeat match goal with X := _ |- _ => + match goal with |- context[X] => idtac end || + match goal with _ : context[X] |- _ => idtac end || clear X +end. Lemma ArithFact_mword (a : Z) (w : mword a) : ArithFact (a >= 0). constructor. @@ -1002,6 +1010,7 @@ Ltac dump_context := match goal with |- ?X => idtac "Goal:" X end. Ltac prepare_for_solver := (*dump_context;*) + clear_irrelevant_defns; clear_non_Z_defns; extract_properties; repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end; @@ -1014,11 +1023,20 @@ Ltac prepare_for_solver := Ltac solve_arithfact := prepare_for_solver; (*dump_context;*) - solve [apply ArithFact_mword; assumption - | constructor; omega with Z - (* The datatypes hints give us some list handling, esp In *) - | constructor; eauto with datatypes zarith sail - | constructor; idtac "Unable to solve constraint"; dump_context; fail]. + solve + [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end + | match goal with |- ArithFact (?x = ?y) => + (is_evar x || is_evar y); + (* compute to allow projections to remove proofs that might not be allowed in the evar *) + let x := eval cbn in x in + let y := eval cbn in y in + idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end + | apply ArithFact_mword; assumption + | constructor; omega with Z + (* The datatypes hints give us some list handling, esp In *) + | constructor; eauto 3 with datatypes zarith sail + | constructor; idtac "Unable to solve constraint"; dump_context; fail + ]. Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. Hint Unfold length_mword : sail. @@ -1036,6 +1054,10 @@ Qed. Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply ReasonableSize_witness; assumption | constructor; omega]) : typeclass_instances. +Definition to_range (x : Z) : {y : Z & ArithFact (x <= y <= x)} := build_ex x. + + + Instance mword_Bitvector {a : Z} `{ArithFact (a >= 0)} : (Bitvector (mword a)) := { bits_of v := List.map bitU_of_bool (bitlistFromWord (get_word v)); of_bits v := option_map (fun bl => to_word isPositive (fit_bbv_word (wordFromBitlist bl))) (just_list (List.map bool_of_bitU v)); diff --git a/lib/hol/.gitignore b/lib/hol/.gitignore index fe652801..73d33f88 100644 --- a/lib/hol/.gitignore +++ b/lib/hol/.gitignore @@ -1,9 +1,10 @@ -prompt_monadScript.sml -promptScript.sml -sail_instr_kindsScript.sml -sail_operators_bitlistsScript.sml -sail_operators_mwordsScript.sml -sail_operatorsScript.sml -sail_valuesScript.sml -state_monadScript.sml -stateScript.sml +sail2_prompt_monadScript.sml +sail2_promptScript.sml +sail2_instr_kindsScript.sml +sail2_operators_bitlistsScript.sml +sail2_operators_mwordsScript.sml +sail2_operatorsScript.sml +sail2_valuesScript.sml +sail2_state_monadScript.sml +sail2_stateScript.sml +sail2_stringScript.sml diff --git a/lib/isabelle/.gitignore b/lib/isabelle/.gitignore index ed83cdc1..fad6adbd 100644 --- a/lib/isabelle/.gitignore +++ b/lib/isabelle/.gitignore @@ -10,4 +10,6 @@ Sail2_valuesAuxiliary.thy Sail2_values.thy Sail2_stateAuxiliary.thy Sail2_state_monad.thy +Sail2_state_lifting.thy Sail2_state.thy +Sail2_string.thy
\ No newline at end of file diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail index aa8d05cd..9e837e10 100644 --- a/lib/mono_rewrites.sail +++ b/lib/mono_rewrites.sail @@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v) /* This is generated internally to deal with case splits which reveal the size of a bitvector */ -val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure +val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure /* Definitions for the rewrites */ |