AST-89 Range restricted Nat* and Int* #487

ggreif · 2019-06-07T15:43:52Z

https://dfinity.atlassian.net/browse/AST-89

Conversions work. Tests prove it. ~~There might be better ways of conversion at the 64-bit plane than going via string, but I am not aware of any.~~ I added ~~Maybe we should add~~ to/from_big_int methods to the NumType signature.

Open Issue: Since we don't have representational equivalence (subtyping) between Nat8 and Int8, we can't do the - : Nat8 -> Int8 hack, so we have to annotate like this: -(42 : Int8) to get the effect. There is was an attempt in the code to fix this, but it is was wrong as-is, and ~~will be~~ has been removed ~~unless we find a better way (e.g. automatic insertion of range checks). Same issue applies to binary operators ==, etc~~.

Laundry list:

and a `Nat` bugfix

- backend: all done -interpreter: `->Nat*` and `->Int*` mostly missing

word32ToNat32 3000000000; crashes word64ToNat64 300000000000000000; probably crashes

and other roundtrip tests

add range tests

and fix msb_adjust for Int/Nat -> IntN/NatN

still needs Int/Nat8/64!

caveat: when using libTomMath binding these fail: - intToInt8 (-128) - intToInt16 (-32768) -intToInt32 (-2147483648) The reason is that `fits_signed_bits` is buggy. (BigNum64 module works in this respect.)

relaxing the fits_signed_bits contract to work with 64

src/interpreter/interpret.ml

crusso

LGTM but I haven't reviewed the compiler - leaving that to Joachim.

PS. Part of me wants to redefine the fixed-size numeric literals so we just have three constructors (WordX, IntX and NatX) that take a module giving the interpretation of the type as an argument and a value of that type.
Something that might be expressed in Haskell as:
WordX : forall w :: Word w, w.
NumX: forwall w:: Num w. w.
NumBinOp: forall n :: Numeric n. nbop * exp * exp
LogBinOp: forall n :: Numeric n. lbop * exp * exp
NumUnOp: forall n :: Numeric n. nup * exp
LogNumOp: forall n :: Logical n. lup * exp
And then the interpeter/compiler would use the first-class module/dictionary to interpret/compile accordingly...
But maybe that would be less direct than what we have now.

crusso · 2019-06-17T13:13:32Z

src/interpreter/interpret.ml

