Fix edge case for STL bit string termination

Since the RLO is only modeled implicitly, changing a value that was
pushed on the RLO previously modifies the RLO post hoc. This fix should
allow for correct results when a value that contributes to the RLO is
modified.

Author: MatWise

src/statement-list/statement_list_typecheck.cpp

@@ -33,6 +33,8 @@ Author: Matthias Weiss, [email protected]
 #define CPROVER_ASSERT "\"" CPROVER_PREFIX "assert\""
 /// Name of the CBMC assume function.
 #define CPROVER_ASSUME "\"" CPROVER_PREFIX "assume\""
+/// Name of the RLO symbol used in some operations.
+#define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
 
 /// Creates the artificial data block parameter with a generic name and the
 /// specified type.
@@ -94,6 +96,8 @@ void statement_list_typecheckt::typecheck()
       parse_tree.function_blocks)
     typecheck_function_block_declaration(fb);
   typecheck_tag_list();
+  // Temporary RLO symbol for certain operations.
+  add_temp_rlo();
 
   // Iterate through all networks to generate the function bodies.
   for(const statement_list_parse_treet::function_blockt &fb :
@@ -197,6 +201,19 @@ void statement_list_typecheckt::typecheck_tag_list()
   }
 }
 
+void statement_list_typecheckt::add_temp_rlo()
+{
+  symbolt temp_rlo;
+  temp_rlo.is_static_lifetime = true;
+  temp_rlo.module = module;
+  temp_rlo.name = CPROVER_TEMP_RLO;
+  temp_rlo.base_name = temp_rlo.name;
+  temp_rlo.pretty_name = temp_rlo.name;
+  temp_rlo.type = get_bool_type();
+  temp_rlo.mode = ID_statement_list;
+  symbol_table.add(temp_rlo);
+}
+
 struct_typet statement_list_typecheckt::create_instance_data_block_type(
   const statement_list_parse_treet::function_blockt &function_block)
 {
@@ -1001,6 +1018,9 @@ void statement_list_typecheckt::typecheck_statement_list_assign(
   tia_element.value.add_to_operands(assignment);
   fc_bit = false;
   or_bit = false;
+  // Set RLO to assigned operand in order to prevent false results if a symbol
+  // that's implicitly part of the RLO was changed by the assignment.
+  rlo_bit = lhs;
 }
 
 void statement_list_typecheckt::typecheck_statement_list_set_rlo(
@@ -1027,6 +1047,9 @@ void statement_list_typecheckt::typecheck_statement_list_set(
 {
   const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)};
   const irep_idt &identifier{op.get_identifier()};
+
+  save_rlo_state(tia_element);
+
   const exprt lhs{typecheck_identifier(tia_element, identifier)};
   const code_assignt assignment{lhs, true_exprt()};
   const code_ifthenelset ifthen{rlo_bit, assignment};
@@ -1041,6 +1064,9 @@ void statement_list_typecheckt::typecheck_statement_list_reset(
 {
   const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)};
   const irep_idt &identifier{op.get_identifier()};
+
+  save_rlo_state(tia_element);
+
   const exprt lhs{typecheck_identifier(tia_element, identifier)};
   const code_assignt assignment{lhs, false_exprt()};
   const code_ifthenelset ifthen{rlo_bit, assignment};
@@ -1480,3 +1506,12 @@ void statement_list_typecheckt::initialize_bit_expression(const exprt &op)
   or_bit = false;
   rlo_bit = op;
 }
+
+void statement_list_typecheckt::save_rlo_state(symbolt &tia_element)
+{
+  symbol_exprt temp_rlo{
+    symbol_table.get_writeable_ref(CPROVER_TEMP_RLO).symbol_expr()};
+  const code_assignt rlo_assignment{temp_rlo, rlo_bit};
+  tia_element.value.add_to_operands(rlo_assignment);
+  rlo_bit = temp_rlo;
+}

src/statement-list/statement_list_typecheck.h

@@ -129,6 +129,10 @@ class statement_list_typecheckt : public typecheckt
   /// adds symbols for its contents to the symbol table.
   void typecheck_tag_list();
 
+  /// Adds a symbol for the RLO to the symbol table. This symbol is used by
+  /// other operations to save intermediate results of the rlo expression.
+  void add_temp_rlo();
+
   /// Creates a data block type for the given function block.
   /// \param function_block: Function block with an interface that should be
   /// converted to a data block.
@@ -624,6 +628,11 @@ class statement_list_typecheckt : public typecheckt
   /// instruction was encontered.
   /// \param op: Operand of the encountered instruction.
   void initialize_bit_expression(const exprt &op);
+
+  /// Saves the current RLO bit to a temporary variable to prevent false
+  /// overrides when modifying boolean variables.
+  /// \param tia_element: Symbol representation of the TIA element.
+  void save_rlo_state(symbolt &tia_element);
 };
 
 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H