herd / herdtools7

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

[asl] Fix the interpretation of the asl try statement. #902

Closed maranget closed 3 weeks ago

maranget commented 1 month ago

Fix for issue #899. Here is an inlined version of the problematic test:

ASL U1

{ }

type  Coucou of exception {};

func g(a:integer) => integer
begin
  try
    let b = SomeBoolean();
    if b then
      throw Coucou {};
    end
    return a+1;
  catch
    when Coucou =>
      return a+3;
  end

end
func main() => integer
begin
  let  x = g(0);
  return 0;
end

locations [0:main.0.x;]

Executing this test with the previous herd7 yields a fatal error due to the duplicated execution of the statement <S> from the try <S> catch construct.

% herd7  U1.litmus
Warning: Uncaught exception: Coucou {}

Namely, in the case when no exception is thrown, <S> is re-executed unprotected, resulting in an uncaught exception fault. See the first commit for details.

maranget commented 3 weeks ago

Thanks a lot Luc

This feels a bit obscure why those are different, but this looks very good to me thanks a lot

Hi @HadrienRenaud. Generally, values of monadic type should not be used more than once. Otherwise, it leads to repeated evaluation by the "concurrent" interpreter. The root cause of the problem solved by PR #867 was similar.

maranget commented 3 weeks ago

Merged, thanks for the review @HadrienRenaud.