Module `Libsail.Sail2_operators`Source

Source

val concat_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'a ->
  'b ->
  Sail2_values.bitU list

Source

val cons_bv : 
  'a Sail2_values.bitvector_class ->
  Sail2_values.bitU ->
  'a ->
  Sail2_values.bitU list

Sourceval cast_unit_bv : Sail2_values.bitU -> Sail2_values.bitU list

Sourceval bv_of_bit : Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list

Source

val most_significant : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Sail2_values.bitU

Sourceval get_max_representable_in : bool -> Nat_big_num.num -> Nat_big_num.num

Sourceval get_min_representable_in : 'a -> Nat_big_num.num -> Nat_big_num.num

Source

val arith_op_bv_int : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a ->
  Nat_big_num.num ->
  'a

Source

val arith_op_int_bv : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'a ->
  'a

Source

val arith_op_bv_bool : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a ->
  bool ->
  'a

Source

val arith_op_bv_bit : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a ->
  Sail2_values.bitU ->
  'a option

Sourcetype shift =

| LL_shift
| RR_shift
| RR_shift_arith
| LL_rot
| RR_rot

Sourceval invert_shift : shift -> shift

Source

val shift_op_bv : 
  'a Sail2_values.bitvector_class ->
  shift ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val shiftl_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val shiftr_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val arith_shiftr_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val rotl_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val rotr_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val shiftl_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

Source

val shiftr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

Source

val arith_shiftr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

Source

val rotl_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

Source

val rotr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

Source

val arith_op_no0 : 
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num option

Source

val arith_op_bv_no0 : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'a ->
  'a ->
  'b option

Source

val mod_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b ->
  'b ->
  'a option

Source

val quot_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b ->
  'b ->
  'a option

Source

val quots_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b ->
  'b ->
  'a option

Sourceval mod_mword : Lem.mword -> Lem.mword -> Lem.mword

Sourceval quot_mword : Lem.mword -> Lem.mword -> Lem.mword

Sourceval quots_mword : Lem.mword -> Lem.mword -> Lem.mword

Source

val arith_op_bv_int_no0 : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'a ->
  Nat_big_num.num ->
  'b option

Source

val quot_bv_int : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b ->
  Nat_big_num.num ->
  'a option

Source

val mod_bv_int : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b ->
  Nat_big_num.num ->
  'a option

Source

val mod_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

Source

val quot_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

Source

val quots_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

Source

val replicate_bits_bv : 
  'a Sail2_values.bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Source

val duplicate_bit_bv : 
  'a Sail2_values.bitU_class ->
  'a ->
  Nat_big_num.num ->
  Sail2_values.bitU list

Sourceval eq_bv : 'a Sail2_values.bitvector_class -> 'a -> 'a -> bool

Sourceval neq_bv : 'a Sail2_values.bitvector_class -> 'a -> 'a -> bool

Source

val get_slice_int_bv : 
  'a Sail2_values.bitvector_class ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a

Source

val set_slice_int_bv : 
  'a Sail2_values.bitvector_class ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a ->
  Nat_big_num.num

package libsail

Module Libsail.Sail2_operatorsSource

Module `Libsail.Sail2_operators`Source