Add conversion for rol and ror operators to c output

This adds conversion for the rol and ror operators from CBMC
internals into C code. This is done by bit-twiddling the values
to achieve the outcome.

Fixes #6241

Author: TGWDB

src/analyses/invariant_set_domain.cpp

@@ -50,11 +50,11 @@ void invariant_set_domaint::transform(
     }
     break;
 
-  case RETURN:
-    // ignore
-    break;
+    case RETURN:
+      // ignore
+      break;
 
-  case ASSIGN:
+    case ASSIGN:
     {
       const code_assignt &assignment = from_l->get_assign();
       invariant_set.assignment(assignment.lhs(), assignment.rhs());

src/ansi-c/expr2c.cpp

@@ -2290,6 +2290,71 @@ std::string expr2ct::convert_initializer_list(const exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_rox(const exprt &src, unsigned precedence)
+{
+  // AAAA rox n ==   (AAAA lhs_op n % width(AAAA))
+  //               | (AAAA rhs_op (width(AAAA) - n % width(AAAA)))
+  // Where lhs_op and rhs_op depend on whether it is rol or ror
+  // auto rotate_expr = to_binary_expr(src);
+  auto rotate_expr = expr_checked_cast<shift_exprt>(src);
+  // Get AAAA and if it's signed wrap it in a cast to remove
+  // the sign since this messes with C shifts
+  exprt &op0 = rotate_expr.op();
+  size_t type_width;
+  if(can_cast_type<signedbv_typet>(op0.type()))
+  {
+    // Set the type width
+    type_width = to_signedbv_type(op0.type()).get_width();
+    // Shifts in C are arithmetic and care about sign, by forcing
+    // a cast to unsigned we force the shifts to perform rol/r
+    op0 = typecast_exprt(op0, unsignedbv_typet(type_width));
+  }
+  else if(can_cast_type<unsignedbv_typet>(op0.type()))
+  {
+    // Set the type width
+    type_width = to_unsignedbv_type(op0.type()).get_width();
+  }
+  else
+  {
+    // Type that can't be represented as bitvector
+    // get some kind of width in a potentially unsafe way
+    type_width = op0.type().get_size_t("width");
+  }
+  // Construct the "width(AAAA)" constant
+  const exprt width_expr =
+    from_integer(type_width, rotate_expr.distance().type());
+  // Apply modulo to n since shifting will overflow
+  // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
+  const exprt distance_modulo_width =
+    mod_exprt(rotate_expr.distance(), width_expr);
+  // Now put the pieces together
+  // width(AAAA) - (n % width(AAAA))
+  const auto complement_expr = minus_exprt(width_expr, distance_modulo_width);
+  // lhs and rhs components defined according to rol/ror
+  exprt lhs_expr;
+  exprt rhs_expr;
+  if(src.id() == ID_rol)
+  {
+    // AAAA << (n % width(AAAA))
+    lhs_expr = shl_exprt(op0, distance_modulo_width);
+    // AAAA >> complement_expr
+    rhs_expr = ashr_exprt(op0, complement_expr);
+  }
+  else if(src.id() == ID_ror)
+  {
+    // AAAA >> (n % width(AAAA))
+    lhs_expr = ashr_exprt(op0, distance_modulo_width);
+    // AAAA << complement_expr
+    rhs_expr = shl_exprt(op0, complement_expr);
+  }
+  else
+  {
+    // Someone called this function when they shouldn't have.
+    UNREACHABLE;
+  }
+  return convert_with_precedence(bitor_exprt(lhs_expr, rhs_expr), precedence);
+}
+
 std::string expr2ct::convert_designated_initializer(const exprt &src)
 {
   if(src.operands().size()!=1)
@@ -3794,6 +3859,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id() == ID_rol || src.id() == ID_ror)
+    return convert_rox(src, precedence);
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;

src/ansi-c/expr2c_class.h

@@ -126,6 +126,15 @@ class expr2ct
     const std::string &symbol2,
     unsigned precedence);
 
+  /// Conversion function from rol/ror expressions to C code strings
+  /// Note that this constructs a complex expression to do bit
+  /// twiddling since rol/ror operations are not native to ANSI-C.
+  /// The complex expression is then recursively converted.
+  /// \param src: is an exprt that must be either an rol or ror
+  /// \param precedence: precedence for bracketing
+  /// \returns string for performing rol/ror as bit twiddling with C
+  std::string convert_rox(const exprt &src, unsigned precedence);
+
   std::string convert_overflow(
     const exprt &src, unsigned &precedence);
 

src/goto-instrument/dot.cpp

@@ -155,10 +155,8 @@ void dott::write_dot_subgraph(
         function_calls.push_back(
           std::pair<std::string, exprt>(ss.str(), function_call.function()));
       }
-      else if(it->is_assign() ||
-              it->is_decl() ||
-              it->is_return() ||
-              it->is_other())
+      else if(
+        it->is_assign() || it->is_decl() || it->is_return() || it->is_other())
       {
         std::string t = from_expr(ns, function_id, it->get_code());
         while(t[ t.size()-1 ]=='\n')

src/goto-instrument/function.cpp

@@ -142,14 +142,14 @@ void function_exit(
     assert(last->is_end_function());
 
     // is there already a return?
-    bool has_return=false;
+    bool has_return = false;
 
     if(last!=body.instructions.begin())
     {
       goto_programt::targett before_last=last;
       --before_last;
       if(before_last->is_return())
-        has_return=true;
+        has_return = true;
     }
 
     if(!has_return)

src/goto-instrument/wmm/goto2graph.cpp

@@ -1227,13 +1227,9 @@ void inline instrumentert::add_instr_to_interleaving(
   goto_programt::instructionst::iterator it,
   goto_programt &interleaving)
 {
-  if(it->is_return() ||
-     it->is_throw() ||
-     it->is_catch() ||
-     it->is_skip() ||
-     it->is_dead() ||
-     it->is_start_thread() ||
-     it->is_end_thread())
+  if(
+    it->is_return() || it->is_throw() || it->is_catch() || it->is_skip() ||
+    it->is_dead() || it->is_start_thread() || it->is_end_thread())
     return;
 
   if(it->is_atomic_begin() ||

src/goto-programs/goto_program.cpp

@@ -174,10 +174,8 @@ std::ostream &goto_programt::output_instruction(
     {
       const auto &landingpad = to_code_landingpad(instruction.get_code());
       out << "EXCEPTION LANDING PAD ("
-          << from_type(ns, identifier, landingpad.catch_expr().type())
-          << ' '
-          << from_expr(ns, identifier, landingpad.catch_expr())
-          << ")";
+          << from_type(ns, identifier, landingpad.catch_expr().type()) << ' '
+          << from_expr(ns, identifier, landingpad.catch_expr()) << ")";
     }
     else if(instruction.get_code().get_statement() == ID_push_catch)
     {

src/goto-programs/goto_program.h

@@ -467,24 +467,78 @@ class goto_programt
       type = GOTO;
     }
 
-    bool is_goto         () const { return type==GOTO;          }
-    bool is_return       () const { return type==RETURN;        }
-    bool is_assign       () const { return type==ASSIGN;        }
-    bool is_function_call() const { return type==FUNCTION_CALL; }
-    bool is_throw        () const { return type==THROW;         }
-    bool is_catch        () const { return type==CATCH;         }
-    bool is_skip         () const { return type==SKIP;          }
-    bool is_location     () const { return type==LOCATION;      }
-    bool is_other        () const { return type==OTHER;         }
-    bool is_decl         () const { return type==DECL;          }
-    bool is_dead         () const { return type==DEAD;          }
-    bool is_assume       () const { return type==ASSUME;        }
-    bool is_assert       () const { return type==ASSERT;        }
-    bool is_atomic_begin () const { return type==ATOMIC_BEGIN;  }
-    bool is_atomic_end   () const { return type==ATOMIC_END;    }
-    bool is_start_thread () const { return type==START_THREAD;  }
-    bool is_end_thread   () const { return type==END_THREAD;    }
-    bool is_end_function () const { return type==END_FUNCTION;  }
+    bool is_goto() const
+    {
+      return type == GOTO;
+    }
+    bool is_return() const
+    {
+      return type == RETURN;
+    }
+    bool is_assign() const
+    {
+      return type == ASSIGN;
+    }
+    bool is_function_call() const
+    {
+      return type == FUNCTION_CALL;
+    }
+    bool is_throw() const
+    {
+      return type == THROW;
+    }
+    bool is_catch() const
+    {
+      return type == CATCH;
+    }
+    bool is_skip() const
+    {
+      return type == SKIP;
+    }
+    bool is_location() const
+    {
+      return type == LOCATION;
+    }
+    bool is_other() const
+    {
+      return type == OTHER;
+    }
+    bool is_decl() const
+    {
+      return type == DECL;
+    }
+    bool is_dead() const
+    {
+      return type == DEAD;
+    }
+    bool is_assume() const
+    {
+      return type == ASSUME;
+    }
+    bool is_assert() const
+    {
+      return type == ASSERT;
+    }
+    bool is_atomic_begin() const
+    {
+      return type == ATOMIC_BEGIN;
+    }
+    bool is_atomic_end() const
+    {
+      return type == ATOMIC_END;
+    }
+    bool is_start_thread() const
+    {
+      return type == START_THREAD;
+    }
+    bool is_end_thread() const
+    {
+      return type == END_THREAD;
+    }
+    bool is_end_function() const
+    {
+      return type == END_FUNCTION;
+    }
     bool is_incomplete_goto() const
     {
       return type == INCOMPLETE_GOTO;

src/goto-programs/goto_trace.cpp

@@ -570,10 +570,10 @@ void show_full_goto_trace(
       break;
 
     case goto_trace_stept::typet::ASSIGNMENT:
-      if(step.pc->is_assign() ||
-         step.pc->is_return() || // returns have a lhs!
-         step.pc->is_function_call() ||
-         (step.pc->is_other() && step.full_lhs.is_not_nil()))
+      if(
+        step.pc->is_assign() || step.pc->is_return() || // returns have a lhs!
+        step.pc->is_function_call() ||
+        (step.pc->is_other() && step.full_lhs.is_not_nil()))
       {
         if(prev_step_nr!=step.step_nr || first_step)
         {