@@ -720,7 +733,8 @@ let interpret_prog flags scope p : (V.value * scope) option =
    let vo = ref None in
    let ve = ref V.Env.empty in
    Scheduler.queue (fun () ->
-      interpret_block env p.it (Some ve) (fun v -> vo := Some v)
+      try interpret_block env p.it (Some ve) (fun v -> vo := Some v)
+      with Invalid_argument s -> trap !last_region "%s" s


Do you still need try … with ... now that you transform Invalid_argument to trap at the interpretation of operations?

I only catch some. I could not make catching where CallE is interpreted to work. (It would have broken general tail-recursion.) So this is still needed. In some ideal world we'll have failure continuations where we can feed the exception into, instead of raise.

What are the remaining places that raise Invalid_argument? Can't you just handle those, as you do for binop and immediately trap? CallE shouldn't (by itself) trap at all. If you think CallE should turn the failure of v_asfunc into a trap I think that is mistake since that an indicates a type soundness bug, not an expected trap. Or perhaps I'm misunderstanding.

Anyway, its probably not worth worrying about since the scheduler itself doesn't use tailcalls to evaluate its tasks:

module Scheduler = struct let q : (unit -> unit) Queue.t = Queue.create () let queue work = Queue.add work q let yield () = trace_depth := 0; try Queue.take q () with Trap (at, msg) -> Printf.printf "%s: execution error, %s\n" (Source.string_of_region at) msg let rec run () = if not (Queue.is_empty q) then (yield (); run ()) end

That would need fixing first (separately from this), for your try with to make any difference.
Sorry about the distraction...

crusso · 2019-06-17T13:36:14Z

src/as_values/prim.ml


 let prim = function
  | "abs" -> fun v k -> k (Int (Nat.abs (as_int v)))

+  | "Nat8->Word8" -> fun v k ->


I wonder if there's enough uniformity in all these conversions that you could refactor them into a uses of a few single higher order function that takes Numeric modules are arguments. Probably not worth it now you've completed but maybe as a future refactoring...

We'd need some sparring on how to use first-class modules, but yeah I was thinking of that. Unfortunately the primitives are not totally homogenous (some details differ). Also the NumType and WordType modules don't have all the methods that we need for interpretation and compilation, so a new functor would be needed. We should re-eval this cleanup idea for v1.0.

That's fine - also, it's not like were going to add more fixed width types in the foreseeable future...

Meta NIT: first-order -> first-class.

Of course. Fixed comment above.

crusso · 2019-06-17T13:39:05Z

src/as_values/value.ml

+
+  include Rep
+  let neg a = let res = Rep.neg a in check res
+  let abs a = let res = Rep.abs a in check res


Since you've implemented all the binary interpretations in value.ml, I wonder if we should just implement the binary operators for AS - or is there much more work in the compiler to do this?
Again, as a separate PR, I'd think

Should be mostly straight-forward, as most arithmetic (8-32 width) can be performed in 64 bits and checked for overflow. pow and mul are trickier, but I know how to check for a fast-path.

I prefer to hand this work over to the IDL community, so they can integrate it, while (me) working on the backend operations in parallel.

crusso · 2019-06-17T13:50:03Z

src/as_frontend/typing.ml

@@ -411,7 +448,7 @@ and infer_exp'' env exp : T.typ =
  | UnE (ot, op, exp1) ->
    let t1 = infer_exp_promote env exp1 in
    (* Special case for subtyping *)
-    let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in
+    let t = special_unop_typing t1 in
    if not env.pre then begin
      assert (!ot = Type.Pre);


I'd be very tempted to changed the syntax type checker to annotate BinE and UnE with the partially evaluated interpretations of the operators, so we don't have to repeat dispatch every time we call an operator... Whadday think? Again, this would be as a separate PR...

Not sure if I like code-in-the-data here. Would cause problems for pretty-printing, or serialization/deserialization. Also, smells a bit of premature optimization. Show me profiling data before you argue about performance :-)

@nomeata Not sure I buy that. The pretty printer can ignore it, serializer and deserialized drop and recompute from the type stored in ot. And I really don't think I need a profiler to tell me that doing redundant work (think of interpreted arithmetic in a loop) is a bad idea.

Plus, it would be more true to the intention that operators are resolved statically, not at runtime. Indeed, weren't you arguing for this in the past? But true, none of that should be part of this PR....

crusso · 2019-06-17T13:55:57Z

src/interpreter/interpret.ml

-    interpret_exp env exp1 (fun v1 -> k (Operator.unop !ot op v1))
+    interpret_exp env exp1
+      (fun v1 ->
+        k (try Operator.unop !ot op v1 with Invalid_argument s -> trap exp.at "%s" s))


For that separate PR I alluded to, it's a shame that we repeatedly resolve operators at application. We could instead store the resolved operation once as an additional field in ot during type-checking and just directly use it during interpretation... In fact, if resolution took a regions as an argument you also partially evaluate the source location too, removing the need for the try with here...

I assume, by "resolution" you mean the worker Operator.unop ? Then yes, passing the srcloc to it makes a lot of sense.

crusso · 2019-06-17T13:57:00Z

src/ir_interpreter/interpret_ir.ml

+        let call_conv, f = V.as_func v1 in
+        check_call_conv exp1 call_conv;
+        check_call_conv_arg env exp v2 call_conv;
+        last_region := exp.at; (* in case the following throws *)


I see why your are object now, since we don't even have a stack of regions, you need to reset the region here. Yuck, but I still think it's ok for now.

EPARSE :-)

Err, I don't get the reference...

I see why your are object now

My completion list for this:

"I see why you are objecting now"

"I see your objective now"

both don't really make sense to me in the context. Maybe you can explain?

Sorry, I meant "I see why you are objecting now, ..."

nomeata

Just looked at compile.ml

test/fail/outrange-nat64.as

src/codegen/compile.ml

ggreif · 2019-06-17T15:09:29Z

@crusso you requested changes, but I am not sure I can distill what exactly. I guess rewrite asc in Haskell was not it :-)

crusso · 2019-06-17T17:17:58Z

Well, I wanted you to remove the try with if possible (and wait for Joachim's review).

crusso

I'm approving (pending Joachim's approval).

