herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
215 stars 54 forks source link

[asl] Fix let binding of tuples #867

Closed maranget closed 2 months ago

maranget commented 2 months ago

Fix various problems related to tuple bindings.

Two tests that illustrate the fixed problems are also added.

{

}

func f() => (integer, integer) begin return (1,2); end

func main() => integer begin let (a,b) = f(); let c = a+b; return 0; end

forall 0:main.0.c=3

Before the fix, this test yielded no execution at all, because if the cyclic `po` introduced while evaluating `let (a,b) = f();`.
- Creating tuples with non-resolved arguments:

ASL frozen-tuple-arg

{ x=15; 0:X0=x; }

func main() => integer begin let x = read_register(0);
let (a,b) = (1,UInt(read_memory(x,32))); let c = a+b; return 0; end

forall 0:main.0.c=16


Before the fix, evaluation of `let (a,b) = (1,UInt(read_memory(x,32)));` was failing because the `read_memory` primitive returns a non-resolved value, resulting in a pair whose second argument is a non-resolved value.
HadrienRenaud commented 2 months ago

Sounds good to me, thank you @maranget for this in depth bug finding

maranget commented 2 months ago

Merged, thanks @HadrienRenaud forthe review.