diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 25 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 25 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 290 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 179 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 274 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 428 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 27 |
7 files changed, 730 insertions, 518 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 1d8623df..8cef266e 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -30,20 +30,35 @@ end declare {isabelle} termination_argument foreachM = automatic -val bool_of_bitU_undef : forall 'rv 'e. bitU -> monad 'rv bool 'e -let bool_of_bitU_undef = function +val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e +let bool_of_bitU_fail = function + | B0 -> return false + | B1 -> return true + | BU -> Fail "bool_of_bitU" +end + +val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e +let bool_of_bitU_oracle = function | B0 -> return false | B1 -> return true | BU -> undefined_bool () end -val bools_of_bitUs : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e -let bools_of_bitUs bits = +val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e +let bools_of_bits_oracle bits = foreachM bits [] (fun b bools -> - bool_of_bitU_undef b >>= (fun b -> + bool_of_bitU_oracle b >>= (fun b -> return (bools ++ [b]))) +val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e +let of_bits_oracle bits = + bools_of_bits_oracle bits >>= (fun bs -> + return (of_bools bs)) + +val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e +let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits) + 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 = diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index edbe1f03..92b9ac5e 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -127,11 +127,20 @@ let try_catchR m h = | Right e -> h e end) +val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e +let maybe_fail msg = function + | Just a -> return a + | Nothing -> Fail msg +end + +val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e +let read_mem_bytes rk addr sz = + Read_mem rk (bits_of addr) (nat_of_int sz) return val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e 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 + read_mem_bytes rk addr sz >>= (fun bytes -> + maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e let read_tag addr = Read_tag (bits_of addr) return @@ -142,7 +151,7 @@ let excl_result () = Excl_res k val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e -let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger sz) (Done ()) +let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ()) val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e let write_mem_val v = match mem_bytes_of_bits v with @@ -166,10 +175,10 @@ let read_reg reg = (* TODO val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e let read_reg_range reg i j = - read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j)) + read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j)) let read_reg_bit reg i = - read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> + read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v -> return (extract_only_element v) let read_reg_field reg regfield = @@ -188,9 +197,9 @@ let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) let write_reg reg v = write_reg_aux (external_reg_whole reg) v let write_reg_range reg i j v = - write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v + write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v let write_reg_pos reg i v = - let iN = natFromInteger i in + let iN = nat_of_int i in write_reg_aux (external_reg_slice reg (iN,iN)) [v] let write_reg_bit = write_reg_pos let write_reg_field reg regfield v = @@ -199,7 +208,7 @@ let write_reg_field_bit reg regfield bit = write_reg_aux (external_reg_field_whole reg regfield.field_name) (Vector [bit] 0 (is_inc_of_reg reg)) let write_reg_field_range reg regfield i j v = - write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v + write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v let write_reg_field_pos reg regfield i v = write_reg_field_range reg regfield i i [v] let write_reg_field_bit = write_reg_field_pos*) diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 9354f9d4..9b0857d9 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -4,20 +4,21 @@ open import Sail_values (*** Bit vector operations *) -val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c -let concat_bv l r = of_bits (bits_of l ++ bits_of r) +val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU +let concat_bv l r = (bits_of l ++ bits_of r) -val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b -let cons_bv b v = of_bits (b :: bits_of v) +val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU +let cons_bv b v = b :: bits_of v -let bool_of_bv v = extract_only_element (bits_of v) -let cast_unit_bv b = of_bits [b] -let bv_of_bit len b = of_bits (extz_bits len [b]) -let int_of_bv sign = if sign then signed else unsigned +val cast_unit_bv : bitU -> list bitU +let cast_unit_bv b = [b] + +val bv_of_bit : integer -> bitU -> list bitU +let bv_of_bit len b = extz_bits len [b] let most_significant v = match bits_of v with | b :: _ -> b - | _ -> failwith "most_significant applied to empty vector" + | _ -> B0 (* Treat empty bitvector as all zeros *) end let get_max_representable_in sign (n : integer) : integer = @@ -36,135 +37,106 @@ let get_min_representable_in _ (n : integer) : integer = else if n = 5 then min_5 else 0 - (integerPow 2 (natFromInteger n)) -val bitwise_binop_bv : forall 'a. Bitvector 'a => - (bool -> bool -> bool) -> 'a -> 'a -> 'a -let bitwise_binop_bv op l r = of_bits (binop_bits op (bits_of l) (bits_of r)) - -let and_bv = bitwise_binop_bv (&&) -let or_bv = bitwise_binop_bv (||) -let xor_bv = bitwise_binop_bv xor -let not_bv v = of_bits (not_bits (bits_of v)) - -val arith_op_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b -let arith_op_bv op sign size l r = - let (l',r') = (int_of_bv sign l, int_of_bv sign r) in - let n = op l' r' in - of_int (size * length l) n - - -let add_bv = arith_op_bv integerAdd false 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 smult_bv = arith_op_bv integerMult true 2 - -let inline add_mword = Machine_word.plus -let inline sub_mword = Machine_word.minus -val mult_mword : forall 'a 'b. Size 'b => mword 'a -> mword 'a -> mword 'b -let mult_mword l r = times (zeroExtend l) (zeroExtend r) - -val arith_op_bv_int : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b -let arith_op_bv_int op sign size l r = - let l' = int_of_bv sign l in - let n = op l' r in - of_int (size * length l) n - -let add_bv_int = arith_op_bv_int integerAdd false 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 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 -let arith_op_int_bv op sign size l r = - let r' = int_of_bv sign r in - let n = op l r' in - of_int (size * length r) n - -let add_int_bv = arith_op_int_bv integerAdd false 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 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 - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - of_int (size * length l) n - -let add_bv_bit = arith_op_bv_bit integerAdd false 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 => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU) +val arith_op_bv_int : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a +let arith_op_bv_int op sign l r = + let r' = of_int (length l) r in + arith_op_bv op sign l r' + +val arith_op_int_bv : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a +let arith_op_int_bv op sign l r = + let l' = of_int (length r) l in + arith_op_bv op sign l' r + +let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0) +let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r) + +(* TODO (or just omit and define it per spec if needed) +val arith_op_overflow_bv : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU) let arith_op_overflow_bv op sign size l r = let len = length l in let act_size = len * size in - let (l_sign,r_sign) = (int_of_bv sign l,int_of_bv sign r) in - let (l_unsign,r_unsign) = (int_of_bv false l,int_of_bv false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size = of_int act_size n in - let one_more_size_u = bits_of_int (act_size + 1) n_unsign in - let overflow = - if n <= get_max_representable_in sign len && - n >= get_min_representable_in sign len - then B0 else B1 in - let c_out = most_significant one_more_size_u in - (correct_size,overflow,c_out) + match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with + | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) -> + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size = of_int act_size n in + let one_more_size_u = bits_of_int (act_size + 1) n_unsign in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size,overflow,c_out) + | (_, _, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv = arith_op_overflow_bv integerAdd false 1 -let add_overflow_bv_signed = arith_op_overflow_bv integerAdd true 1 +let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1 let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1 -let sub_overflow_bv_signed = arith_op_overflow_bv integerMinus true 1 +let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1 let mult_overflow_bv = arith_op_overflow_bv integerMult false 2 -let mult_overflow_bv_signed = arith_op_overflow_bv integerMult true 2 +let mults_overflow_bv = arith_op_overflow_bv integerMult true 2 -val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU) +val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU) let arith_op_overflow_bv_bit op sign size l r_bit = let act_size = length l * size in - let l' = int_of_bv sign l in - let l_u = int_of_bv false l in - let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) - | BU -> failwith "arith_op_overflow_bv_bit applied to undefined bit" - end in - let correct_size = of_int act_size n in - let one_larger = bits_of_int (act_size + 1) nu in - let overflow = - if changed - then - if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B0 in - (correct_size,overflow,most_significant one_larger) + match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with + | (Just l', Just l_u, false) -> + let (n, nu, changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l', l_u, false) + | BU -> (* unreachable due to check above *) + failwith "arith_op_overflow_bv_bit applied to undefined bit" + end in + let correct_size = of_int act_size n in + let one_larger = bits_of_int (act_size + 1) nu in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size, overflow, most_significant one_larger) + | (_, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1 -let add_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerAdd true 1 +let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1 let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1 -let sub_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerMinus true 1 +let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*) type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot -val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a +let invert_shift = function + | LL_shift -> RR_shift + | RR_shift -> LL_shift + | RR_shift_arith -> LL_shift + | LL_rot -> RR_rot + | RR_rot -> LL_rot +end + +val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU let shift_op_bv op v n = + let v = bits_of v in + if n = 0 then v else + let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in match op with | LL_shift -> - of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n) + subrange_list true v n (length v - 1) ++ repeat [B0] n | RR_shift -> - of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1)) + repeat [B0] n ++ subrange_list true v 0 (length v - n - 1) | RR_shift_arith -> - of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1)) + repeat [most_significant v] n ++ subrange_list true v 0 (length v - n - 1) | LL_rot -> - of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1)) + subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1) | RR_rot -> - of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1)) + subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1) end let shiftl_bv = shift_op_bv LL_shift (*"<<"*) @@ -173,10 +145,11 @@ let arith_shiftr_bv = shift_op_bv RR_shift_arith let rotl_bv = shift_op_bv LL_rot (*"<<<"*) let rotr_bv = shift_op_bv LL_rot (*">>>"*) -let shiftl_mword w n = Machine_word.shiftLeft w (natFromInteger n) -let shiftr_mword w n = Machine_word.shiftRight w (natFromInteger n) -let rotl_mword w n = Machine_word.rotateLeft (natFromInteger n) w -let rotr_mword w n = Machine_word.rotateRight (natFromInteger n) w +let shiftl_mword w n = Machine_word.shiftLeft w (nat_of_int n) +let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n) +let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n) +let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w +let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 @@ -184,27 +157,19 @@ let rec arith_op_no0 (op : integer -> integer -> integer) l r = else Just (op l r) val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b let arith_op_bv_no0 op sign size l r = - let act_size = length l * size in - let (l',r') = (int_of_bv sign l,int_of_bv sign r) in - let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> - (n' <= get_max_representable_in sign act_size && - n' >= get_min_representable_in sign act_size, n') - | _ -> (false,0) - end in - if representable then (of_int act_size n') else (of_bits (repeat [BU] act_size)) + Maybe.bind (int_of_bv sign l) (fun l' -> + Maybe.bind (int_of_bv sign r) (fun r' -> + if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r')))) let mod_bv = arith_op_bv_no0 hardware_mod false 1 let quot_bv = arith_op_bv_no0 hardware_quot false 1 -let quot_bv_signed = arith_op_bv_no0 hardware_quot true 1 +let quots_bv = arith_op_bv_no0 hardware_quot true 1 let mod_mword = Machine_word.modulo let quot_mword = Machine_word.unsignedDivide -let quot_mword_signed = Machine_word.signedDivide +let quots_mword = Machine_word.signedDivide let arith_op_bv_int_no0 op sign size l r = arith_op_bv_no0 op sign size l (of_int (length l) r) @@ -212,26 +177,49 @@ let arith_op_bv_int_no0 op sign size l r = let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1 let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1 -let replicate_bits_bv v count = of_bits (repeat (bits_of v) count) +let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r) +let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r) +let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r) + +let replicate_bits_bv v count = repeat (bits_of v) count let duplicate_bit_bv bit len = replicate_bits_bv [bit] len val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let eq_bv l r = (unsigned l = unsigned r) +let eq_bv l r = (bits_of l = bits_of r) + +let eq_mword l r = (l = r) val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let neq_bv l r = (unsigned l <> unsigned r) - -val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let ucmp_bv cmp l r = cmp (unsigned l) (unsigned r) - -val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let scmp_bv cmp l r = cmp (signed l) (signed r) - -let ult_bv = ucmp_bv (<) -let slt_bv = scmp_bv (<) -let ugt_bv = ucmp_bv (>) -let sgt_bv = scmp_bv (>) -let ulteq_bv = ucmp_bv (<=) -let slteq_bv = scmp_bv (<=) -let ugteq_bv = ucmp_bv (>=) -let sgteq_bv = scmp_bv (>=) +let neq_bv l r = not (eq_bv l r) + +let neq_mword l r = (l <> r) + +val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) +let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) +let ugt_bv l r = not (ulteq_bv l r) +let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) + +val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let slt_bv l r = + match (most_significant l, most_significant r) with + | (B0, B0) -> ult_bv l r + | (B0, B1) -> false + | (B1, B0) -> true + | (B1, B1) -> + let l' = add_one_bit_ignore_overflow (bits_of l) in + let r' = add_one_bit_ignore_overflow (bits_of r) in + ugt_bv l' r' + | (BU, BU) -> ult_bv l r + | (BU, _) -> true + | (_, BU) -> false + end +let slteq_bv l r = (eq_bv l r) || (slt_bv l r) +let sgt_bv l r = not (slteq_bv l r) +let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) + +val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) + +val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index a627f560..9b81e233 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -2,9 +2,27 @@ open import Pervasives_extra open import Machine_word open import Sail_values open import Sail_operators +open import Prompt_monad +open import Prompt (* Specialisation of operators to bit lists *) +val uint_maybe : list bitU -> maybe integer +let uint_maybe v = unsigned v +let uint_fail v = maybe_fail "uint" (unsigned v) +let uint_oracle v = + bools_of_bits_oracle v >>= (fun bs -> + return (int_of_bools false bs)) +let uint v = maybe_failwith (uint_maybe v) + +val sint_maybe : list bitU -> maybe integer +let sint_maybe v = signed v +let sint_fail v = maybe_fail "sint" (signed v) +let sint_oracle v = + bools_of_bits_oracle v >>= (fun bs -> + return (int_of_bools true bs)) +let sint v = maybe_failwith (sint_maybe v) + val access_vec_inc : list bitU -> integer -> bitU let access_vec_inc = access_bv_inc @@ -13,9 +31,15 @@ let access_vec_dec = access_bv_dec val update_vec_inc : list bitU -> integer -> bitU -> list bitU let update_vec_inc = update_bv_inc +let update_vec_inc_maybe v i b = Just (update_vec_inc v i b) +let update_vec_inc_fail v i b = return (update_vec_inc v i b) +let update_vec_inc_oracle v i b = return (update_vec_inc v i b) val update_vec_dec : list bitU -> integer -> bitU -> list bitU let update_vec_dec = update_bv_dec +let update_vec_dec_maybe v i b = Just (update_vec_dec v i b) +let update_vec_dec_fail v i b = return (update_vec_dec v i b) +let update_vec_dec_oracle v i b = return (update_vec_dec v i b) val subrange_vec_inc : list bitU -> integer -> integer -> list bitU let subrange_vec_inc = subrange_bv_inc @@ -40,21 +64,30 @@ let concat_vec = concat_bv val cons_vec : bitU -> list bitU -> list bitU let cons_vec = cons_bv +let cons_vec_maybe b v = Just (cons_vec b v) +let cons_vec_fail b v = return (cons_vec b v) +let cons_vec_oracle b v = return (cons_vec b v) -val bool_of_vec : mword ty1 -> bitU -let bool_of_vec = bool_of_bv - -val cast_unit_vec : bitU -> mword ty1 +val cast_unit_vec : bitU -> list bitU let cast_unit_vec = cast_unit_bv +let cast_unit_vec_maybe b = Just (cast_unit_vec b) +let cast_unit_vec_fail b = return (cast_unit_vec b) +let cast_unit_vec_oracle b = return (cast_unit_vec b) val vec_of_bit : integer -> bitU -> list bitU let vec_of_bit = bv_of_bit +let vec_of_bit_maybe len b = Just (vec_of_bit len b) +let vec_of_bit_fail len b = return (vec_of_bit len b) +let vec_of_bit_oracle len b = return (vec_of_bit len b) val msb : list bitU -> bitU let msb = most_significant -val int_of_vec : bool -> list bitU -> integer -let int_of_vec = int_of_bv +val int_of_vec_maybe : bool -> list bitU -> maybe integer +let int_of_vec_maybe = int_of_bv +let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v) +let int_of_vec_oracle sign v = bools_of_bits_oracle v >>= (fun v -> return (int_of_bools sign v)) +let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v) val string_of_vec : list bitU -> string let string_of_vec = string_of_bv @@ -63,52 +96,75 @@ val and_vec : list bitU -> list bitU -> list bitU val or_vec : list bitU -> list bitU -> list bitU val xor_vec : list bitU -> list bitU -> list bitU val not_vec : list bitU -> list bitU -let and_vec = and_bv -let or_vec = or_bv -let xor_vec = xor_bv -let not_vec = not_bv +let and_vec = binop_list and_bit +let or_vec = binop_list or_bit +let xor_vec = binop_list xor_bit +let not_vec = List.map not_bit + +val arith_op_double_bl : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> 'a -> 'a -> list bitU +let arith_op_double_bl op sign l r = + let len = 2 * length l in + let l' = if sign then exts_bv len l else extz_bv len l in + let r' = if sign then exts_bv len r else extz_bv len r in + arith_op_bv op sign l' r' val add_vec : list bitU -> list bitU -> list bitU -val sadd_vec : list bitU -> list bitU -> list bitU +val adds_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 smult_vec : list bitU -> list bitU -> list bitU -let add_vec = add_bv -let sadd_vec = sadd_bv -let sub_vec = sub_bv -let mult_vec = mult_bv -let smult_vec = smult_bv - -val add_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 smult_vec_int : list bitU -> integer -> list bitU -let add_vec_int = add_bv_int -let sadd_vec_int = sadd_bv_int -let sub_vec_int = sub_bv_int -let mult_vec_int = mult_bv_int -let smult_vec_int = smult_bv_int - -val add_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 smult_int_vec : integer -> list bitU -> list bitU -let add_int_vec = add_int_bv -let sadd_int_vec = sadd_int_bv -let sub_int_vec = sub_int_bv -let mult_int_vec = mult_int_bv -let smult_int_vec = smult_int_bv - -val add_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 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) +val mults_vec : list bitU -> list bitU -> list bitU +let add_vec = arith_op_bv integerAdd false +let adds_vec = arith_op_bv integerAdd true +let sub_vec = arith_op_bv integerMinus false +let mult_vec = arith_op_double_bl integerMult false +let mults_vec = arith_op_double_bl integerMult true + +val add_vec_int : list bitU -> integer -> list bitU +val adds_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 +let add_vec_int l r = arith_op_bv_int integerAdd false l r +let adds_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus false l r +let mult_vec_int l r = arith_op_double_bl integerMult false l (of_int (length l) r) +let mults_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r) + +val add_int_vec : integer -> list bitU -> list bitU +val adds_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 +let add_int_vec l r = arith_op_int_bv integerAdd false l r +let adds_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus false l r +let mult_int_vec l r = arith_op_double_bl integerMult false (of_int (length r) l) r +let mults_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r + +val add_vec_bit : list bitU -> bitU -> list bitU +val adds_vec_bit : list bitU -> bitU -> list bitU +val sub_vec_bit : list bitU -> bitU -> list bitU + +let add_vec_bool l r = arith_op_bv_bool integerAdd false l r +let add_vec_bit_maybe l r = arith_op_bv_bit integerAdd false l r +let add_vec_bit_fail l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r) +let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r) + +let adds_vec_bool l r = arith_op_bv_bool integerAdd true l r +let adds_vec_bit_maybe l r = arith_op_bv_bit integerAdd true l r +let adds_vec_bit_fail l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r) +let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r) + +let sub_vec_bool l r = arith_op_bv_bool integerMinus false l r +let sub_vec_bit_maybe l r = arith_op_bv_bit integerMinus false l r +let sub_vec_bit_fail l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r) +let sub_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r) + +(*val add_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) val add_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) val sub_overflow_vec : list bitU -> list bitU -> (list bitU * bitU * bitU) val sub_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU) @@ -128,7 +184,7 @@ val sub_overflow_vec_bit_signed : list bitU -> bitU -> (list bitU * bitU * bitU let add_overflow_vec_bit = add_overflow_bv_bit let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit -let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) val shiftl : list bitU -> integer -> list bitU val shiftr : list bitU -> integer -> list bitU @@ -141,23 +197,28 @@ let arith_shiftr = arith_shiftr_bv let rotl = rotl_bv let rotr = rotr_bv -val mod_vec : list bitU -> list bitU -> list bitU -val quot_vec : list bitU -> list bitU -> list bitU -val quot_vec_signed : list bitU -> list bitU -> list bitU -let mod_vec = mod_bv -let quot_vec = quot_bv -let quot_vec_signed = quot_bv_signed +val mod_vec : list bitU -> list bitU -> list bitU +val quot_vec : list bitU -> list bitU -> list bitU +val quots_vec : list bitU -> list bitU -> list bitU +let mod_vec l r = fromMaybe (repeat [BU] (length l)) (mod_bv l r) +let quot_vec l r = fromMaybe (repeat [BU] (length l)) (quot_bv l r) +let quots_vec l r = fromMaybe (repeat [BU] (length l)) (quots_bv l r) -val mod_vec_int : list bitU -> integer -> list bitU -val quot_vec_int : list bitU -> integer -> list bitU -let mod_vec_int = mod_bv_int -let quot_vec_int = quot_bv_int +val mod_vec_int : list bitU -> integer -> list bitU +val quot_vec_int : list bitU -> integer -> list bitU +let mod_vec_int l r = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r) +let quot_vec_int l r = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r) val replicate_bits : list bitU -> integer -> list bitU let replicate_bits = replicate_bits_bv val duplicate : bitU -> integer -> list bitU let duplicate = duplicate_bit_bv +let duplicate_maybe b n = Just (duplicate b n) +let duplicate_fail b n = return (duplicate b n) +let duplicate_oracle b n = + bool_of_bitU_oracle b >>= (fun b -> + return (duplicate (bitU_of_bool b) n)) val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 7411c0a9..ea7c11cf 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -2,59 +2,109 @@ open import Pervasives_extra open import Machine_word open import Sail_values open import Sail_operators +open import Prompt_monad +open import Prompt + +val mword_zero : forall 'a. Size 'a => mword 'a +let mword_zero = wordFromInteger 0 (* Specialisation of operators to machine words *) +let uint v = unsignedIntegerFromWord v +let uint_maybe v = Just (uint v) +let uint_fail v = return (uint v) +let uint_oracle v = return (uint v) + +let sint v = signedIntegerFromWord v +let sint_maybe v = Just (sint v) +let sint_fail v = return (sint v) +let sint_oracle v = return (sint v) + +val vec_of_bits_failwith : forall 'a. Size 'a => integer -> list bitU -> mword 'a +let vec_of_bits_failwith _ bits = of_bits_failwith bits + +val vec_of_bits_fail : forall 'rv 'a 'e. Size 'a => integer -> list bitU -> monad 'rv (mword 'a) 'e +let vec_of_bits_fail _ bits = of_bits_fail bits + +val vec_of_bits_oracle : forall 'rv 'a 'e. Size 'a => integer -> list bitU -> monad 'rv (mword 'a) 'e +let vec_of_bits_oracle _ bits = of_bits_oracle bits + val access_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU let access_vec_inc = access_bv_inc val access_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU let access_vec_dec = access_bv_dec -val update_vec_inc : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a -let update_vec_inc = update_bv_inc +let update_vec_dec_maybe w i b = update_mword_dec w i b +let update_vec_dec_fail w i b = + bool_of_bitU_fail b >>= (fun b -> + return (update_mword_bool_dec w i b)) +let update_vec_dec_oracle w i b = + bool_of_bitU_oracle b >>= (fun b -> + return (update_mword_bool_dec w i b)) +let update_vec_dec w i b = maybe_failwith (update_vec_dec_maybe w i b) + +let update_vec_inc_maybe w i b = update_mword_inc w i b +let update_vec_inc_fail w i b = + bool_of_bitU_fail b >>= (fun b -> + return (update_mword_bool_inc w i b)) +let update_vec_inc_oracle w i b = + bool_of_bitU_oracle b >>= (fun b -> + return (update_mword_bool_inc w i b)) +let update_vec_inc w i b = maybe_failwith (update_vec_inc_maybe w i b) -val update_vec_dec : forall 'a. Size 'a => mword 'a -> integer -> bitU -> mword 'a -let update_vec_dec = update_bv_dec +val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b +let subrange_vec_dec w i j = Machine_word.word_extract (nat_of_int i) (nat_of_int j) w val subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -let subrange_vec_inc = subrange_bv_inc +let subrange_vec_inc w i j = subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) -val subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -let subrange_vec_dec = subrange_bv_dec +val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a +let update_subrange_vec_dec w i j w' = Machine_word.word_update w (nat_of_int i) (nat_of_int j) w' val update_subrange_vec_inc : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_subrange_vec_inc = update_subrange_bv_inc - -val update_subrange_vec_dec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_subrange_vec_dec = update_subrange_bv_dec +let update_subrange_vec_inc w i j w' = update_subrange_vec_dec w (length w - 1 - i) (length w - 1 - j) w' val extz_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let extz_vec = extz_bv +let extz_vec _ w = Machine_word.zeroExtend w val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let exts_vec = exts_bv +let exts_vec _ w = Machine_word.signExtend w val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c -let concat_vec = concat_bv - -val cons_vec : forall 'a 'b 'c. Size 'a, Size 'b => bitU -> mword 'a -> mword 'b -let cons_vec = cons_bv - -val bool_of_vec : mword ty1 -> bitU -let bool_of_vec = bool_of_bv - -val cast_unit_vec : bitU -> mword ty1 -let cast_unit_vec = cast_unit_bv - -val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a -let vec_of_bit = bv_of_bit +let concat_vec = Machine_word.word_concat + +val cons_vec_bool : forall 'a 'b 'c. Size 'a, Size 'b => bool -> mword 'a -> mword 'b +let cons_vec_bool b w = wordFromBitlist (b :: bitlistFromWord w) +let cons_vec_maybe b w = Maybe.map (fun b -> cons_vec_bool b w) (bool_of_bitU b) +let cons_vec_fail b w = bool_of_bitU_fail b >>= (fun b -> return (cons_vec_bool b w)) +let cons_vec_oracle b w = bool_of_bitU_oracle b >>= (fun b -> return (cons_vec_bool b w)) +let cons_vec b w = maybe_failwith (cons_vec_maybe b w) + +val vec_of_bool : forall 'a. Size 'a => integer -> bool -> mword 'a +let vec_of_bool _ b = wordFromBitlist [b] +let vec_of_bit_maybe len b = Maybe.map (vec_of_bool len) (bool_of_bitU b) +let vec_of_bit_fail len b = bool_of_bitU_fail b >>= (fun b -> return (vec_of_bool len b)) +let vec_of_bit_oracle len b = bool_of_bitU_oracle b >>= (fun b -> return (vec_of_bool len b)) +let vec_of_bit len b = maybe_failwith (vec_of_bit_maybe len b) + +val cast_bool_vec : bool -> mword ty1 +let cast_bool_vec b = vec_of_bool 1 b +let cast_unit_vec_maybe b = vec_of_bit_maybe 1 b +let cast_unit_vec_fail b = bool_of_bitU_fail b >>= (fun b -> return (cast_bool_vec b)) +let cast_unit_vec_oracle b = bool_of_bitU_oracle b >>= (fun b -> return (cast_bool_vec b)) +let cast_unit_vec b = maybe_failwith (cast_unit_vec_maybe b) val msb : forall 'a. Size 'a => mword 'a -> bitU let msb = most_significant val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer -let int_of_vec = int_of_bv +let int_of_vec sign w = + if sign + then signedIntegerFromWord w + else unsignedIntegerFromWord w +let int_of_vec_maybe sign w = Just (int_of_vec sign w) +let int_of_vec_fail sign w = return (int_of_vec sign w) val string_of_vec : forall 'a. Size 'a => mword 'a -> string let string_of_vec = string_of_bv @@ -63,63 +113,83 @@ val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val or_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a val not_vec : forall 'a. Size 'a => mword 'a -> mword 'a -let and_vec = and_bv -let or_vec = or_bv -let xor_vec = xor_bv -let not_vec = not_bv +let and_vec = Machine_word.lAnd +let or_vec = Machine_word.lOr +let xor_vec = Machine_word.lXor +let not_vec = Machine_word.lNot val add_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 adds_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 smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b -let add_vec = add_bv -let sadd_vec = sadd_bv -let sub_vec = sub_bv -let mult_vec = mult_bv -let smult_vec = smult_bv +val mults_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword 'b +let add_vec l r = arith_op_bv integerAdd false l r +let adds_vec l r = arith_op_bv integerAdd true l r +let sub_vec l r = arith_op_bv integerMinus true l r +let mult_vec l r = arith_op_bv integerMult false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b) +let mults_vec l r = arith_op_bv integerMult true (signExtend l : mword 'b) (signExtend r : mword 'b) 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 +val adds_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 smult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -let add_vec_int = add_bv_int -let sadd_vec_int = sadd_bv_int -let sub_vec_int = sub_bv_int -let mult_vec_int = mult_bv_int -let smult_vec_int = smult_bv_int +val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let add_vec_int l r = arith_op_bv_int integerAdd false l r +let adds_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus true l r +let mult_vec_int l r = arith_op_bv_int integerMult false (zeroExtend l : mword 'b) r +let mults_vec_int l r = arith_op_bv_int integerMult true (signExtend l : mword 'b) r val add_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 adds_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 smult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let add_int_vec = add_int_bv -let sadd_int_vec = sadd_int_bv -let sub_int_vec = sub_int_bv -let mult_int_vec = mult_int_bv -let smult_int_vec = smult_int_bv - -val add_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 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) -val add_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val sub_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -val mult_overflow_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> (mword 'a * bitU * bitU) -let add_overflow_vec = add_overflow_bv -let add_overflow_vec_signed = add_overflow_bv_signed -let sub_overflow_vec = sub_overflow_bv -let sub_overflow_vec_signed = sub_overflow_bv_signed -let mult_overflow_vec = mult_overflow_bv -let mult_overflow_vec_signed = mult_overflow_bv_signed +val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b +let add_int_vec l r = arith_op_int_bv integerAdd false l r +let adds_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus true l r +let mult_int_vec l r = arith_op_int_bv integerMult false l (zeroExtend r : mword 'b) +let mults_int_vec l r = arith_op_int_bv integerMult true l (signExtend r : mword 'b) + +val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a +val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a +val sub_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a + +let add_vec_bool l r = arith_op_bv_bool integerAdd false l r +let add_vec_bit_maybe l r = Maybe.map (add_vec_bool l) (bool_of_bitU r) +let add_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (add_vec_bool l r)) +let add_vec_bit l r = maybe_failwith (add_vec_bit_maybe l r) + +let adds_vec_bool l r = arith_op_bv_bool integerAdd true l r +let adds_vec_bit_maybe l r = Maybe.map (adds_vec_bool l) (bool_of_bitU r) +let adds_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (adds_vec_bool l r)) +let adds_vec_bit l r = maybe_failwith (adds_vec_bit_maybe l r) + +let sub_vec_bool l r = arith_op_bv_bool integerMinus true l r +let sub_vec_bit_maybe l r = Maybe.map (sub_vec_bool l) (bool_of_bitU r) +let sub_vec_bit_fail l r = bool_of_bitU_fail r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit_oracle l r = bool_of_bitU_oracle r >>= (fun r -> return (sub_vec_bool l r)) +let sub_vec_bit l r = maybe_failwith (sub_vec_bit_maybe l r) + +(* TODO +val maybe_mword_of_bits_overflow : forall 'a. Size 'a => (list bitU * bitU * bitU) -> maybe (mword 'a * bitU * bitU) +let maybe_mword_of_bits_overflow (bits, overflow, carry) = + Maybe.map (fun w -> (w, overflow, carry)) (of_bits bits) + +val add_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val adds_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val sub_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val subs_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mult_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +val mults_overflow_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> maybe (mword 'a * bitU * bitU) +let add_overflow_vec l r = maybe_mword_of_bits_overflow (add_overflow_bv l r) +let adds_overflow_vec l r = maybe_mword_of_bits_overflow (adds_overflow_bv l r) +let sub_overflow_vec l r = maybe_mword_of_bits_overflow (sub_overflow_bv l r) +let subs_overflow_vec l r = maybe_mword_of_bits_overflow (subs_overflow_bv l r) +let mult_overflow_vec l r = maybe_mword_of_bits_overflow (mult_overflow_bv l r) +let mults_overflow_vec l r = maybe_mword_of_bits_overflow (mults_overflow_bv l r) val add_overflow_vec_bit : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) val add_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mword 'a * bitU * bitU) @@ -128,36 +198,40 @@ val sub_overflow_vec_bit_signed : forall 'a. Size 'a => mword 'a -> bitU -> (mw let add_overflow_vec_bit = add_overflow_bv_bit let add_overflow_vec_bit_signed = add_overflow_bv_bit_signed let sub_overflow_vec_bit = sub_overflow_bv_bit -let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed +let sub_overflow_vec_bit_signed = sub_overflow_bv_bit_signed*) val shiftl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -let shiftl = shiftl_bv -let shiftr = shiftr_bv -let arith_shiftr = arith_shiftr_bv -let rotl = rotl_bv -let rotr = rotr_bv - -val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -val quot_vec_signed : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a -let mod_vec = mod_bv -let quot_vec = quot_bv -let quot_vec_signed = quot_bv_signed +let shiftl = shiftl_mword +let shiftr = shiftr_mword +let arith_shiftr = arith_shiftr_mword +let rotl = rotl_mword +let rotr = rotr_mword + +val mod_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +val quot_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +val quots_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a +let mod_vec = mod_mword +let quot_vec = quot_mword +let quots_vec = quots_mword val mod_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a val quot_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -let mod_vec_int = mod_bv_int -let quot_vec_int = quot_bv_int +let mod_vec_int = mod_mword_int +let quot_vec_int = quot_mword_int val replicate_bits : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -let replicate_bits = replicate_bits_bv +let replicate_bits v count = wordFromBitlist (repeat (bitlistFromWord v) count) -val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a -let duplicate = duplicate_bit_bv +val duplicate_bool : forall 'a. Size 'a => bool -> integer -> mword 'a +let duplicate_bool b n = wordFromBitlist (repeat [b] n) +let duplicate_maybe b n = Maybe.map (fun b -> duplicate_bool b n) (bool_of_bitU b) +let duplicate_fail b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_bool b n)) +let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n)) +let duplicate b n = maybe_failwith (duplicate_maybe b n) val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool @@ -169,13 +243,13 @@ val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -let eq_vec = eq_bv -let neq_vec = neq_bv -let ult_vec = ult_bv -let slt_vec = slt_bv -let ugt_vec = ugt_bv -let sgt_vec = sgt_bv -let ulteq_vec = ulteq_bv -let slteq_vec = slteq_bv -let ugteq_vec = ugteq_bv -let sgteq_vec = sgteq_bv +let eq_vec = eq_mword +let neq_vec = neq_mword +let ult_vec = ucmp_mword (<) +let slt_vec = scmp_mword (<) +let ugt_vec = ucmp_mword (>) +let sgt_vec = scmp_mword (>) +let ulteq_vec = ucmp_mword (<=) +let slteq_vec = scmp_mword (<=) +let ugteq_vec = ucmp_mword (>=) +let sgteq_vec = scmp_mword (>=) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index edb8da88..238ebe58 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,5 +1,3 @@ -(* Version of sail_values.lem that uses Lem's machine words library *) - open import Pervasives_extra open import Machine_word (*open import Sail_impl_base*) @@ -8,8 +6,11 @@ open import Machine_word type ii = integer type nn = natural +val nat_of_int : integer -> nat +let nat_of_int i = if i < 0 then 0 else natFromInteger i + val pow : integer -> integer -> integer -let pow m n = m ** (natFromInteger n) +let pow m n = m ** (nat_of_int n) let pow2 n = pow 2 n @@ -31,7 +32,7 @@ let mult_int l r = integerMult l r let div_int l r = integerDiv l r let div_nat l r = natDiv l r let power_int_nat l r = integerPow l r -let power_int_int l r = integerPow l (natFromInteger r) +let power_int_int l r = integerPow l (nat_of_int r) let negate_int i = integerNegate i let min_int l r = integerMin l r let max_int l r = integerMax l r @@ -50,8 +51,8 @@ let xor_bool l r = xor l r let append_list l r = l ++ r let length_list xs = integerFromNat (List.length xs) -let take_list n xs = List.take (natFromInteger n) xs -let drop_list n xs = List.drop (natFromInteger n) xs +let take_list n xs = List.take (nat_of_int n) xs +let drop_list n xs = List.drop (nat_of_int n) xs val repeat : forall 'a. list 'a -> integer -> list 'a let rec repeat xs n = @@ -99,6 +100,29 @@ let min_8 = (0 - 128 : integer) let max_5 = (31 : integer) let min_5 = (0 - 32 : integer) +(* just_list takes a list of maybes and returns Just xs if all elements have + a value, and Nothing if one of the elements is Nothing. *) +val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a) +let rec just_list l = match l with + | [] -> Just [] + | (x :: xs) -> + match (x, just_list xs) with + | (Just x, Just xs) -> Just (x :: xs) + | (_, _) -> Nothing + end + end +declare {isabelle} termination_argument just_list = automatic + +lemma just_list_spec: + ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) && + (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es))) + +val maybe_failwith : forall 'a. maybe 'a -> 'a +let maybe_failwith = function + | Just a -> a + | Nothing -> failwith "maybe_failwith" +end + (*** Bits *) type bitU = B0 | B1 | BU @@ -118,6 +142,25 @@ instance (Show bitU) let show = showBitU end +val compare_bitU : bitU -> bitU -> ordering +let compare_bitU l r = match (l, r) with + | (BU, BU) -> EQ + | (B0, B0) -> EQ + | (B1, B1) -> EQ + | (BU, _) -> LT + | (_, BU) -> GT + | (B0, _) -> LT + | (_, _) -> GT +end + +instance (Ord bitU) + let compare = compare_bitU + let (<) l r = (compare_bitU l r) = LT + let (<=) l r = (compare_bitU l r) <> GT + let (>) l r = (compare_bitU l r) = GT + let (>=) l r = (compare_bitU l r) <> LT +end + class (BitU 'a) val to_bitU : 'a -> bitU val of_bitU : bitU -> 'a @@ -129,44 +172,20 @@ instance (BitU bitU) end let bool_of_bitU = function - | B0 -> false - | B1 -> true - | BU -> failwith "bool_of_bitU applied to BU" + | B0 -> Just false + | B1 -> Just true + | BU -> Nothing end let bitU_of_bool b = if b then B1 else B0 -instance (BitU bool) +(*instance (BitU bool) let to_bitU = bitU_of_bool let of_bitU = bool_of_bitU -end +end*) let cast_bit_bool = bool_of_bitU -(*let bit_lifted_of_bitU = function - | B0 -> Bitl_zero - | B1 -> Bitl_one - | BU -> Bitl_undef - end - -let bitU_of_bit = function - | Bitc_zero -> B0 - | Bitc_one -> B1 - end - -let bit_of_bitU = function - | B0 -> Bitc_zero - | B1 -> Bitc_one - | BU -> failwith "bit_of_bitU: BU" - end - -let bitU_of_bit_lifted = function - | Bitl_zero -> B0 - | Bitl_one -> B1 - | Bitl_undef -> BU - | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" - end*) - let not_bit = function | B1 -> B0 | B0 -> B1 @@ -177,20 +196,33 @@ val is_one : integer -> bitU let is_one i = if i = 1 then B1 else B0 -let binop_bit op x y = match (x, y) with - | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (x,y) -> bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y)) - end - val and_bit : bitU -> bitU -> bitU -let and_bit = binop_bit (&&) +let and_bit x y = + match (x, y) with + | (B0, _) -> B0 + | (_, B0) -> B0 + | (B1, B1) -> B1 + | (_, _) -> BU + end val or_bit : bitU -> bitU -> bitU -let or_bit = binop_bit (||) +let or_bit x y = + match (x, y) with + | (B1, _) -> B1 + | (_, B1) -> B1 + | (B0, B0) -> B0 + | (_, _) -> BU + end val xor_bit : bitU -> bitU -> bitU -let xor_bit = binop_bit xor +let xor_bit x y= + match (x, y) with + | (B0, B0) -> B0 + | (B0, B1) -> B1 + | (B1, B0) -> B1 + | (B1, B1) -> B0 + | (_, _) -> BU + end val (&.) : bitU -> bitU -> bitU let inline (&.) x y = and_bit x y @@ -202,81 +234,134 @@ val (+.) : bitU -> bitU -> bitU let inline (+.) x y = xor_bit x y -(*** Bit lists ***) +(*** Bool lists ***) -val bits_of_nat_aux : natural -> list bitU -let rec bits_of_nat_aux x = +val bools_of_nat_aux : natural -> list bool +let rec bools_of_nat_aux x = if x = 0 then [] - else (if x mod 2 = 1 then B1 else B0) :: bits_of_nat_aux (x / 2) -declare {isabelle} termination_argument bits_of_nat_aux = automatic -let bits_of_nat n = List.reverse (bits_of_nat_aux n) + else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2) +declare {isabelle} termination_argument bools_of_nat_aux = automatic +let bools_of_nat n = List.reverse (bools_of_nat_aux n) -val nat_of_bits_aux : natural -> list bitU -> natural -let rec nat_of_bits_aux acc bs = match bs with +val nat_of_bools_aux : natural -> list bool -> natural +let rec nat_of_bools_aux acc bs = match bs with | [] -> acc - | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs - | B0 :: bs -> nat_of_bits_aux (2 * acc) bs - | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits" + | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs + | false :: bs -> nat_of_bools_aux (2 * acc) bs end -declare {isabelle} termination_argument nat_of_bits_aux = automatic -let nat_of_bits bits = nat_of_bits_aux 0 bits +declare {isabelle} termination_argument nat_of_bools_aux = automatic +let nat_of_bools bs = nat_of_bools_aux 0 bs + +val unsigned_of_bools : list bool -> integer +let unsigned_of_bools bs = integerFromNatural (nat_of_bools bs) + +val signed_of_bools : list bool -> integer +let signed_of_bools bs = + match bs with + | true :: _ -> 0 - (1 + (unsigned_of_bools (List.map not bs))) + | false :: _ -> unsigned_of_bools bs + | [] -> 0 (* Treat empty list as all zeros *) + end -let not_bits = List.map not_bit +val int_of_bools : bool -> list bool -> integer +let int_of_bools sign bs = if sign then signed_of_bools bs else unsigned_of_bools bs -let binop_bits op bsl bsr = - foldr (fun (bl, br) acc -> binop_bit op bl br :: acc) [] (zip bsl bsr) +val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a +let rec pad_list x xs n = + if n <= 0 then xs else pad_list x (x :: xs) (n - 1) +declare {isabelle} termination_argument pad_list = automatic -let and_bits = binop_bits (&&) -let or_bits = binop_bits (||) -let xor_bits = binop_bits xor +let ext_list pad len xs = + let longer = len - (integerFromNat (List.length xs)) in + if longer < 0 then drop (nat_of_int (abs (longer))) xs + else pad_list pad xs longer -val unsigned_of_bits : list bitU -> integer -let unsigned_of_bits bs = integerFromNatural (nat_of_bits bs) +let extz_bools len bs = ext_list false len bs +let exts_bools len bs = + match bs with + | true :: _ -> ext_list true len bs + | _ -> ext_list false len bs + end -val signed_of_bits : list bitU -> integer -let signed_of_bits bits = - match bits with - | B1 :: _ -> 0 - (1 + (unsigned_of_bits (not_bits bits))) - | B0 :: _ -> unsigned_of_bits bits - | BU :: _ -> failwith "signed_of_bits applied to list with undefined bits" - | [] -> failwith "signed_of_bits applied to empty list" +let rec add_one_bool_ignore_overflow_aux bits = match bits with + | [] -> [] + | false :: bits -> true :: bits + | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits +end +declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic + +let add_one_bool_ignore_overflow bits = + List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits)) + +let bool_list_of_int n = + let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in + if n >= (0 : integer) then bs_abs + else add_one_bool_ignore_overflow (List.map not bs_abs) +let bools_of_int len n = exts_bools len (bool_list_of_int n) + +(*** Bit lists ***) + +val has_undefined_bits : list bitU -> bool +let has_undefined_bits bs = List.any (function BU -> true | _ -> false end) bs + +let bits_of_nat n = List.map bitU_of_bool (bools_of_nat n) + +let nat_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (nat_of_bools bs) + | Nothing -> Nothing + end + +let not_bits = List.map not_bit + +val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a +let binop_list op xs ys = + foldr (fun (x, y) acc -> op x y :: acc) [] (zip xs ys) + +let unsigned_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (unsigned_of_bools bs) + | Nothing -> Nothing end -val pad_bitlist : bitU -> list bitU -> integer -> list bitU -let rec pad_bitlist b bits n = - if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1) -declare {isabelle} termination_argument pad_bitlist = automatic +let signed_of_bits bits = + match (just_list (List.map bool_of_bitU bits)) with + | Just bs -> Just (signed_of_bools bs) + | Nothing -> Nothing + end -let ext_bits pad len bits = - let longer = len - (integerFromNat (List.length bits)) in - if longer < 0 then drop (natFromInteger (abs (longer))) bits - else pad_bitlist pad bits longer +val int_of_bits : bool -> list bitU -> maybe integer +let int_of_bits sign bs = if sign then signed_of_bits bs else unsigned_of_bits bs -let extz_bits len bits = ext_bits B0 len bits +let extz_bits len bits = ext_list B0 len bits let exts_bits len bits = match bits with - | BU :: _ -> failwith "exts_bits: undefined bit" - | B1 :: _ -> ext_bits B1 len bits - | _ -> ext_bits B0 len bits + | BU :: _ -> ext_list BU len bits + | B1 :: _ -> ext_list B1 len bits + | _ -> ext_list B0 len bits end let rec add_one_bit_ignore_overflow_aux bits = match bits with | [] -> [] | B0 :: bits -> B1 :: bits | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits - | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" + | BU :: bits -> BU :: List.map (fun _ -> BU) bits end declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) -let bitlist_of_int n = - let bits_abs = B0 :: bits_of_nat (naturalFromInteger (abs n)) in - if n >= (0 : integer) then bits_abs - else add_one_bit_ignore_overflow (not_bits bits_abs) +let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n) +let bits_of_int len n = exts_bits len (bit_list_of_int n) -let bits_of_int len n = exts_bits len (bitlist_of_int n) +val arith_op_bits : + (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU +let arith_op_bits op sign l r = + match (int_of_bits sign l, int_of_bits sign r) with + | (Just li, Just ri) -> bits_of_int (length_list l) (op li ri) + | (_, _) -> repeat [BU] (length_list l) + end let char_of_nibble = function | (B0, B0, B0, B0) -> Just #'0' @@ -322,8 +407,8 @@ let inline (^^) = append_list val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a let subrange_list_inc xs i j = - let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in - let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in + let (toJ,_suffix) = List.splitAt (nat_of_int (j + 1)) xs in + let (_prefix,fromItoJ) = List.splitAt (nat_of_int i) toJ in fromItoJ val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a @@ -336,8 +421,8 @@ let subrange_list is_inc xs i j = if is_inc then subrange_list_inc xs i j else s val update_subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a let update_subrange_list_inc xs i j xs' = - let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in - let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in + let (toJ,suffix) = List.splitAt (nat_of_int (j + 1)) xs in + let (prefix,_fromItoJ) = List.splitAt (nat_of_int i) toJ in prefix ++ xs' ++ suffix val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a @@ -350,7 +435,7 @@ let update_subrange_list is_inc xs i j xs' = if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs' val access_list_inc : forall 'a. list 'a -> integer -> 'a -let access_list_inc xs n = List_extra.nth xs (natFromInteger n) +let access_list_inc xs n = List_extra.nth xs (nat_of_int n) val access_list_dec : forall 'a. list 'a -> integer -> 'a let access_list_dec xs n = @@ -362,7 +447,7 @@ let access_list is_inc xs n = if is_inc then access_list_inc xs n else access_list_dec xs n val update_list_inc : forall 'a. list 'a -> integer -> 'a -> list 'a -let update_list_inc xs n x = List.update xs (natFromInteger n) x +let update_list_inc xs n x = List.update xs (nat_of_int n) x val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a let update_list_dec xs n x = @@ -373,36 +458,19 @@ val update_list : forall 'a. bool -> list 'a -> integer -> 'a -> list 'a let update_list is_inc xs n x = if is_inc then update_list_inc xs n x else update_list_dec xs n x -let extract_only_element = function - | [] -> failwith "extract_only_element called for empty list" +let extract_only_bit = function + | [] -> BU | [e] -> e - | _ -> failwith "extract_only_element called for list with more elements" + | _ -> BU end -(* just_list takes a list of maybes and returns Just xs if all elements have - a value, and Nothing if one of the elements is Nothing. *) -val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a) -let rec just_list l = match l with - | [] -> Just [] - | (x :: xs) -> - match (x, just_list xs) with - | (Just x, Just xs) -> Just (x :: xs) - | (_, _) -> Nothing - end - end -declare {isabelle} termination_argument just_list = automatic - -lemma just_list_spec: - ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) && - (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es))) - (*** Machine words *) val length_mword : forall 'a. mword 'a -> integer let length_mword w = integerFromNat (word_length w) val slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -let slice_mword_dec w i j = word_extract (natFromInteger i) (natFromInteger j) w +let slice_mword_dec w i j = word_extract (nat_of_int i) (nat_of_int j) w val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b let slice_mword_inc w i j = @@ -413,7 +481,7 @@ val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword let slice_mword is_inc w i j = if is_inc then slice_mword_inc w i j else slice_mword_dec w i j val update_slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a -let update_slice_mword_dec w i j w' = word_update w (natFromInteger i) (natFromInteger j) w' +let update_slice_mword_dec w i j w' = word_update w (nat_of_int i) (nat_of_int j) w' val update_slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a let update_slice_mword_inc w i j w' = @@ -425,7 +493,7 @@ let update_slice_mword is_inc w i j w' = if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w' val access_mword_dec : forall 'a. mword 'a -> integer -> bitU -let access_mword_dec w n = bitU_of_bool (getBit w (natFromInteger n)) +let access_mword_dec w n = bitU_of_bool (getBit w (nat_of_int n)) val access_mword_inc : forall 'a. mword 'a -> integer -> bitU let access_mword_inc w n = @@ -436,22 +504,19 @@ val access_mword : forall 'a. bool -> mword 'a -> integer -> bitU let access_mword is_inc w n = if is_inc then access_mword_inc w n else access_mword_dec w n -val update_mword_dec : forall 'a. mword 'a -> integer -> bitU -> mword 'a -let update_mword_dec w n b = setBit w (natFromInteger n) (bool_of_bitU b) +val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a +let update_mword_bool_dec w n b = setBit w (nat_of_int n) b +let update_mword_dec w n b = Maybe.map (update_mword_bool_dec w n) (bool_of_bitU b) -val update_mword_inc : forall 'a. mword 'a -> integer -> bitU -> mword 'a -let update_mword_inc w n b = +val update_mword_bool_inc : forall 'a. mword 'a -> integer -> bool -> mword 'a +let update_mword_bool_inc w n b = let top = (length_mword w) - 1 in - update_mword_dec w (top - n) b - -val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a -let update_mword is_inc w n b = - if is_inc then update_mword_inc w n b else update_mword_dec w n b + update_mword_bool_dec w (top - n) b +let update_mword_inc w n b = Maybe.map (update_mword_bool_inc w n) (bool_of_bitU b) -val mword_of_int : forall 'a. Size 'a => integer -> integer -> mword 'a -let mword_of_int len n = - let w = wordFromInteger n in - if (length_mword w = len) then w else failwith "unexpected word length" +val int_of_mword : forall 'a. bool -> mword 'a -> integer +let int_of_mword sign w = + if sign then signedIntegerFromWord w else unsignedIntegerFromWord w (* Translating between a type level number (itself 'n) and an integer *) @@ -461,68 +526,71 @@ let size_itself_int x = integerFromNat (size_itself x) the actual integer is ignored. *) val make_the_value : forall 'n. integer -> itself 'n -let inline make_the_value x = the_value +let inline make_the_value = (fun _ -> the_value) (*** Bitvectors *) class (Bitvector 'a) val bits_of : 'a -> list bitU - val of_bits : list bitU -> 'a - (* The first parameter specifies the desired length of the bitvector *) - val of_int : integer -> integer -> 'a + (* We allow of_bits to be partial, as not all bitvector representations + support undefined bits *) + val of_bits : list bitU -> maybe 'a + val of_bools : list bool -> 'a val length : 'a -> integer - val unsigned : 'a -> integer - val signed : 'a -> integer - (* The first parameter specifies the indexing order (true is increasing) *) - val get_bit : bool -> 'a -> integer -> bitU - val set_bit : bool -> 'a -> integer -> bitU -> 'a - val get_bits : bool -> 'a -> integer -> integer -> list bitU - val set_bits : bool -> 'a -> integer -> integer -> list bitU -> 'a + (* of_int: the first parameter specifies the desired length of the bitvector *) + val of_int : integer -> integer -> 'a + (* Conversion to integers is undefined if any bit is undefined *) + val unsigned : 'a -> maybe integer + val signed : 'a -> maybe integer + (* Lifting of integer operations to bitvectors: The boolean flag indicates + whether to treat the bitvectors as signed (true) or not (false). *) + val arith_op_bv : (integer -> integer -> integer) -> bool -> 'a -> 'a -> 'a end +val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a +let of_bits_failwith bits = maybe_failwith (of_bits bits) + +let int_of_bv sign = if sign then signed else unsigned + instance forall 'a. BitU 'a => (Bitvector (list 'a)) let bits_of v = List.map to_bitU v - let of_bits v = List.map of_bitU v + let of_bits v = Just (List.map of_bitU v) + let of_bools v = List.map of_bitU (List.map bitU_of_bool v) let of_int len n = List.map of_bitU (bits_of_int len n) let length = length_list let unsigned v = unsigned_of_bits (List.map to_bitU v) let signed v = signed_of_bits (List.map to_bitU v) - let get_bit is_inc v n = to_bitU (access_list is_inc v n) - let set_bit is_inc v n b = update_list is_inc v n (of_bitU b) - let get_bits is_inc v i j = List.map to_bitU (subrange_list is_inc v i j) - let set_bits is_inc v i j v' = update_subrange_list is_inc v i j (List.map of_bitU v') + let arith_op_bv op sign l r = List.map of_bitU (arith_op_bits op sign (List.map to_bitU l) (List.map to_bitU r)) end instance forall 'a. Size 'a => (Bitvector (mword 'a)) - let bits_of v = List.map to_bitU (bitlistFromWord v) - let of_bits v = wordFromBitlist (List.map of_bitU v) - let of_int = mword_of_int + let bits_of v = List.map bitU_of_bool (bitlistFromWord v) + let of_bits v = Maybe.map wordFromBitlist (just_list (List.map bool_of_bitU v)) + let of_bools v = wordFromBitlist v + let of_int = (fun _ n -> wordFromInteger n) let length v = integerFromNat (word_length v) - let unsigned = unsignedIntegerFromWord - let signed = signedIntegerFromWord - let get_bit = access_mword - let set_bit = update_mword - let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j - let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v') + let unsigned v = Just (unsignedIntegerFromWord v) + let signed v = Just (signedIntegerFromWord v) + let arith_op_bv op sign l r = wordFromInteger (op (int_of_mword sign l) (int_of_mword sign r)) end -let access_bv_inc v n = get_bit true v n -let access_bv_dec v n = get_bit false v n +let access_bv_inc v n = access_list true (bits_of v) n +let access_bv_dec v n = access_list false (bits_of v) n -let update_bv_inc v n b = set_bit true v n b -let update_bv_dec v n b = set_bit false v n b +let update_bv_inc v n b = update_list true (bits_of v) n b +let update_bv_dec v n b = update_list false (bits_of v) n b -let subrange_bv_inc v i j = of_bits (get_bits true v i j) -let subrange_bv_dec v i j = of_bits (get_bits false v i j) +let subrange_bv_inc v i j = subrange_list true (bits_of v) i j +let subrange_bv_dec v i j = subrange_list false (bits_of v) i j -let update_subrange_bv_inc v i j v' = set_bits true v i j (bits_of v') -let update_subrange_bv_dec v i j v' = set_bits false v i j (bits_of v') +let update_subrange_bv_inc v i j v' = update_subrange_list true (bits_of v) i j (bits_of v') +let update_subrange_bv_dec v i j v' = update_subrange_list false (bits_of v) i j (bits_of v') -val extz_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b -let extz_bv n v = of_bits (extz_bits n (bits_of v)) +val extz_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU +let extz_bv n v = extz_bits n (bits_of v) -val exts_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b -let exts_bv n v = of_bits (exts_bits n (bits_of v)) +val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU +let exts_bv n v = exts_bits n (bits_of v) val string_of_bv : forall 'a. Bitvector 'a => 'a -> string let string_of_bv v = show_bitlist (bits_of v) @@ -543,8 +611,8 @@ declare {isabelle} termination_argument byte_chunks = automatic val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte) let bytes_of_bits bs = byte_chunks (bits_of bs) -val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a -let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs)) +val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> list bitU +let bits_of_bytes bs = List.concat (List.map bits_of bs) let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs) let bits_of_mem_bytes bs = bits_of_bytes (List.reverse bs) @@ -596,9 +664,6 @@ let rec reverse_endianness_list bits = if List.length bits <= 8 then bits else reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits -val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a -let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v)) - (*** Registers *) @@ -760,10 +825,10 @@ let internal_mem_value bytes = val foreach : forall 'a 'vars. (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars let rec foreach l vars body = -match l with -| [] -> vars -| (x :: xs) -> foreach xs (body x vars) body -end + match l with + | [] -> vars + | (x :: xs) -> foreach xs (body x vars) body + end declare {isabelle} termination_argument foreach = automatic @@ -783,13 +848,6 @@ let rec until vars cond body = if cond vars then vars else until (body vars) cond body -let assert' b msg_opt = - let msg = match msg_opt with - | Just msg -> msg - | Nothing -> "unspecified error" - end in - if b then () else failwith msg - (* convert numbers unsafely to naturals *) class (ToNatural 'a) val toNatural : 'a -> natural end diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 9fcbd5ce..8253b800 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -120,14 +120,21 @@ let try_catchSR m h = | Right e -> h e end) +val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e +let maybe_failS msg = function + | Just a -> returnS a + | Nothing -> failS msg +end + val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e let read_tagS addr = - readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate)) + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> + readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate))) (* Read bytes from memory and return in little endian order *) val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e let read_mem_bytesS read_kind addr sz = - let addr = unsigned addr in + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in let addrs = index_list addr (addr+sz-1) 1 in let read_byte s addr = Map.lookup addr s.memstate in @@ -139,12 +146,12 @@ let read_mem_bytesS read_kind addr sz = else s) >>$ returnS mem_val | Nothing -> failS "read_memS" - end) + end)) val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e let read_memS rk a sz = - read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes -> - returnS (bits_of_mem_bytes bytes)) + read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes -> + maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e let excl_resultS () = @@ -154,9 +161,9 @@ let excl_resultS () = val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e let write_mem_eaS write_kind addr sz = - let addr = unsigned addr in + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in - updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>) + updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)) (* Write little-endian list of bytes to previously announced address *) val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e @@ -181,9 +188,9 @@ end val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e let write_tagS addr t = - (*let taddr = addr / cap_alignment in*) - updateS (fun s -> <| s with tagstate = Map.insert (unsigned addr) t s.tagstate |>) >>$ - returnS true + maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> + updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$ + returnS true) val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e let read_regS reg = readS (fun s -> reg.read_from s.regstate) |