nomeata

LGTM as well

src/codegen/compile.ml

I don't think allowing the non-canonical range in `Word*` patterns is a good idea, so I have not enabled them in `desugar.ml`.

src/codegen/compile.ml

ggreif · 2019-06-18T10:08:08Z

src/codegen/compile.ml

@@ -5132,6 +5132,48 @@ and compile_lit_pat env l =
  | (NatLit _ | IntLit _) ->
    compile_lit_as env SR.Vanilla l ^^
    BigNum.compile_eq env
+  | Nat8Lit _ ->
+    snd (compile_lit env l) ^^


I see no point spelling out the SR for compile_lit_as all the time, instead I rely on what is done by both lines below implicitly. Also there is no guarantee that the latter operates on Vanilla (other than inspecting the implementation).

ggreif · 2019-06-18T10:08:54Z

src/codegen/compile.ml

+    BoxedWord.unbox env ^^
+    snd (compile_lit env l) ^^
+    compile_eq env Type.(Prim Int64)
+  | Word8Lit _ ->


Words were an earlier omission, filled in now.

ggreif · 2019-06-18T10:10:56Z

src/codegen/compile.ml

+    snd (compile_lit env l) ^^
+    compile_eq env Type.(Prim Int16)
+  | Int32Lit _ ->
+    BoxedSmallWord.unbox env ^^


Since the scrutinee is captured as SR.Vanilla we need to unbox it for *32 and *64 prim types.

src/codegen/compile.ml

and other review feedback

I am convinced now that they are not needed. For the 8/16/32 bit types the OCaml `int32` provides the correct shift semantics and conversion from `int`. `int` OTOH has enough bits to represent the occurring ranges, negatives including.

ggreif added 12 commits June 4, 2019 19:37

add finite-bitwidth integral primitive types

9609c1e

WIP: compiles

ad41b0b

WIP: more progress

4637882

and a `Nat` bugfix

WIP: first round of backed changes

a9fb7a3

More conversions

1a42bce

- backend: all done -interpreter: `->Nat*` and `->Int*` mostly missing

WIP: added WordN->NatN/IntN

b710aa4

word32ToNat32 3000000000; crashes word64ToNat64 300000000000000000; probably crashes

refactor tests

e0e3dcf

implement and test Nat->Nat32 and Int->Int32

1e59f40

and other roundtrip tests

implement Nat->Nat* and Int->Int*

324e416

add range tests

fix Word32->Nat32

8c0fec8

soup up roundtrip tests

4ba1823

fix roundtrip bug

77c4693

ggreif changed the title Range restricted Nat* and Int* AST-89 Range restricted Nat* and Int* Jun 7, 2019

ggreif added 11 commits June 8, 2019 17:06

serialisation support

6dbc868

compile literals

bdc2d91

and fix msb_adjust for Int/Nat -> IntN/NatN

New primitive types for emacs mode (AST-89)

34f8a8e

fix conversions (i.e. boxing)

656e268

test Int/Nat16/32 serialisation

e83eca6

still needs Int/Nat8/64!

trap for outrange Nat->Nat8/16/32

e8a5240

range check for Int->Int8/16/32

664c798

caveat: when using libTomMath binding these fail: - intToInt8 (-128) - intToInt16 (-32768) -intToInt32 (-2147483648) The reason is that `fits_signed_bits` is buggy. (BigNum64 module works in this respect.)

cope with libTomMath flaw for now

18dd7a9

range check for ->Nat64

e8ebf62

resolved

76dc485

range check for ->Int64

15f798b

relaxing the fits_signed_bits contract to work with 64

ggreif force-pushed the gabor/ranged-int-nat branch from 393e979 to 15f798b Compare June 11, 2019 11:26

ggreif added 5 commits June 11, 2019 16:24

factor out special_unop_typing

53652f2

extend special_unop_typing to other Nat* types too

921a8ac

Merge remote-tracking branch 'origin/master' into gabor/ranged-int-nat

93c4f20

fix func import oversight

e324f85

update ok files

74be50d

ggreif added 2 commits June 17, 2019 11:23

revert the ability to negate Nat{8,16,32,64} and get an Int{8,16,32,64}

a5afc38

tweaks

ce7b7a7

