Verilog: fix string literals

The conversion of string literals has assumed a binary number represenation.

Author: kroening

regression/verilog/string/string_literals1.desc

@@ -0,0 +1,7 @@
+CORE
+string_literals1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/string/string_literals1.v

@@ -0,0 +1,12 @@
+module main;
+
+  // padded from left with zeros
+  wire [6*8-1:0] hello = "hello";
+  always assert p0: hello[0*8+7:0*8] == "o";
+  always assert p1: hello[1*8+7:1*8] == "l";
+  always assert p2: hello[2*8+7:2*8] == "l";
+  always assert p3: hello[3*8+7:3*8] == "e";
+  always assert p4: hello[4*8+7:4*8] == "h";
+  always assert p5: hello[5*8+7:5*8] == 0;
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -902,23 +902,21 @@ void verilog_typecheck_exprt::convert_constant(constant_exprt &expr)
 {
   if(expr.type().id()==ID_string)
   {
-    exprt new_expr;
+    // 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);
 
-    new_expr.type()=unsignedbv_typet(value.size()*8);
-
-    std::string new_value;
-
-    for(unsigned i=0; i<value.size(); i++)
-      for(unsigned bit=0; bit<8; bit++)
-      {
-        bool b=(value[i]&(1<<bit))!=0;
-        new_value=(b?"1":"0")+new_value;
-      }
+    // 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);
+    }
 
-    new_expr.set(ID_value, new_value);
-    
-    expr.swap(new_expr);
+    expr =
+      from_integer(new_value, type).with_source_location<constant_exprt>(expr);
     return;
   }
   else if(expr.type().id()==ID_unsignedbv ||