Improvement: Support all combinations of target and unwind action for function calls.

A specific case that was not supported was the function `std::process::exit`, which in some cases generates a cleanup block but no return block.

Besides, the new `match` considers all possibilities and handles the `Unreacheable` case where it was simply ignored before.

The new `match` statement cannot be moved to a separate function because of the divergent function case.

Author: hlisdero

examples/results/function_call/greet/net.dot

@@ -74,7 +74,7 @@ digraph petrinet {
     std_ops_Index_index_0_CALL_UNWIND [shape="box" xlabel="" label="std_ops_Index_index_0_CALL_UNWIND"];
     std_ops_Index_index_1_CALL [shape="box" xlabel="" label="std_ops_Index_index_1_CALL"];
     std_ops_Index_index_1_CALL_UNWIND [shape="box" xlabel="" label="std_ops_Index_index_1_CALL_UNWIND"];
-    std_process_exit_DIVERGING_CALL [shape="box" xlabel="" label="std_process_exit_DIVERGING_CALL"];
+    std_process_exit_0_CALL [shape="box" xlabel="" label="std_process_exit_0_CALL"];
     std_vec_Vec_T_A_len_0_CALL [shape="box" xlabel="" label="std_vec_Vec_T_A_len_0_CALL"];
     std_vec_Vec_T_A_len_0_CALL_UNWIND [shape="box" xlabel="" label="std_vec_Vec_T_A_len_0_CALL_UNWIND"];
     PROGRAM_START -> std_env_args_0_CALL;
@@ -116,7 +116,7 @@ digraph petrinet {
     main_BB6_STMT1_END -> main_BB6_STMT2;
     main_BB7 -> std_io__eprint_0_CALL;
     main_BB7 -> std_io__eprint_0_CALL_UNWIND;
-    main_BB8 -> std_process_exit_DIVERGING_CALL;
+    main_BB8 -> std_process_exit_0_CALL;
     main_BB9 -> main_BB9_STMT0;
     main_BB9_END_PLACE -> std_ops_Index_index_1_CALL;
     main_BB9_END_PLACE -> std_ops_Index_index_1_CALL_UNWIND;
@@ -160,6 +160,7 @@ digraph petrinet {
     std_ops_Index_index_0_CALL_UNWIND -> main_BB15;
     std_ops_Index_index_1_CALL -> main_BB10;
     std_ops_Index_index_1_CALL_UNWIND -> main_BB15;
+    std_process_exit_0_CALL -> main_BB15;
     std_vec_Vec_T_A_len_0_CALL -> main_BB3;
     std_vec_Vec_T_A_len_0_CALL_UNWIND -> main_BB15;
 }

examples/results/function_call/greet/net.lola

@@ -237,9 +237,11 @@ TRANSITION std_ops_Index_index_1_CALL_UNWIND
     main_BB9_END_PLACE : 1;
   PRODUCE
     main_BB15 : 1;
-TRANSITION std_process_exit_DIVERGING_CALL
+TRANSITION std_process_exit_0_CALL
   CONSUME
     main_BB8 : 1;
+  PRODUCE
+    main_BB15 : 1;
 TRANSITION std_vec_Vec_T_A_len_0_CALL
   CONSUME
     main_BB2_END_PLACE : 1;

examples/results/function_call/greet/net.pnml

@@ -380,9 +380,9 @@
           <text>std_ops_Index_index_1_CALL_UNWIND</text>
         </name>
       </transition>
-      <transition id="std_process_exit_DIVERGING_CALL">
+      <transition id="std_process_exit_0_CALL">
         <name>
-          <text>std_process_exit_DIVERGING_CALL</text>
+          <text>std_process_exit_0_CALL</text>
         </name>
       </transition>
       <transition id="std_vec_Vec_T_A_len_0_CALL">
@@ -707,9 +707,9 @@
           <text>1</text>
         </inscription>
       </arc>
-      <arc source="main_BB8" target="std_process_exit_DIVERGING_CALL" id="(main_BB8, std_process_exit_DIVERGING_CALL)">
+      <arc source="main_BB8" target="std_process_exit_0_CALL" id="(main_BB8, std_process_exit_0_CALL)">
         <name>
-          <text>(main_BB8, std_process_exit_DIVERGING_CALL)</text>
+          <text>(main_BB8, std_process_exit_0_CALL)</text>
         </name>
         <inscription>
           <text>1</text>
@@ -1059,6 +1059,14 @@
           <text>1</text>
         </inscription>
       </arc>
+      <arc source="std_process_exit_0_CALL" target="main_BB15" id="(std_process_exit_0_CALL, main_BB15)">
+        <name>
+          <text>(std_process_exit_0_CALL, main_BB15)</text>
+        </name>
+        <inscription>
+          <text>1</text>
+        </inscription>
+      </arc>
       <arc source="std_vec_Vec_T_A_len_0_CALL" target="main_BB3" id="(std_vec_Vec_T_A_len_0_CALL, main_BB3)">
         <name>
           <text>(std_vec_Vec_T_A_len_0_CALL, main_BB3)</text>

src/translator.rs

@@ -186,12 +186,12 @@ impl<'tcx> Translator<'tcx> {
         let function_def_id =
             extract_def_id_of_called_function_from_operand(func, current_function.def_id, self.tcx);
         let function_name = self.tcx.def_path_str(function_def_id);
+        let start_place = current_function.get_start_place_for_function_call();
         info!("Encountered function call: {function_name}");
 
         if is_panic_function(&function_name) {
             // Function call which starts an abnormal termination of the program.
             // Non-recursive call for the translation process.
-            let start_place = current_function.get_start_place_for_function_call();
             call_panic_function(
                 &start_place,
                 &self.program_panic,
@@ -201,22 +201,63 @@ impl<'tcx> Translator<'tcx> {
             return;
         }
 
-        let Some(return_block) = target else {
-            // Call to a function which does not return (Return type: -> !).
-            // Non-recursive call for the translation process.
-            let start_place = current_function.get_start_place_for_function_call();
-            call_diverging_function(&start_place, &function_name, &mut self.net);
-            return;
-        };
-
-        let start_place = current_function.get_start_place_for_function_call();
-        let end_place =
-            current_function.get_end_place_for_function_call(return_block, &mut self.net);
-        let cleanup_place = if let rustc_middle::mir::UnwindAction::Cleanup(cleanup_block) = unwind
-        {
-            Some(current_function.get_end_place_for_function_call(cleanup_block, &mut self.net))
-        } else {
-            None
+        // Depending on whether a return or a unwind for the function are present,
+        // we have different possibilities for the function call end place and the (optional) cleanup place.
+        let (end_place, cleanup_place) = match (target, unwind) {
+            (Some(return_block), rustc_middle::mir::UnwindAction::Continue) => {
+                // MIR function or foreign function calls without a cleanup block.
+                let end_place =
+                    current_function.get_end_place_for_function_call(return_block, &mut self.net);
+                (end_place, None)
+            }
+            (Some(return_block), rustc_middle::mir::UnwindAction::Cleanup(cleanup_block)) => {
+                // The usual foreign function call case.
+                let end_place =
+                    current_function.get_end_place_for_function_call(return_block, &mut self.net);
+                let cleanup_place =
+                    current_function.get_end_place_for_function_call(cleanup_block, &mut self.net);
+                (end_place, Some(cleanup_place))
+            }
+            (Some(return_block), rustc_middle::mir::UnwindAction::Terminate) => {
+                // Specific foreign function calls that terminate the program (abort).
+                let end_place =
+                    current_function.get_end_place_for_function_call(return_block, &mut self.net);
+                // Connect cleanup to panic place
+                (end_place, Some(self.program_panic.clone()))
+            }
+            (None, rustc_middle::mir::UnwindAction::Terminate) => {
+                // Foreign function calls that simply terminate the program.
+                (self.program_panic.clone(), None)
+            }
+            (None, rustc_middle::mir::UnwindAction::Cleanup(cleanup_block)) => {
+                // A very special case seen in functions like `std::process::exit`
+                // where the return block is actually expressed as a cleanup.
+                // This needs to be modelled differently than a diverging function.
+                let end_place =
+                    current_function.get_end_place_for_function_call(cleanup_block, &mut self.net);
+                (end_place, None)
+            }
+            (None, rustc_middle::mir::UnwindAction::Continue) => {
+                // Call to a function which does not return (Return type: -> !).
+                // Non-recursive call for the translation process.
+                call_diverging_function(&start_place, &function_name, &mut self.net);
+                return;
+            }
+            (Some(return_block), rustc_middle::mir::UnwindAction::Unreachable) => {
+                // Support the unreachable case simply by matching the cleanup place to the program end place.
+                // This is a compromise solution to avoid polluting the panic state with these extraneous states
+                // that are actually not reachable during execution.
+                let end_place =
+                    current_function.get_end_place_for_function_call(return_block, &mut self.net);
+                // Connect cleanup to program end place.
+                (end_place, Some(self.program_end.clone()))
+            }
+            (None, rustc_middle::mir::UnwindAction::Unreachable) => {
+                // Support the unreachable case simply by matching the cleanup place to the program end place.
+                // This is a compromise solution to avoid polluting the panic state with these extraneous states
+                // that are actually not reachable during execution.
+                (self.program_end.clone(), None)
+            }
         };
 
         let function_call = FunctionCall::new(function_def_id, self.tcx);