ggreif marked this pull request as ready for review June 17, 2019 12:20

crusso reviewed Jun 17, 2019

View reviewed changes

src/interpreter/interpret.ml Show resolved Hide resolved

crusso requested changes Jun 17, 2019

View reviewed changes

nomeata reviewed Jun 17, 2019

View reviewed changes

handle a few review comments

032a91e

crusso approved these changes Jun 17, 2019

View reviewed changes

ggreif added 2 commits June 17, 2019 20:03

more review feedback

129ca99

more review feedback

bbbda66

nomeata approved these changes Jun 18, 2019

View reviewed changes

src/codegen/compile.ml Outdated Show resolved Hide resolved

ggreif added 2 commits June 18, 2019 09:45

implement ordering relation(s)

f5d8987

minor tweaks, doc fixes and codegen optimisations

1ded795

ggreif commented Jun 18, 2019

View reviewed changes

src/codegen/compile.ml Show resolved Hide resolved

ggreif added 2 commits June 18, 2019 11:32

fix build

de4e053

pattern matching {Word,Int,Nat}x{8,16,32,64}

eafa524

I don't think allowing the non-canonical range in `Word*` patterns is a good idea, so I have not enabled them in `desugar.ml`.

nomeata reviewed Jun 18, 2019

View reviewed changes

src/codegen/compile.ml Show resolved Hide resolved

ggreif commented Jun 18, 2019

View reviewed changes

nomeata reviewed Jun 18, 2019

View reviewed changes

src/codegen/compile.ml Outdated Show resolved Hide resolved

src/codegen/compile.ml Show resolved Hide resolved

ggreif added 3 commits June 18, 2019 12:54

rename BoxedWord64

789f1f9

and other review feedback

remove FIXMEs

2fe00c8

I am convinced now that they are not needed. For the 8/16/32 bit types the OCaml `int32` provides the correct shift semantics and conversion from `int`. `int` OTOH has enough bits to represent the occurring ranges, negatives including.

factor out the type-dependent creation of UnboxedSmallWord literals

8f45485

ggreif merged commit 1e1757a into master Jun 18, 2019

ggreif deleted the gabor/ranged-int-nat branch June 18, 2019 18:02

This was referenced Jun 18, 2019

allow (-128 : Int8) #505

Closed

Trapping in the interpreter is hacky #506

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

AST-89 Range restricted Nat* and Int* #487

AST-89 Range restricted Nat* and Int* #487

ggreif commented Jun 7, 2019 •

edited

Loading

crusso left a comment

crusso Jun 17, 2019

ggreif Jun 17, 2019

crusso Jun 17, 2019

crusso Jun 17, 2019

crusso Jun 17, 2019

ggreif Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019

ggreif Jun 17, 2019

crusso Jun 17, 2019

ggreif Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019

nomeata Jun 17, 2019

crusso Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019

ggreif Jun 18, 2019 •

edited

Loading

crusso Jun 17, 2019

ggreif Jun 17, 2019

crusso Jun 17, 2019

ggreif Jun 17, 2019

crusso Jun 17, 2019

nomeata left a comment

ggreif commented Jun 17, 2019

crusso commented Jun 17, 2019 •

edited

Loading

crusso left a comment

nomeata left a comment

ggreif Jun 18, 2019

ggreif Jun 18, 2019

ggreif Jun 18, 2019

AST-89 Range restricted Nat* and Int* #487

AST-89 Range restricted Nat* and Int* #487

Conversation

ggreif commented Jun 7, 2019 • edited Loading

crusso left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ggreif Jun 17, 2019 • edited Loading

Choose a reason for hiding this comment

crusso Jun 17, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ggreif Jun 17, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

crusso Jun 17, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ggreif Jun 18, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nomeata left a comment

Choose a reason for hiding this comment

ggreif commented Jun 17, 2019

crusso commented Jun 17, 2019 • edited Loading

crusso left a comment

Choose a reason for hiding this comment

nomeata left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ggreif commented Jun 7, 2019 •

edited

Loading

ggreif Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019 •

edited

Loading

ggreif Jun 17, 2019 •

edited

Loading

crusso Jun 17, 2019 •

edited

Loading

ggreif Jun 18, 2019 •

edited

Loading

crusso commented Jun 17, 2019 •

edited

Loading