[asl] Fix unsound controlflow analysis for try .. catch

asllib/Typing.ml

@@ -3419,7 +3419,17 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
       | S_Cond (_, s1, s2) -> join (from_stmt s1) (from_stmt s2)
       | S_Repeat (body, _, _) -> from_stmt body
       | S_While _ | S_For _ -> MayNotInterrupt
-      | S_Try (body, _, _) -> from_stmt body
+      | S_Try (body, catchers, otherwise) ->
+          let res0 = from_stmt body in
+          let res1 =
+            match otherwise with
+            | None -> res0
+            | Some s -> join (from_stmt s) res0
+          in
+          List.fold_left
+            (fun res (_, _, s) -> join res (from_stmt s))
+            res1 catchers
+
     (* End *)
 
     (** [check_stmt_interrupts name env body] checks that the function named

asllib/tests/control-flow.t/run.t

@@ -26,3 +26,29 @@
   File if-return-if.asl, line 3, character 2 to line 5, character 6:
   ASL Typing error: function "sign" does not return anything.
   [1]
+
+  $ aslref try-00.asl
+
+  $ aslref try-01.asl
+  File try-01.asl, line 5, character 2 to line 6, character 41:
+  ASL Typing error: function "test0" does not return anything.
+  [1]
+
+  $ aslref try-02.asl
+
+  $ aslref try-03.asl
+
+  $ aslref try-04.asl
+  File try-04.asl, line 5, character 2 to line 9, character 6:
+  ASL Typing error: function "test0" does not return anything.
+  [1]
+
+  $ aslref try-05.asl
+  File try-05.asl, line 6, character 2 to line 11, character 6:
+  ASL Typing error: function "test0" does not return anything.
+  [1]
+
+  $ aslref try-06.asl
+  File try-06.asl, line 5, character 2 to line 9, character 6:
+  ASL Typing error: function "test0" does not return anything.
+  [1]

asllib/tests/control-flow.t/try-00.asl

@@ -0,0 +1,15 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try return 0;
+  catch when E => return 1; end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-01.asl

@@ -0,0 +1,15 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try return 0;
+  catch when E => print("caught E"); end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-02.asl

@@ -0,0 +1,15 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try throw E {};
+  catch when E => return 1; end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 1;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-03.asl

@@ -0,0 +1,18 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try return 0;
+  catch
+    when E => return 1;
+    otherwise => throw E {};
+  end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-04.asl

@@ -0,0 +1,18 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try return 0;
+  catch
+    when E => return 1;
+    otherwise => println("Otherwise");
+  end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-05.asl

@@ -0,0 +1,20 @@
+type E of exception {};
+type F of exception {};
+
+func test0 () => integer
+begin
+  try throw E {};
+  catch
+    when E => return 1;
+    when F => println("Caught F");
+    otherwise => throw E {};
+  end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;

asllib/tests/control-flow.t/try-06.asl

@@ -0,0 +1,18 @@
+type E of exception {};
+
+func test0 () => integer
+begin
+  try print("body");
+  catch
+    when E => return 1;
+    otherwise => throw E {};
+  end;
+end;
+
+func main () => integer
+begin
+  let res = test0();
+  assert res == 0;
+
+  return 0;
+end;