summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/prompt_monad.lem6
-rw-r--r--src/gen_lib/sail_operators.lem14
-rw-r--r--src/gen_lib/sail_operators_bitlists.lem28
-rw-r--r--src/gen_lib/sail_operators_mwords.lem28
-rw-r--r--src/process_file.ml4
-rw-r--r--src/sail_lib.ml2
6 files changed, 44 insertions, 38 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 3c414d6e..0966f911 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -123,6 +123,9 @@ let read_mem rk addr sz =
let k bytes = Done (bits_of_mem_bytes bytes) in
Read_mem rk (bits_of addr) (natFromInteger sz) k
+val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
+let read_tag addr = Read_tag (bits_of addr) return
+
val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
let excl_result () =
let k successful = (return successful) in
@@ -137,6 +140,9 @@ let write_mem_val v = match mem_bytes_of_bits v with
| Nothing -> Fail "write_mem_val"
end
+val write_tag_val : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let write_tag_val b = Write_tagv b return
+
val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
let read_reg reg =
let k v =
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 7d6b156b..9354f9d4 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -54,10 +54,10 @@ let arith_op_bv op sign size l r =
let add_bv = arith_op_bv integerAdd false 1
-let addS_bv = arith_op_bv integerAdd true 1
+let sadd_bv = arith_op_bv integerAdd true 1
let sub_bv = arith_op_bv integerMinus false 1
let mult_bv = arith_op_bv integerMult false 2
-let multS_bv = arith_op_bv integerMult true 2
+let smult_bv = arith_op_bv integerMult true 2
let inline add_mword = Machine_word.plus
let inline sub_mword = Machine_word.minus
@@ -72,10 +72,10 @@ let arith_op_bv_int op sign size l r =
of_int (size * length l) n
let add_bv_int = arith_op_bv_int integerAdd false 1
-let addS_bv_int = arith_op_bv_int integerAdd true 1
+let sadd_bv_int = arith_op_bv_int integerAdd true 1
let sub_bv_int = arith_op_bv_int integerMinus false 1
let mult_bv_int = arith_op_bv_int integerMult false 2
-let multS_bv_int = arith_op_bv_int integerMult true 2
+let smult_bv_int = arith_op_bv_int integerMult true 2
val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
(integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b
@@ -85,10 +85,10 @@ let arith_op_int_bv op sign size l r =
of_int (size * length r) n
let add_int_bv = arith_op_int_bv integerAdd false 1
-let addS_int_bv = arith_op_int_bv integerAdd true 1
+let sadd_int_bv = arith_op_int_bv integerAdd true 1
let sub_int_bv = arith_op_int_bv integerMinus false 1
let mult_int_bv = arith_op_int_bv integerMult false 2
-let multS_int_bv = arith_op_int_bv integerMult true 2
+let smult_int_bv = arith_op_int_bv integerMult true 2
let arith_op_bv_bit op sign (size : integer) l r =
let l' = int_of_bv sign l in
@@ -96,7 +96,7 @@ let arith_op_bv_bit op sign (size : integer) l r =
of_int (size * length l) n
let add_bv_bit = arith_op_bv_bit integerAdd false 1
-let addS_bv_bit = arith_op_bv_bit integerAdd true 1
+let sadd_bv_bit = arith_op_bv_bit integerAdd true 1
let sub_bv_bit = arith_op_bv_bit integerMinus true 1
val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index 5658dc21..a627f560 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -69,43 +69,43 @@ let xor_vec = xor_bv
let not_vec = not_bv
val add_vec : list bitU -> list bitU -> list bitU
-val addS_vec : list bitU -> list bitU -> list bitU
+val sadd_vec : list bitU -> list bitU -> list bitU
val sub_vec : list bitU -> list bitU -> list bitU
val mult_vec : list bitU -> list bitU -> list bitU
-val multS_vec : list bitU -> list bitU -> list bitU
+val smult_vec : list bitU -> list bitU -> list bitU
let add_vec = add_bv
-let addS_vec = addS_bv
+let sadd_vec = sadd_bv
let sub_vec = sub_bv
let mult_vec = mult_bv
-let multS_vec = multS_bv
+let smult_vec = smult_bv
val add_vec_int : list bitU -> integer -> list bitU
-val addS_vec_int : list bitU -> integer -> list bitU
+val sadd_vec_int : list bitU -> integer -> list bitU
val sub_vec_int : list bitU -> integer -> list bitU
val mult_vec_int : list bitU -> integer -> list bitU
-val multS_vec_int : list bitU -> integer -> list bitU
+val smult_vec_int : list bitU -> integer -> list bitU
let add_vec_int = add_bv_int
-let addS_vec_int = addS_bv_int
+let sadd_vec_int = sadd_bv_int
let sub_vec_int = sub_bv_int
let mult_vec_int = mult_bv_int
-let multS_vec_int = multS_bv_int
+let smult_vec_int = smult_bv_int
val add_int_vec : integer -> list bitU -> list bitU
-val addS_int_vec : integer -> list bitU -> list bitU
+val sadd_int_vec : integer -> list bitU -> list bitU
val sub_int_vec : integer -> list bitU -> list bitU
val mult_int_vec : integer -> list bitU -> list bitU
-val multS_int_vec : integer -> list bitU -> list bitU
+val smult_int_vec : integer -> list bitU -> list bitU
let add_int_vec = add_int_bv
-let addS_int_vec = addS_int_bv
+let sadd_int_vec = sadd_int_bv
let sub_int_vec = sub_int_bv
let mult_int_vec = mult_int_bv
-let multS_int_vec = multS_int_bv
+let smult_int_vec = smult_int_bv
val add_vec_bit : list bitU -> bitU -> list bitU
-val addS_vec_bit : list bitU -> bitU -> list bitU
+val sadd_vec_bit : list bitU -> bitU -> list bitU
val sub_vec_bit : list bitU -> bitU -> list bitU
let add_vec_bit = add_bv_bit
-let addS_vec_bit = addS_bv_bit
+let sadd_vec_bit = sadd_bv_bit
let sub_vec_bit = sub_bv_bit
val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU)
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index fcc3153b..7411c0a9 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -69,43 +69,43 @@ let xor_vec = xor_bv
let not_vec = not_bv
val add_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
-val addS_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
+val sadd_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val sub_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
val mult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
-val multS_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
+val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b
let add_vec = add_bv
-let addS_vec = addS_bv
+let sadd_vec = sadd_bv
let sub_vec = sub_bv
let mult_vec = mult_bv
-let multS_vec = multS_bv
+let smult_vec = smult_bv
val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val addS_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
+val sadd_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
-val multS_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+val smult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
let add_vec_int = add_bv_int
-let addS_vec_int = addS_bv_int
+let sadd_vec_int = sadd_bv_int
let sub_vec_int = sub_bv_int
let mult_vec_int = mult_bv_int
-let multS_vec_int = multS_bv_int
+let smult_vec_int = smult_bv_int
val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
-val addS_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
+val sadd_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a
val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
-val multS_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
+val smult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let add_int_vec = add_int_bv
-let addS_int_vec = addS_int_bv
+let sadd_int_vec = sadd_int_bv
let sub_int_vec = sub_int_bv
let mult_int_vec = mult_int_bv
-let multS_int_vec = multS_int_bv
+let smult_int_vec = smult_int_bv
val add_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
-val addS_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
+val sadd_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
val sub_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> mword 'a
let add_vec_bit = add_bv_bit
-let addS_vec_bit = addS_bv_bit
+let sadd_vec_bit = sadd_bv_bit
let sub_vec_bit = sub_bv_bit
val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU)
diff --git a/src/process_file.ml b/src/process_file.ml
index a447061b..ffd61fae 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -252,8 +252,8 @@ let output_lem filename libs defs =
separate hardline [
string ("theory " ^ isa_thy_name);
string " imports";
- string " Sail.Sail_values_extras";
- string " Sail.State_extras";
+ string " Sail.Sail_values_lemmas";
+ string " Sail.State_lemmas";
string (" " ^ String.capitalize filename);
string "begin";
string "";
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 53f4aec6..44dd4ac5 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -282,7 +282,7 @@ let mult_vec (x, y) =
to_bits' (2*len, prod)
(* signed multiplication of two n bit lists producing a list of 2n bits. *)
-let mult_svec (x, y) =
+let smult_vec (x, y) =
let xi = sint(x) in
let yi = sint(y) in
let len = List.length x in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:00:36 +0000