diff options
| author | Robert Norton | 2019-03-22 16:50:48 +0000 |
|---|---|---|
| committer | Robert Norton | 2019-03-22 16:55:23 +0000 |
| commit | f4acbce30be2aecdfc491478a24c5eb551824f24 (patch) | |
| tree | d09f2561e19ab1c4928f053c9f5226c06ce94ee6 /aarch64_small | |
| parent | c9471630ad64af00a58a3c92f4b6a22f2194e9ee (diff) | |
Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
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 |