Expand expr2statement_list

Adds support for the conversion of boolean expressions. Note that this
will hardly have any effect on the output of CBMC and in the current
state only be used by projects which rely on it.

There are several STL-specific simplification routines integrated in the
conversion, e.g. changing the conversion order of operands to avoid
unnecessary nesting.

Author: MatWise

src/statement-list/converters/expr2statement_list.cpp

@@ -10,12 +10,52 @@ Author: Matthias Weiss, [email protected]
 
 #include <ansi-c/expr2c.h>
 
+#include <util/std_expr.h>
+#include <util/suffix.h>
+#include <util/symbol_table.h>
+
+#include <algorithm>
+
+/// STL code for an AND instruction.
+#define AND 'A'
+
+/// STL code for an OR instruction.
+#define OR 'O'
+
+/// STL code for a XOR instruction.
+#define XOR 'X'
+
+/// Postfix for any negated boolean instruction.
+#define NOT_POSTFIX 'N'
+
+/// STL code for a NOT instruction.
+#define NOT "NOT"
+
+/// Separator between the instruction code and it's operand.
+#define OPERAND_SEPARATOR ' '
+
+/// Separator between the end of an instruction and the next one.
+#define LINE_SEPARATOR ";\n"
+
+/// Separator for the end of an instruction that introduces a new layer of
+/// nesting.
+#define NESTING_OPEN_LINE_SEPARATOR "(;\n"
+
+/// Separator for the end of an instruction that closes a nesting layer. Also
+/// known as the NESTING CLOSED instruction.
+#define NESTING_CLOSED_LINE_SEPARATOR ");\n"
+
+/// Prefix for the reference to any variable.
+#define REFERENCE_FLAG '#'
+
+/// CBMC-internal separator for variable scopes.
+#define SCOPE_SEPARATOR "::"
+
 std::string expr2stl(const exprt &expr, const namespacet &ns)
 {
-  // TODO: Implement expr2stl.
-  // Expand this section so that it is able to properly convert from
-  // CBMC expressions to STL code.
-  return expr2c(expr, ns);
+  expr2stlt expr2stl{ns};
+
+  return expr2stl.convert(expr);
 }
 
 std::string type2stl(const typet &type, const namespacet &ns)
@@ -25,3 +65,219 @@ std::string type2stl(const typet &type, const namespacet &ns)
   // CBMC types to STL code.
   return type2c(type, ns);
 }
