diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 6 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 4 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt_monad.v | 7 | ||||
| -rw-r--r-- | lib/coq/Sail2_state.v | 1 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
5 files changed, 15 insertions, 4 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 224ab18d..ebcc0925 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -245,8 +245,10 @@ val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword Definition add_vec {n} : mword n -> mword n -> mword n := word_binop Word.wplus. (*Definition sadd_vec {n} : mword n -> mword n -> mword n := sadd_bv w.*) Definition sub_vec {n} : mword n -> mword n -> mword n := word_binop Word.wminus. -Definition mult_vec {n} : mword n -> mword n -> mword n := word_binop Word.wmult. -(*Definition smult_vec {n} : mword n -> mword n -> mword n := smult_bv w.*) +Definition mult_vec {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m := + word_binop Word.wmult (zero_extend l _) (zero_extend r _). +Definition mults_vec {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m := + word_binop Word.wmult (sign_extend l _) (sign_extend r _). (*val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val sadd_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 802fc302..336ca8de 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -48,7 +48,7 @@ match b with | BU => Fail "bool_of_bitU" end. -(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e +(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e*) Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E := match b with | B0 => returnm false @@ -57,7 +57,7 @@ match b with end. -val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> +(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e let rec whileM vars cond body = cond vars >>= fun cond_val -> diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v index 5bb9d477..2715b5e7 100644 --- a/lib/coq/Sail2_prompt_monad.v +++ b/lib/coq/Sail2_prompt_monad.v @@ -31,6 +31,7 @@ Inductive monad regval a e := | Read_reg : register_name -> (regval -> monad regval a e) -> monad regval a e (* Request to write register *) | Write_reg : register_name -> regval -> monad regval a e -> monad regval a e + | Undefined : (bool -> monad regval a e) -> monad regval a e (*Result : a failed assert with possible error message to report*) | Fail : string -> monad regval a e | Error : string -> monad regval a e @@ -49,6 +50,7 @@ Arguments Footprint [_ _ _]. Arguments Barrier [_ _ _]. Arguments Read_reg [_ _ _]. Arguments Write_reg [_ _ _]. +Arguments Undefined [_ _ _]. Arguments Fail [_ _ _]. Arguments Error [_ _ _]. Arguments Exception [_ _ _]. @@ -65,6 +67,7 @@ Fixpoint bind {rv A B E} (m : monad rv A E) (f : A -> monad rv B E) := match m w | Write_tag a t k => Write_tag a t (fun v => bind (k v) f) | Read_reg descr k => Read_reg descr (fun v => bind (k v) f) | Excl_res k => Excl_res (fun v => bind (k v) f) + | Undefined k => Undefined (fun v => bind (k v) f) | Write_ea wk a sz k => Write_ea wk a sz (bind k f) | Footprint k => Footprint (bind k f) | Barrier bk k => Barrier bk (bind k f) @@ -83,6 +86,9 @@ Notation "m >> n" := (bind0 m n) (at level 50, left associativity). (*val exit : forall rv a e. unit -> monad rv a e*) Definition exit {rv A E} (_ : unit) : monad rv A E := Fail "exit". +(*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*) +Definition undefined_bool {rv e} (_:unit) : monad rv bool e := Undefined returnm. + (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*) Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E := if exp then Done tt else Fail msg. @@ -105,6 +111,7 @@ Fixpoint try_catch {rv A E1 E2} (m : monad rv A E1) (h : E1 -> monad rv A E2) := | Write_tag a t k => Write_tag a t (fun v => try_catch (k v) h) | Read_reg descr k => Read_reg descr (fun v => try_catch (k v) h) | Excl_res k => Excl_res (fun v => try_catch (k v) h) + | Undefined k => Undefined (fun v => try_catch (k v) h) | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h) | Footprint k => Footprint (try_catch k h) | Barrier bk k => Barrier bk (try_catch k h) diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 7e10aba3..1d5cb342 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -15,6 +15,7 @@ let rec liftState ra s = match s with | (Write_tagv t k) -> bindS (write_tagS t) (fun v -> liftState ra (k v)) | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v)) | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v)) + | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v)) | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) | (Footprint k) -> liftState ra k diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 7c70f88b..55d85b3a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1032,6 +1032,7 @@ Arguments write_to [_ _ _]. Arguments of_regval [_ _ _]. Arguments regval_of [_ _ _]. +(* Register accessors: pair of functions for reading and writing register values *) Definition register_accessors regstate regval : Type := ((string -> regstate -> option regval) * (string -> regval -> regstate -> option regstate)). |