diff --git a/src/statement-list/converters/expr2statement_list.cpp b/src/statement-list/converters/expr2statement_list.cpp index 4d8ed594c86..2aa6e399bf4 100644 --- a/src/statement-list/converters/expr2statement_list.cpp +++ b/src/statement-list/converters/expr2statement_list.cpp @@ -10,12 +10,105 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include +#include +#include + +#include +#include +#include + +/// 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 "::" + +/// Modifies the parameters of a binary equal expression with the help of its +/// symmetry properties. This function basically converts the operands to +/// operands of a XOR expression so that the whole expression can be treated as +/// such. This can reduce complexity in some cases. +/// \param lhs: Left side of the binary expression. +/// \param rhs: Right side of the binary expression. +/// \return: List of instrumented operands. +static std::vector +instrument_equal_operands(const exprt &lhs, const exprt &rhs) +{ + std::vector 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; +} + +/// Checks if the expression or one of its parameters is not of type bool. +/// \param expr: Expression to verify. +/// \return: True if the expression and its operands are not or only partially +/// of type bool, false otherwise. +static bool is_not_bool(const exprt &expr) +{ + if(!expr.is_boolean()) + return true; + for(const exprt &op : expr.operands()) + if(!op.is_boolean()) + return true; + return false; +} + 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 +118,187 @@ 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) +{ + // Redirect to expr2c if no boolean expression. + if(is_not_bool(expr)) + return expr2c(expr, ns); + + if(ID_and == expr.id()) + convert(to_and_expr(expr)); + else if(ID_or == expr.id()) + convert(to_or_expr(expr)); + else if(ID_xor == expr.id()) + convert(to_xor_expr(expr)); + else if(ID_notequal == expr.id()) + convert(to_notequal_expr(expr)); + else if(ID_equal == expr.id()) + convert(to_equal_expr(expr)); + else if(ID_symbol == expr.id()) + convert(to_symbol_expr(expr)); + else if(ID_not == expr.id() && expr.op0().type().id() == ID_bool) + convert(to_not_expr(expr)); + else // TODO: support more instructions in expr2stl. + return expr2c(expr, ns); + + return result.str(); +} + +void expr2stlt::convert(const and_exprt &expr) +{ + std::vector operands = expr.operands(); + convert_multiary_bool(operands, AND); +} + +void expr2stlt::convert(const or_exprt &expr) +{ + std::vector operands = expr.operands(); + convert_multiary_bool(operands, OR); +} + +void expr2stlt::convert(const xor_exprt &expr) +{ + std::vector operands = expr.operands(); + convert_multiary_bool(operands, XOR); +} + +void expr2stlt::convert(const notequal_exprt &expr) +{ + std::vector operands = expr.operands(); + convert_multiary_bool(operands, XOR); +} + +void expr2stlt::convert(const equal_exprt &expr) +{ + std::vector operands = + instrument_equal_operands(expr.lhs(), expr.rhs()); + convert_multiary_bool(operands, XOR); +} + +void expr2stlt::convert(const not_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.op().id()) + { + // Use AN to load the symbol. + is_reference = true; + result << AND << NOT_POSTFIX << OPERAND_SEPARATOR; + convert(to_symbol_expr(expr.op())); + result << LINE_SEPARATOR; + } + else + { + // Use NOT to negate the RLO after the wrapped expression was loaded. + convert(expr.op()); + result << NOT LINE_SEPARATOR; + } +} + +void expr2stlt::convert(const symbol_exprt &expr) +{ + if(is_reference) + { + result << REFERENCE_FLAG; + is_reference = false; + } + result << id2string(id_shorthand(expr.get_identifier())); +} + +void expr2stlt::convert_multiary_bool( + std::vector &operands, + const char operation) +{ + if(inside_bit_string) + convert_multiary_bool_operands(operands, operation); + else + { + convert_first_non_trivial_operand(operands); + convert_multiary_bool_operands(operands, operation); + } +} + +void expr2stlt::convert_multiary_bool_operands( + const std::vector &operands, + const char operation) +{ + for(const exprt &op : operands) + { + if(ID_not == op.id()) + { + 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(to_symbol_expr(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 &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; +} + +irep_idt expr2stlt::id_shorthand(const irep_idt &identifier) +{ + const symbolt *symbol; + std::string shorthand = id2string(identifier); + if( + !ns.lookup(identifier, symbol) && !symbol->base_name.empty() && + has_suffix(shorthand, id2string(symbol->base_name))) + return symbol->base_name; + + const std::string::size_type pos = shorthand.rfind(SCOPE_SEPARATOR); + if(pos != std::string::npos) + shorthand.erase(0, pos + std::strlen(SCOPE_SEPARATOR)); + + return shorthand; +} diff --git a/src/statement-list/converters/expr2statement_list.h b/src/statement-list/converters/expr2statement_list.h index 668b5433e20..6593c25dfd0 100644 --- a/src/statement-list/converters/expr2statement_list.h +++ b/src/statement-list/converters/expr2statement_list.h @@ -9,18 +9,137 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H #define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H +#include +#include +#include + #include /// Converts a given expression to human-readable STL code. /// \param expr: Expression to be converted. /// \param ns: Namespace of the TIA application. /// \result String with the STL representation of the given parameters. -std::string expr2stl(const class exprt &expr, const class namespacet &ns); +std::string expr2stl(const exprt &expr, const namespacet &ns); /// Converts a given type to human-readable STL code. /// \param type: Type to be converted. /// \param ns: Namespace of the TIA application. /// \result String with the STL representation of the given type. -std::string type2stl(const class typet &type, const class namespacet &ns); +std::string type2stl(const typet &type, const namespacet &ns); + +/// Class for saving the internal state of the conversion process. +class expr2stlt +{ + /// Internal representation of the FC bit in STL. Used to track if the + /// current boolean operation is part of another. + bool inside_bit_string; + + /// Flag to specify if the next symbol to convert is a reference to a + /// variable. + bool is_reference; + + /// Contains the symbol table of the current program to convert. + const namespacet &ns; + + /// Used for saving intermediate results of the conversion process. + std::stringstream result; + +public: + /// Creates a new instance of the converter. + /// \param ns: Namespace containing the symbols of the program to convert. + explicit expr2stlt(const namespacet &ns); + + /// Invokes the conversion process for the given expression and calls itself + /// recursively in the process. + /// \param expr: Expression to convert. Operands of this expression will be + /// converted as well via recursion. + /// \return: String containing human-readable STL code for the expression. + std::string convert(const exprt &expr); + +private: + /// Converts the given AND expression to human-readable STL code. If the + /// expression marks the beginning of a bit string, the first non-trivial + /// operand (that encloses all expressions which are not a symbol or a + /// negation of a symbol) is being converted first. This reduces nesting. + /// \param expr: AND expression to convert. + void convert(const and_exprt &expr); + + /// Converts the given OR expression to human-readable STL code. If the + /// expression marks the beginning of a bit string, the first non-trivial + /// operand (that encloses all expressions which are not a symbol or a + /// negation of a symbol) is being converted first. This reduces nesting. + /// \param expr: OR expression to convert. + void convert(const or_exprt &expr); + + /// Converts the given XOR expression to human-readable STL code. If the + /// expression marks the beginning of a bit string, the first non-trivial + /// operand (that encloses all expressions which are not a symbol or a + /// negation of a symbol) is being converted first. This reduces nesting. + /// \param expr: XOR expression to convert. + void convert(const xor_exprt &expr); + + /// Converts the given notequal (!=) expression to human-readable STL code. + /// If the expression marks the beginning of a bit string, the first + /// non-trivial operand (that encloses all expressions which are not a symbol + /// or a negation of a symbol) is being converted first. This reduces + /// nesting. + /// \param expr: Notequal expression to convert. + void convert(const notequal_exprt &expr); + + /// Converts the given equal (==) expression to human-readable STL code. If + /// the expression marks the beginning of a bit string, the first non-trivial + /// operand (that encloses all expressions which are not a symbol or a + /// negation of a symbol) is being converted first. This reduces nesting. + /// \param expr: Equal expression to convert. + void convert(const equal_exprt &expr); + + /// Converts the given NOT expression to human-readable STL code. This + /// function may only be called in the case of a new bit string. If the NOT + /// expression wraps a symbol it is negated and loaded on the RLO via a + /// simple AN instruction. In the case of a more complex expression, the + /// expression is being converted first and negated afterwards. + /// \param expr: Not expression to convert. + void convert(const not_exprt &expr); + + /// Converts the given symbol expression to human-readable STL code. This + /// function also checks if the symbol should be a reference and adds the + /// additional code if needed. + /// \param expr: Symbol expression to convert. + void convert(const symbol_exprt &expr); + + /// Iterates through all the given operands and converts them depending on + /// the operation. Performs a simplification by rearranging the operands + /// if appropriate. + /// \param [out] operands: Operands of any multiary instruction. + /// \param operation: Character specifying the operation in STL. + void + convert_multiary_bool(std::vector &operands, const char operation); + + /// Iterates through all the given operands and converts them depending on + /// the operation. + /// \param operands: Operands of any multiary instruction. + /// \param operation: Character specifying the operation in STL. + void convert_multiary_bool_operands( + const std::vector &operands, + const char operation); + + /// Converts a single boolean operand and introduces an additional nesting + /// layer if needed. + void convert_bool_operand(const exprt &op); + + /// Iterates through all the given operands in search for the first + /// non-trivial operand (that encloses all expressions which are not a symbol + /// or a negation of a symbol). If found, removes the operand from the list + /// and converts it first. This is used to avoid unnecessary nesting. + /// \param [out] operands: List of operands. Gets modified by this function + /// if it includes a non-trivial operand. + void convert_first_non_trivial_operand(std::vector &operands); + + /// Returns the given identifier in a form that is compatible with STL by + /// looking up the symbol or cutting the scope when needed. + /// \param identifier: Identifier that should be converted. + /// \return: Converted identifier. + irep_idt id_shorthand(const irep_idt &identifier); +}; #endif // CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l index 3ed788a34d3..892942eff35 100644 --- a/src/statement-list/scanner.l +++ b/src/statement-list/scanner.l @@ -116,6 +116,7 @@ void statement_list_scanner_init() CLR { loc(); return TOK_CLR_RLO; } S { loc(); return TOK_SET; } R { loc(); return TOK_RESET; } + NOT { loc(); return TOK_NOT; } A { loc(); return TOK_AND; } AN { loc(); return TOK_AND_NOT; } O { loc(); return TOK_OR; } diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index 65366966dac..13380f934e7 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -387,6 +387,8 @@ void statement_list_typecheckt::typecheck_statement_list_instruction( typecheck_statement_list_accu_real_lte(op_code); else if(ID_statement_list_accu_real_gte == statement) typecheck_statement_list_accu_real_gte(op_code); + else if(ID_statement_list_not == statement) + typecheck_statement_list_not(op_code); else if(ID_statement_list_and == statement) typecheck_statement_list_and(op_code, tia_element); else if(ID_statement_list_and_not == statement) @@ -753,6 +755,20 @@ void statement_list_typecheckt::typecheck_statement_list_accu_real_gte( typecheck_accumulator_compare_instruction(ID_ge); } +void statement_list_typecheckt::typecheck_statement_list_not( + const codet &op_code) +{ + typecheck_instruction_without_operand(op_code); + if(fc_bit) + { + const not_exprt unsimplified{rlo_bit}; + rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table)); + or_bit = false; + } + else + initialize_bit_expression(false_exprt{}); +} + void statement_list_typecheckt::typecheck_statement_list_and( const codet &op_code, const symbolt &tia_element) diff --git a/src/statement-list/statement_list_typecheck.h b/src/statement-list/statement_list_typecheck.h index 4a99fdf70be..fb209e94212 100644 --- a/src/statement-list/statement_list_typecheck.h +++ b/src/statement-list/statement_list_typecheck.h @@ -364,6 +364,11 @@ class statement_list_typecheckt : public typecheckt // Bit Logic instructions + /// Performs a typecheck on a STL boolean NOT instruction. Reads and modifies + /// the RLO, OR and FC bit. + /// \param op_code: OP code of the instruction. + void typecheck_statement_list_not(const codet &op_code); + /// Performs a typecheck on a STL boolean And instruction. Reads and modifies /// the RLO, OR and FC bit. /// \param op_code: OP code of the instruction.