+
+expr2stlt::expr2stlt(const namespacet &ns)
+  : inside_bit_string(false), is_reference(false), ns(ns)
+{
+}
+
+std::string expr2stlt::convert(const exprt &expr)
+{
+  if(ID_and == expr.id())
+    convert_and(expr);
+  else if(ID_or == expr.id())
+    convert_or(expr);
+  else if(ID_xor == expr.id() || ID_notequal == expr.id())
+    convert_xor(expr);
+  else if(ID_equal == expr.id())
+    convert_equal(expr);
+  else if(ID_symbol == expr.id())
+    convert_symbol(expr);
+  else if(ID_not == expr.id())
+    convert_not(expr);
+  else // TODO: support more instructions in expr2stl.
+    return expr2c(expr, ns);
+
+  return result.str();
+}
+
+void expr2stlt::convert_and(const exprt &expr)
+{
+  if(inside_bit_string)
+    convert_multiary_bool(expr.operands(), AND);
+  else
+  {
+    std::vector<exprt> operands = expr.operands();
+    convert_first_non_trivial_operand(operands);
+    convert_multiary_bool(operands, AND);
+  }
+}
+
+void expr2stlt::convert_or(const exprt &expr)
+{
+  if(inside_bit_string)
+    convert_multiary_bool(expr.operands(), OR);
+  else
+  {
+    std::vector<exprt> operands = expr.operands();
+    convert_first_non_trivial_operand(operands);
+    convert_multiary_bool(operands, OR);
+  }
+}
+
+void expr2stlt::convert_xor(const exprt &expr)
+{
+  if(inside_bit_string)
+    convert_multiary_bool(expr.operands(), XOR);
+  else
+  {
+    std::vector<exprt> operands = expr.operands();
+    convert_first_non_trivial_operand(operands);
+    convert_multiary_bool(operands, XOR);
+  }
+}
+
+void expr2stlt::convert_equal(const exprt &expr)
+{
+  std::vector<exprt> operands =
+    instrument_equal_operands(expr.op0(), expr.op1());
+  if(inside_bit_string)
+    convert_multiary_bool(operands, XOR);
+  else
+  {
+    convert_first_non_trivial_operand(operands);
+    convert_multiary_bool(operands, XOR);
+  }
+}
+
+void expr2stlt::convert_not(const exprt &expr)
+{
+  // If a NOT expression is being handled here it must always mark the
+  // beginning of a new bit string.
+  PRECONDITION(!inside_bit_string);
+
+  if(ID_symbol == expr.op0().id())
+  {
+    // Use AN to load the symbol.
+    is_reference = true;
+    result << AND << NOT_POSTFIX << OPERAND_SEPARATOR;
+    convert(expr.op0());
+    result << LINE_SEPARATOR;
+  }
+  else
+  {
+    // Use NOT to negate the RLO after the wrapped expression was loaded.
+    convert(expr.op0());
+    result << NOT LINE_SEPARATOR;
+  }
+}
+
+void expr2stlt::convert_symbol(const exprt &expr)
+{
+  if(is_reference)
+  {
+    result << REFERENCE_FLAG;
+    is_reference = false;
+  }
+  result << id2string(id_shorthand(expr.get(ID_identifier)));
+}
+
+void expr2stlt::convert_multiary_bool(
+  const std::vector<exprt> &operands,
+  const char operation)
+{
+  for(const exprt &op : operands)
+  {
+    if(op.id() == ID_not)
+    {
+      result << operation << NOT_POSTFIX;
+      convert_bool_operand(op.op0());
+    }
+    else
+    {
+      result << operation;
+      convert_bool_operand(op);
+    }
+  }
+}
+
+void expr2stlt::convert_bool_operand(const exprt &op)
+{
+  if(op.id() == ID_symbol)
+  {
+    is_reference = true;
+    result << OPERAND_SEPARATOR;
+    convert(op);
+    result << LINE_SEPARATOR;
+  }
+  else
+  {
+    inside_bit_string = false;
+    result << NESTING_OPEN_LINE_SEPARATOR;
+    convert(op);
+    result << NESTING_CLOSED_LINE_SEPARATOR;
+  }
+}
+
+void expr2stlt::convert_first_non_trivial_operand(std::vector<exprt> &operands)
+{
+  exprt non_trivial_op;
+  for(auto it(begin(operands)); it != end(operands); ++it)
+  {
+    if(
+      (ID_symbol == it->id()) ||
+      (ID_not == it->id() && ID_symbol == it->op0().id()))
+      continue;
+    else
+    {
+      non_trivial_op = *it;
+      operands.erase(it);
+      break;
+    }
+  }
+  // Important for some scenarios: Convert complex op first, set bit string
+  // flag to true afterwards.
+  if(non_trivial_op.is_not_nil())
+    convert(non_trivial_op);
+
+  inside_bit_string = true;
+}
+
+std::vector<exprt>
+expr2stlt::instrument_equal_operands(const exprt &lhs, const exprt &rhs)
+{
+  std::vector<exprt> result;
+  if(ID_not != lhs.id() && ID_not != rhs.id())
+  {
+    // lhs == rhs is equivalent to X lhs; XN rhs;
+    result.push_back(lhs);
+    result.push_back(not_exprt{rhs});
+  }
+  else if(ID_not != lhs.id() && ID_not == rhs.id())
+  {
+    // lhs == !rhs is equivalent to X lhs; X rhs;
+    result.push_back(lhs);
+    result.push_back(rhs.op0());
+  }
+  else if(ID_not == lhs.id() && ID_not != rhs.id())
+  {
+    // !lhs == rhs is equivalent to X lhs; X rhs;
+    result.push_back(lhs.op0());
+    result.push_back(rhs);
+  }
+  else // ID_not == lhs.id() && ID_not == rhs.id()
+  {
+    // !lhs == !rhs is equivalent to X lhs; XN rhs;
+    result.push_back(lhs.op0());
+    result.push_back(rhs);
+  }
+  return result;
+}
+
+irep_idt expr2stlt::id_shorthand(const irep_idt &identifier)
+{
+  const symbolt *symbol;
+
+  if(
+    !ns.lookup(identifier, symbol) && !symbol->base_name.empty() &&
+    has_suffix(id2string(identifier), id2string(symbol->base_name)))
+    return symbol->base_name;
+
+  std::string sh = id2string(identifier);
+
+  std::string::size_type pos = sh.rfind(SCOPE_SEPARATOR);
+  if(pos != std::string::npos)
+    sh.erase(0, pos + 2);
+
+  return sh;
+}