Merge branch 'feature/subtle-nontail-fail' into 'dev'

Support always-failing conditionals

Closes #119

See merge request ligolang/ligo!311

src/bin/expect_tests/contract_tests.ml

@@ -1012,3 +1012,27 @@ let%expect_test _ =
 let%expect_test _ =
     run_ligo_good [ "dry-run" ; contract "double_main.ligo" ; "main" ; "unit" ; "0" ] ;
     [%expect {|( [] , 2 ) |}]
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; contract "subtle_nontail_fail.mligo" ; "main" ] ;
+  [%expect {|
+    { parameter unit ;
+      storage unit ;
+      code { PUSH bool True ;
+             IF { PUSH string "This contract always fails" ; FAILWITH }
+                { PUSH string "This contract still always fails" ; FAILWITH } } } |}]
+
+let%expect_test _ =
+  (* TODO should not be bad? *)
+  run_ligo_bad [ "dry-run" ; contract "subtle_nontail_fail.mligo" ; "main" ; "()" ; "()" ] ;
+  [%expect {|
+    ligo: error of execution
+
+     If you're not sure how to fix this error, you can
+     do one of the following:
+
+    * Visit our documentation: https://ligolang.org/docs/intro/what-and-why/
+    * Ask a question on our Discord: https://discord.gg/9rhYaEt
+    * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new
+    * Check the changelog by running 'ligo changelog' |}]
+

src/main/run/of_michelson.ml

@@ -103,7 +103,7 @@ let run_contract ?options (exp:Michelson.t) (exp_type:ex_ty) (input_michelson:Mi
   let exp = Michelson.strip_annots exp in
   let%bind descr =
     Trace.trace_tzresult_lwt (simple_error "error parsing program code") @@
-    Memory_proto_alpha.parse_michelson ~top_level exp ty_stack_before ty_stack_after in
+    Memory_proto_alpha.parse_michelson_fail ~top_level exp ty_stack_before ty_stack_after in
   let open! Memory_proto_alpha.Protocol.Script_interpreter in
   let%bind (Item(output, Empty)) =
     Trace.trace_tzresult_lwt (simple_error "error of execution") @@
@@ -120,7 +120,7 @@ let run_expression ?options (exp:Michelson.t) (exp_type:ex_ty) : run_res result
   and ty_stack_after = Script_typed_ir.Item_t (exp_type', Empty_t, None) in
   let%bind descr =
     Trace.trace_tzresult_lwt (simple_error "error parsing program code") @@
-    Memory_proto_alpha.parse_michelson ~top_level exp ty_stack_before ty_stack_after in
+    Memory_proto_alpha.parse_michelson_fail ~top_level exp ty_stack_before ty_stack_after in
   let open! Memory_proto_alpha.Protocol.Script_interpreter in
   let%bind res =
     Trace.trace_tzresult_lwt (simple_error "error of execution") @@

src/passes/9-self_michelson/self_michelson.ml

@@ -359,13 +359,30 @@ let opt_swap2 : peep2 = function
    thwarting the intent of the Michelson tail fail restriction -- the
    LIGO _user_ might accidentally write dead code immediately after a
    failure, and we will simply erase it. *)
+let rec is_failing : michelson -> bool =
+  function
+  | Seq (_, []) -> false
+  | Seq (_, [arg]) -> is_failing arg
+  | Seq (l, _ :: args) -> is_failing (Seq (l, args))
+  | Prim (_, I_FAILWITH, _, _) -> true
+  | Prim (_, I_IF, [bt; bf], _)
+  | Prim (_, I_IF_CONS, [bt; bf], _)
+  | Prim (_, I_IF_LEFT, [bt; bf], _)
+  | Prim (_, I_IF_NONE, [bt; bf], _) ->
+    is_failing bt && is_failing bf
+  (* Note: the body of ITER, LOOP, LOOP_LEFT _can_ be
+     failing. However, the loop will _not_ be failing, because the
+     body might never be executed. The body of MAP _cannot_ be
+     failing. *)
+  | _ -> false
+
 let rec opt_tail_fail : michelson -> michelson =
   function
   | Seq (l, args) ->
      let rec aux args =
        match args with
        | [] -> []
-       | Prim (l, I_FAILWITH, args, annot) :: _ -> [ Prim (l, I_FAILWITH, args, annot) ]
+       | arg :: _ when is_failing arg -> [arg]
        | arg :: args -> arg :: aux args in
      let args = aux args in
      Seq (l, List.map opt_tail_fail args)

src/test/contracts/subtle_nontail_fail.mligo

@@ -0,0 +1,4 @@
+let main (ps : unit * unit) =
+  if true
+  then failwith "This contract always fails"
+  else failwith "This contract still always fails"