From e7360c2c26558caa3b2762afae97065f6c5acb0e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 18 Nov 2024 12:52:45 +0000 Subject: [PATCH] Verilog: extract code for converting literals This extracts the code for converting string, real and integral literals into separate functions, in a separate file. --- lib/cbmc | 2 +- src/verilog/Makefile | 1 + src/verilog/convert_literals.cpp | 359 +++++++++++++++++++++++++ src/verilog/convert_literals.h | 18 ++ src/verilog/verilog_typecheck_expr.cpp | 317 ++-------------------- src/verilog/verilog_types.h | 2 +- 6 files changed, 398 insertions(+), 301 deletions(-) create mode 100644 src/verilog/convert_literals.cpp create mode 100644 src/verilog/convert_literals.h diff --git a/lib/cbmc b/lib/cbmc index beebdda9e..e8d340909 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit beebdda9e501efd7605ec33045d1e0979463bdb7 +Subproject commit e8d3409090087bd530bc56f83730c64b07e27529 diff --git a/src/verilog/Makefile b/src/verilog/Makefile index d502d79bf..9fd9d22fa 100644 --- a/src/verilog/Makefile +++ b/src/verilog/Makefile @@ -1,4 +1,5 @@ SRC = aval_bval_encoding.cpp \ + convert_literals.cpp \ expr2verilog.cpp \ sva_expr.cpp \ verilog_elaborate.cpp \ diff --git a/src/verilog/convert_literals.cpp b/src/verilog/convert_literals.cpp new file mode 100644 index 000000000..1e03a4a7d --- /dev/null +++ b/src/verilog/convert_literals.cpp @@ -0,0 +1,359 @@ +/*******************************************************************\ + +Module: Conversion for Verilog Literals + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "convert_literals.h" + +#include +#include +#include + +#include + +#include "verilog_types.h" + +constant_exprt convert_string_literal(const irep_idt &value) +{ + // These are unsigned integer vectors with 8 bits per character. + // The first character is the most significant one. + auto type = unsignedbv_typet{value.size() * 8}; + + // The below is quadratic, and should be made linear. + mp_integer new_value = 0; + for(std::size_t i = 0; i < value.size(); i++) + { + unsigned char character = value[i]; + new_value += mp_integer(character) << ((value.size() - i - 1) * 8); + } + + return from_integer(new_value, type); +} + +constant_exprt convert_real_literal(const irep_idt &value) +{ + // first, get rid of whitespace and underscores + // and make everything lower case + std::string rest; + rest.reserve(value.size()); + + for(unsigned i = 0; i < value.size(); i++) + { + char ch = value[i]; + if(!isspace(ch) && ch != '_') + rest += tolower(ch); + } + + const char *p = rest.c_str(); + + std::string str_whole_number, str_fraction_part, str_exponent; + + // get whole number part + while(*p != '.' && *p != 0 && *p != 'e') + { + str_whole_number += *p; + p++; + } + + // skip dot + if(*p == '.') + p++; + + // get fraction part + while(*p != 0 && *p != 'e') + { + str_fraction_part += *p; + p++; + } + + // skip e + if(*p == 'e') + p++; + + // skip + + if(*p == '+') + p++; + + // get exponent + while(*p != 0) + { + str_exponent += *p; + p++; + } + + std::string str_number = str_whole_number + str_fraction_part; + + mp_integer significand; + + if(str_number.empty()) + significand = 0; + else + significand = string2integer(str_number, 10); + + mp_integer exponent; + + if(str_exponent.empty()) + exponent = 0; + else + exponent = string2integer(str_exponent, 10); + + // adjust exponent + exponent -= str_fraction_part.size(); + + ieee_floatt ieee_float{ieee_float_spect::double_precision()}; + + ieee_float.from_base10(significand, exponent); + + constant_exprt result = ieee_float.to_expr(); + result.type() = verilog_real_typet{}; + + return result; +} + +constant_exprt convert_integral_literal(const irep_idt &value) +{ + // first, get rid of whitespace and underscores + // and make everything lower case + std::string rest; + rest.reserve(value.size()); + + for(unsigned i = 0; i < value.size(); i++) + { + char ch = value[i]; + if(!isspace(ch) && ch != '_') + rest += tolower(ch); + } + + std::string::size_type pos = rest.find('\''); + std::size_t bits = 0; + bool bits_given = false; + + if(pos != std::string::npos) // size given? + { + if(rest[0] != '\'') + { + bits = safe_string2size_t(rest); + bits_given = true; + } + + rest = rest.substr(pos + 1); + } + + // signed-flag 's' used? + bool s_flag_given = false; + + if(rest != "" && tolower(rest[0]) == 's') + { + s_flag_given = true; + rest = rest.substr(1); + } + + unsigned base = 10; + + // base given? + bool based = false; + + if(rest != "") + { + switch(rest[0]) + { + case 'b': + based = true; + base = 2; + rest.erase(0, 1); + break; + case 'd': + based = true; + base = 10; + rest.erase(0, 1); + break; + case 'h': + based = true; + base = 16; + rest.erase(0, 1); + break; + case 'o': + based = true; + base = 8; + rest.erase(0, 1); + break; + default: + base = 10; + } + } + + // based numbers are always unsigned unless 's' flag is given + bool is_signed = !based || s_flag_given; + + // check for z/x + bool four_valued = false; + + for(unsigned i = 0; i < rest.size(); i++) + if(rest[i] == '?' || rest[i] == 'z' || rest[i] == 'x') + four_valued = true; + + if(base != 10) + { + // expand bits + + std::string full_value = rest; + std::string bit_value; + + switch(base) + { + case 2: + bit_value = full_value; + break; + + case 8: + for(unsigned i = 0; i < full_value.size(); i++) + { + switch(full_value[i]) + { + // clang-format off + case '0': bit_value+="000"; break; + case '1': bit_value+="001"; break; + case '2': bit_value+="010"; break; + case '3': bit_value+="011"; break; + case '4': bit_value+="100"; break; + case '5': bit_value+="101"; break; + case '6': bit_value+="110"; break; + case '7': bit_value+="111"; break; + case 'x': bit_value+="xxx"; break; + case 'z': bit_value+="zzz"; break; + // clang-format on + } + } + break; + + case 16: + for(unsigned i = 0; i < full_value.size(); i++) + { + switch(full_value[i]) + { + // clang-format off + case '0': bit_value+="0000"; break; + case '1': bit_value+="0001"; break; + case '2': bit_value+="0010"; break; + case '3': bit_value+="0011"; break; + case '4': bit_value+="0100"; break; + case '5': bit_value+="0101"; break; + case '6': bit_value+="0110"; break; + case '7': bit_value+="0111"; break; + case '8': bit_value+="1000"; break; + case '9': bit_value+="1001"; break; + case 'a': bit_value+="1010"; break; + case 'b': bit_value+="1011"; break; + case 'c': bit_value+="1100"; break; + case 'd': bit_value+="1101"; break; + case 'e': bit_value+="1110"; break; + case 'f': bit_value+="1111"; break; + case 'x': bit_value+="xxxx"; break; + case 'z': bit_value+="zzzz"; break; + // clang-format on + } + } + break; + + default: + throw ebmc_errort() << "cannot convert literal " << value; + } + + std::string fvalue; + + if(bits_given) + { + fvalue = bit_value; + + if(fvalue.size() > bits) + fvalue.erase(0, fvalue.size() - bits); // cut off... + else if(fvalue.size() < bits) + { + // extend appropriately + char ext = '0'; + + if(fvalue.size() != 0 && (fvalue[0] == 'x' || fvalue[0] == 'z')) + ext = fvalue[0]; + + // add missing bits + fvalue = std::string(bits - fvalue.size(), ext) + fvalue; + } + } + else + { + fvalue = bit_value; + bits = fvalue.size(); + } + + if(four_valued) + { + // we do a 32-bit minimum if the number of bits isn't given + if(!bits_given) + { + if(bits < 32) + { + // do sign extension + char extension = is_signed ? fvalue.front() : '0'; + fvalue = std::string(32 - bits, extension) + fvalue; + bits = 32; + } + } + + typet type; + + if(is_signed) + type = verilog_signedbv_typet(bits); + else + type = verilog_unsignedbv_typet(bits); + + // stored as individual bits + return constant_exprt{fvalue, type}; + } + else // two valued + { + mp_integer int_value = binary2integer(fvalue, is_signed); + + // we do a 32-bit minimum if the number of bits isn't given + if(!bits_given) + if(bits < 32) + bits = 32; + + typet type; + + if(is_signed) + type = signedbv_typet(bits); + else + type = unsignedbv_typet(bits); + + // stored as bvrep + return constant_exprt{integer2bvrep(int_value, bits), type}; + } + } + else + { + // base 10, never negative + mp_integer int_value = string2integer(rest, base); + + if(!bits_given) + { + bits = address_bits(int_value + 1); + // we do a 32-bit minimum + if(bits < 32) + bits = 32; + } + + typet type; + + if(is_signed) + type = signedbv_typet(bits); + else + type = unsignedbv_typet(bits); + + return constant_exprt{integer2bvrep(int_value, bits), type}; + } + + UNREACHABLE; +} diff --git a/src/verilog/convert_literals.h b/src/verilog/convert_literals.h new file mode 100644 index 000000000..40a000b34 --- /dev/null +++ b/src/verilog/convert_literals.h @@ -0,0 +1,18 @@ +/*******************************************************************\ + +Module: Conversion for Verilog Literals + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_VERILOG_CONVERT_LITERALS_H +#define CPROVER_VERILOG_CONVERT_LITERALS_H + +#include + +constant_exprt convert_string_literal(const irep_idt &); +constant_exprt convert_real_literal(const irep_idt &); +constant_exprt convert_integral_literal(const irep_idt &); + +#endif diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index d0cc7ac1b..73a2c45df 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "convert_literals.h" #include "expr2verilog.h" #include "verilog_expr.h" #include "verilog_types.h" @@ -1248,22 +1249,13 @@ Function: verilog_typecheck_exprt::convert_constant exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr) { + auto source_location = expr.source_location(); + if(expr.type().id()==ID_string) { - // These are unsigned integer vectors with 8 bits per character. - // The first character is the most significant one. - const std::string &value=expr.get_string(ID_value); - auto type = unsignedbv_typet(value.size() * 8); - - // The below is quadratic, and should be made linear. - mp_integer new_value = 0; - for(std::size_t i = 0; i < value.size(); i++) - { - unsigned char character = value[i]; - new_value += mp_integer(character) << ((value.size() - i - 1) * 8); - } - - return from_integer(new_value, type).with_source_location(expr); + auto result = convert_string_literal(expr.get_value()); + result.add_source_location() = source_location; + return std::move(result); } else if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv || @@ -1274,301 +1266,28 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr) return std::move(expr); } - // first, get rid of whitespace and underscores - // and make everything lower case + const std::string &value = id2string(expr.get_value()); - const std::string &value=expr.get_string(ID_value); - expr.set("#verilog_value", value); - - std::string rest; - - for(unsigned i=0; ibits) - fvalue.erase(0, fvalue.size()-bits); // cut off... - else if(fvalue.size() +#include /// Used during elaboration only, /// to signal that a symbol is yet to be elaborated.