The following rule crashed because of invalid generated stratego code

TypeConversion(op, operand, typ):-
where (
        typ => Int(width)
        and (op => Fptoui() or op => Fptosi())
        and operand: operandt
        and operandt == Float()
        else error $[Expected float, got [operandt]] on operand
  ) or (
        typ => Vector(length, Int(x))
        and operand: operandt
        and operandt == Vector(length, Float())
       else error $[Expected vector of floats, got [operandt]] on operand
  ) else error $[[op] targets (vectors of) signed integer types, got [typ]] on typ

It seems that using the name operandt twice seems to mess things up (using operandt2 instead, compiles).
(in my case I actually did not want them to be equal, so that fitted as a solution)

The generated stratego code looks like this (most important here is that operandt is defined at the end, and used before that point.

nabl-constraint(|ctx) :
  TypeConversion(op, operand, typ) -> <fail>
  where 
    width := <new-task(|ctx)> Rewrite("proj323", typ);
    eq594 := <type-match(|ctx, Fptoui()); task-create-id(|ctx, [width])> op;
    eq595 := <type-match(|ctx, Fptosi()); task-create-id(|ctx, [width])> op;
    or61 := <type-is(|ctx)> <task-create-choice(|ctx)> [eq594, eq595];
    operandt64 := <type-task(|ctx); task-create-id(|ctx, [or61])> operand;
    eq596 := <type-match(|ctx, Float()); task-create-id(|ctx, [operandt64])> operandt;
    <task-create-error-on-failure(|ctx, eq596, ["Expected float, got ", operandt])> operand;
    length := <new-task(|ctx)> Rewrite("proj324", typ);
    x := <new-task(|ctx)> Rewrite("proj325", typ); task-create-id(|ctx, [length]);
    operandt65 := <type-task(|ctx); task-create-id(|ctx, [x])> operand;
    eq597 := <type-match(|ctx, Vector(length, Float())); task-create-id(|ctx, [operandt65])> operandt;
    <task-create-error-on-failure(|ctx, eq597, ["Expected vector of floats, got ", operandt])> operand;
    <task-create-error-on-failure(|ctx, eq597, [op, " targets (vectors of) signed integer types, got ", typ])> typ;
    or62 := <type-is(|ctx)> <task-create-choice(|ctx)> [eq596, eq597];
    operandt := <type-is(|ctx); task-create-id(|ctx, [or62])> <task-create-choice(|ctx)> [operandt64, operandt65]
Submitted by Arjen on 13 May 2014 at 18:31

On 15 May 2014 at 14:38 Eelco Visser commented:

fixed (in github)


On 15 May 2014 at 14:38 Eelco Visser closed this issue.

On 24 July 2014 at 17:32 Augusto commented:

Has this actually been fixed? The exemplified generated rule seems to indicate NaBL code, but the bug report title indicates TS.

There are two different issues I keep getting. The following silly example may exemplify the issue better (ignore the non-sensical semantics, just focus on the actual generated code):

Abs(p,e): Arr(Tf,Tr)
where e : Tr
  and p : Tf
   or (
       p : Arr(S1,S2)
       and S1 == S2
   ) or (
       p : Arr(S1,S2)
       and S1 == S2
   )

This generates the following:

create-type-task(|ctx) :
Abs(p, e) -> <task-create-id(|ctx,[x20])> x20
where 
  Tr := <type-task(|ctx)> e;
  Tf := <type-task(|ctx); task-create-id(|ctx, [Tr])> p;
  x18 := <type-task(|ctx)> p;
  S12 := <new-task(|ctx)> Rewrite("proj10", x18); task-create-id(|ctx, [x18]);
  S22 := <new-task(|ctx)> Rewrite("proj11", x18); task-create-id(|ctx, [S12]);
  eq6 := <type-match(|ctx, S2); task-create-id(|ctx, [S22])> S1;
  or3 := <type-is(|ctx)> <task-create-choice(|ctx)> [Tf, eq6];
  x19 := <type-task(|ctx)> p;
  S13 := <new-task(|ctx)> Rewrite("proj12", x19); task-create-id(|ctx, [x19]);
  S23 := <new-task(|ctx)> Rewrite("proj13", x19); task-create-id(|ctx, [S13]);
  eq7 := <type-match(|ctx, S2); task-create-id(|ctx, [S23])> S1;
  or4 := <type-is(|ctx)> <task-create-choice(|ctx)> [or3, eq7];
  S1 := <type-is(|ctx); task-create-id(|ctx, [or4])> <task-create-choice(|ctx)> [S12, S13];
  S2 := <type-is(|ctx); task-create-id(|ctx, [S1])> <task-create-choice(|ctx)> [S22, S23];
  x20 := <type-is(|ctx); task-create-id(|ctx, [S2])> Arr(Tf, Tr)

Note how both eq6 and eq7 refer to S1 and S2 even though those are only generated later. Not only that, but they are using the same (instead of S1[2-3] and S2[2-3]).

The same issue happened in relation rules and constraints (:-, like above).
I believe this bug needs to be reopened or refiled.

Log in to post comments