diff options
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/armV8.sail | 2 | ||||
| -rw-r--r-- | aarch64_small/prelude.sail | 14 |
2 files changed, 4 insertions, 12 deletions
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail index f125ec72..a9a78900 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -2201,7 +2201,7 @@ function clause execute ( Division((d,n,m,datasize as int('R),_unsigned)) ) = { if IsZero(operand2) then result = 0 else - result = /* ARM: RoundTowardsZero*/ quot (_Int(operand1, _unsigned), _Int(operand2, _unsigned)); /* FIXME: does quot round towards zero? */ + result = /* ARM: RoundTowardsZero*/ tdiv_int (_Int(operand1, _unsigned), _Int(operand2, _unsigned)); wX(d) = to_bits(result) : (bits('R)) ; /* ARM: result[(datasize-1)..0] */ } diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index 2dbd2bf4..f97c84a6 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -150,17 +150,9 @@ overload operator ^ = {xor_vec, int_power, concat_str} val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l) -/* put this val spec into Sail lib for "%" */ - -val mod = { - smt: "mod", - ocaml: "modulus", - lem: "integerMod", - c: "tmod_int", - coq: "Z.rem" -} : forall 'M 'N. (int('M), int('N)) -> {'O, 0 <= 'O & 'O < N . int('O)} - -/* overload operator % = {mod_int} */ +overload operator % = {emod_int} +overload operator / = {ediv_int} +overload mod = {emod_int} val print = "print_endline" : string -> unit |