Handle layout generation for split sub blocks correctly and for JUMP …

…instructions

src/liveness/layout_generation.py

@@ -30,7 +30,21 @@ def output_stack_layout(input_stack: List[str], final_stack_elements: List[str],
 
     # We keep the variables in the input stack in the same order if they appear in the variable vars (so that we
     # don't need to move them elsewhere). It might contain None variables if the corresponding variables are consumed
-    output_stack = final_stack_elements + [var_ if var_ in live_vars and var_ not in final_stack_elements else None for var_ in input_stack]
+    # Variables can appear repeated in the input stack due to splitting in several instructions. Hence, we just want
+    # to keep a copy of each variable, the one that is deepest in the stack.
+    reversed_stack_relative_order = []
+    already_introduced = set()
+    for var_ in reversed(input_stack):
+        if var_ in live_vars and var_ not in already_introduced:
+            reversed_stack_relative_order.append(var_)
+            already_introduced.add(var_)
+        else:
+            reversed_stack_relative_order.append(None)
+
+    # We undo the reversed traversal
+    relative_order = list(reversed(reversed_stack_relative_order))
+
+    output_stack = final_stack_elements + relative_order
     vars_to_place = live_vars.difference(set(output_stack))
 
     # Sort the vars to place according to the variable depth info order in reversed order

src/parser/cfg_block.py

@@ -427,10 +427,14 @@ def _build_spec_for_sequence(self, instructions, map_instructions: Dict, out_idx
                     pos = uninter["inpt_sk"].index(out_var)
                     uninter["inpt_sk"][pos] = new_out_var
 
+        # As JUMP instructions are not considered as part of the SFS, we must remove the corresponding values
+        # from the final stack
+        final_stack_bef_jump = (jump_instr.get_in_args() if jump_instr is not None else []) + final_stack
+
         # If there is a bottom value in the final stack, then we introduce it as part of the assignments and
         # then we pop it. Same for constant values in the final stack
         assignments_out_to_remove = set()
-        for stack_value in final_stack:
+        for stack_value in final_stack_bef_jump:
             if stack_value == "bottom" or stack_value.startswith("0x"):
                 self.assignment_dict[stack_value] = "0x00" if stack_value == "bottom" else stack_value
                 assignments_out_to_remove.add(stack_value)
@@ -472,7 +476,7 @@ def _build_spec_for_sequence(self, instructions, map_instructions: Dict, out_idx
 
         # Some of the final stack values can correspond to constant values already assigned, so we need to
         # unify the format with the corresponding representative stack variable
-        spec["tgt_ws"] = [assignment2stack_var.get(stack_value, stack_value) for stack_value in final_stack]
+        spec["tgt_ws"] = [assignment2stack_var.get(stack_value, stack_value) for stack_value in final_stack_bef_jump]
 
         spec["user_instrs"] = uninter_functions
         spec["variables"] = self._get_vars_spec(uninter_functions)