[herd] Asl bool condition

[maranget]

The choice operator of the "concurrent" ASL interpreted now assigns unresolved condition to TRUE or FALSE depending on the selected branch.

As a result the "SomeBoolean" primitive can now reduce to a simple non-resolved variable and could have been replaced by the construct UNKNOWN : boolean. Typically the following running herd7 on the following test will result in two outcomes with values 0 and 1 for x. Moreover the final values of b are FALSE and TRUE, respectively.

ASL U
{}

func main() => integer
begin
  var x = 0;
  let b = UNKNOWN : boolean;
  if b then
    x = 1;
  end
  return 0;
end

locations [0:main.0.x;]

Previously, the same result could be achieved by adding option -variant ASL or by replacing the UNKNOWN expression by a primitive call SomeBoolean ().

Unfortunately this "complete" resolution does not succeed in general. See the example herd/tests/instructions/ASL/unknown-integer.litmus for instance.

[HadrienRenaud]

Hi Luc,

Thank you very much for this, this is very interesting.

This looks great to me.

I am wondering if we could write can_predict_from in ASL as the following:

func can_predict_from (a: integer, b: integer) => integer
begin
  return
    if a != b then a
    else
      if UNKNOWN: boolean then a
      else b;
end

[maranget]

Hi @HadrienRenaud, if you could write it with SomeBoolean() before, it would work...