summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mips_new_tc/Makefile22
-rw-r--r--mips_new_tc/mips_extras.lem94
-rw-r--r--mips_new_tc/mips_extras_embed.lem47
-rw-r--r--mips_new_tc/mips_extras_embed_sequential.lem51
-rw-r--r--mips_new_tc/mips_prelude.sail23
-rw-r--r--mips_new_tc/mips_tlb_stub.sail8
-rw-r--r--mips_new_tc/mips_wrappers.sail5
-rw-r--r--mips_new_tc/prelude.sail5
-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
14 files changed, 187 insertions, 150 deletions
diff --git a/mips_new_tc/Makefile b/mips_new_tc/Makefile
index 3bef7551..d9ccba6b 100644
--- a/mips_new_tc/Makefile
+++ b/mips_new_tc/Makefile
@@ -6,10 +6,26 @@ MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
SAIL:=$(SAIL_DIR)/sail
-MIPS_SAILS:=$(SAIL_LIB_DIR)/flow.sail $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+MIPS_PRE:=$(SAIL_LIB_DIR)/flow.sail $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail
+MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail
+MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
+MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_MAIN:=$(MIPS_SAIL_DIR)/main.sail
-mips: $(MIPS_SAILS)
- $(SAIL) -ocaml -o mips $(MIPS_SAILS)
+mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN)
+ $(SAIL) -ocaml -o mips $^
+
+mips_no_tlb.lem: $(MIPS_PRE) $(MIPS_TLB_STUB) $(MIPS_SAILS)
+ $(SAIL) -lem -o mips_no_tlb -lem_mwords -lem_lib Mips_extras -undefined_gen $^
+mips_no_tlb_types.lem: mips_no_tlb.lem
+
+# TODO: Use monomorphisation so that we can switch to machine words
+mips.lem: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
+ $(SAIL) -lem -o mips -lem_lib Mips_extras -undefined_gen $^
+mips_types.lem: mips.lem
+
+M%.thy: m%.lem m%_types.lem mips_extras.lem
+ lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
clean:
rm -rf _sbuild
diff --git a/mips_new_tc/mips_extras.lem b/mips_new_tc/mips_extras.lem
new file mode 100644
index 00000000..920277f6
--- /dev/null
+++ b/mips_new_tc/mips_extras.lem
@@ -0,0 +1,94 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators
+open import Prompt_monad
+open import Prompt
+
+val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
+val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
+val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
+val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
+
+let MEMr addr size = read_mem Read_plain addr size
+let MEMr_reserve addr size = read_mem Read_reserve addr size
+
+let MEMr_tag addr size =
+ read_mem Read_plain addr size >>= fun v ->
+ read_tag addr >>= fun t ->
+ return (bool_of_bitU t, v)
+
+let MEMr_tag_reserve addr size =
+ read_mem Read_plain addr size >>= fun v ->
+ read_tag addr >>= fun t ->
+ return (bool_of_bitU t, v)
+
+
+val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
+
+let MEMea addr size = write_mem_ea Write_plain addr size
+let MEMea_conditional addr size = write_mem_ea Write_conditional addr size
+
+let MEMea_tag addr size = write_mem_ea Write_plain addr size
+let MEMea_tag_conditional addr size = write_mem_ea Write_conditional addr size
+
+
+val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e
+val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e
+val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e
+val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e
+
+let MEMval _ size v = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional _ size v = write_mem_val v >>= fun b -> return (if b then true else false)
+let MEMval_tag _ size t v = write_mem_val v >>= fun _ -> write_tag_val (bitU_of_bool t) >>= fun _ -> return ()
+let MEMval_tag_conditional _ size t v = write_mem_val v >>= fun b -> write_tag_val (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
+
+val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e
+
+let MEM_sync () = barrier Barrier_MIPS_SYNC
+
+(* Some wrappers copied from aarch64_extras *)
+(* TODO: Harmonise into a common library *)
+
+let get_slice_int_bl len n lo =
+ (* TODO: Is this the intended behaviour? *)
+ let hi = lo + len - 1 in
+ let bits = bits_of_int (hi + 1) n in
+ get_bits false bits hi lo
+
+val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+
+let write_ram _ size _ addr data =
+ MEMea addr size >>
+ MEMval addr size data
+
+let read_ram _ size _ addr = MEMr addr size
+
+let sign_extend bits len = exts_bv len bits
+let zero_extend bits len = extz_bv len bits
+
+let shift_bits_left v n = shiftl_bv v (unsigned n)
+let shift_bits_right v n = shiftr_bv v (unsigned n)
+let shift_bits_right_arith v n = arith_shiftr_bv v (unsigned n)
+
+(* TODO: These could be monadic instead of hardcoded *)
+let internal_pick vs = head vs
+let undefined_string () = ""
+let undefined_unit () = ()
+let undefined_int () = (0:ii)
+let undefined_bool () = false
+val undefined_vector : forall 'a. integer -> 'a -> list 'a
+let undefined_vector len u = repeat [u] len
+val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a
+let undefined_bitvector len = of_bits (repeat [B0] len)
+let undefined_bits len = undefined_bitvector len
+let undefined_bit () = B0
+let undefined_real () = realFromFrac 0 1
+let undefined_range i j = i
+let undefined_atom i = i
+let undefined_nat () = (0:ii)
diff --git a/mips_new_tc/mips_extras_embed.lem b/mips_new_tc/mips_extras_embed.lem
deleted file mode 100644
index bda70274..00000000
--- a/mips_new_tc/mips_extras_embed.lem
+++ /dev/null
@@ -1,47 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_impl_base
-open import Sail_values
-open import Prompt
-
-val MEMr : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
-val MEMr_reserve : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
-val MEMr_tag : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
-val MEMr_tag_reserve : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
-
-let MEMr (addr,size) = read_mem false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
-
-let MEMr_tag (addr,size) = read_mem false Read_plain addr size
-let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size
-
-
-val MEMea : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
-val MEMea_conditional : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
-val MEMea_tag : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
-val MEMea_tag_conditional : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
-
-let MEMea (addr,size) = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size
-
-let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size
-let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
-
-
-val MEMval : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e
-val MEMval_conditional : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e
-val MEMval_tag : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e
-val MEMval_tag_conditional : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e
-
-let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false)
-
-(* TODO *)
-val TAGw : forall 'e. (vector bitU * vector bitU) -> M unit 'e
-let TAGw (addr, tag) = failwith "TAGw not implemented"
-
-val MEM_sync : forall 'e. unit -> M unit 'e
-
-let MEM_sync () = barrier Barrier_Isync
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem
deleted file mode 100644
index b50052dc..00000000
--- a/mips_new_tc/mips_extras_embed_sequential.lem
+++ /dev/null
@@ -1,51 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_impl_base
-open import Sail_values
-open import Sail_operators_mwords
-open import State
-
-val MEMr : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e
-val MEMr_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e
-val MEMr_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e
-val MEMr_tag_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e
-
-let MEMr (addr,size) = read_mem false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
-
-let MEMr_tag (addr,size) =
- read_mem false Read_plain addr size >>= fun v ->
- read_tag false Read_plain addr >>= fun t ->
- return (bitU_to_bool t, v)
-
-let MEMr_tag_reserve (addr,size) =
- read_mem false Read_plain addr size >>= fun v ->
- read_tag false Read_plain addr >>= fun t ->
- return (bitU_to_bool t, v)
-
-
-val MEMea : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
-val MEMea_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
-val MEMea_tag : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
-val MEMea_tag_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
-
-let MEMea (addr,size) = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size
-
-let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size
-let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
-
-
-val MEMval : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit 'e
-val MEMval_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool 'e
-val MEMval_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit 'e
-val MEMval_tag_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool 'e
-
-let MEMval (_,size,v) = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,size,v) = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag (_,size,t,v) = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return ()
-let MEMval_tag_conditional (_,size,t,v) = write_mem_val v >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false)
-
-val MEM_sync : forall 'regs 'e. unit -> M 'regs unit 'e
-
-let MEM_sync () = barrier Barrier_MIPS_SYNC
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index 24196c29..d2e44092 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -324,14 +324,21 @@ function wGPR (idx, v) = {
if i == 0 then () else GPR[i] = v
}
-val MEMr : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEMr_reserve : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEM_sync : unit -> unit effect { barr }
-
-val MEMea : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMea_conditional : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMval : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv }
-val MEMval_conditional : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv }
+val MEMr = {lem: "MEMr"} : forall 'n.
+ ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
+val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n.
+ ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
+val MEM_sync = {lem: "MEM_sync"} :
+ unit -> unit effect { barr }
+
+val MEMea = {lem: "MEMea"} : forall 'n.
+ ( bits(64) , atom('n)) -> unit effect { eamem }
+val MEMea_conditional = {lem: "MEMea_conditional"} : forall 'n.
+ ( bits(64) , atom('n)) -> unit effect { eamem }
+val MEMval = {lem: "MEMval"} : forall 'n.
+ ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv }
+val MEMval_conditional = {lem: "MEMval_conditional"} : forall 'n.
+ ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv }
/* Extern nops with effects, sometimes useful for faking effect */
val skip_eamem = "skip" : unit -> unit effect {eamem}
diff --git a/mips_new_tc/mips_tlb_stub.sail b/mips_new_tc/mips_tlb_stub.sail
index 04f80c35..f0ffb9dd 100644
--- a/mips_new_tc/mips_tlb_stub.sail
+++ b/mips_new_tc/mips_tlb_stub.sail
@@ -32,9 +32,17 @@
/* SUCH DAMAGE. */
/*========================================================================*/
+$ifndef _MIPS_TLB_STUB
+$define _MIPS_TLB_STUB
+
+val tlbEntryMatch : (bits(2), bits(27), bits(8), TLBEntry) -> bool effect pure
function tlbSearch(VAddr) : bits(64) -> option(TLBIndexT) = None
+val TLBTranslate2 : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
function TLBTranslate (vAddr, accessType) : (bits(64), MemAccessType) -> bits(64) =
vAddr
+val TLBTranslateC : (bits(64), MemAccessType) -> (bits(64), bool) effect pure
function TLBTranslateC (vAddr, accessType) : (bits(64), MemAccessType) -> (bits(64), bool) = (vAddr, false)
+
+$endif
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index 42e3e427..fd0619f4 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -60,7 +60,12 @@ val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64)
function addrWrapper(addr, accessType, width) =
addr
+$ifdef _MIPS_TLB_STUB
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape}
+$else
val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef}
+$endif
+
function TranslatePC (vAddr) = {
incrementCP0Count();
if (vAddr[1..0] != 0b00) then /* bad PC alignment */
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail
index 1fab008b..1add5bf8 100644
--- a/mips_new_tc/prelude.sail
+++ b/mips_new_tc/prelude.sail
@@ -267,7 +267,7 @@ val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
infix 8 ^^
-val operator ^^ : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm)
+val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm)
function operator ^^ (bs, n) = replicate_bits (bs, n)
val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
@@ -351,7 +351,7 @@ val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits
val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
infix 7 *_s
-val operator *_s = "mult_svec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
+val operator *_s = "smult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
infix 7 *_u
val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n)
@@ -374,4 +374,3 @@ overload vector_update_subrange = {vector_update_subrange_dec, vector_update_sub
val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n)
function mask bs = bs['n - 1 .. 0]
-
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-17 00:38:24 +0000