[Solidity] add c library

src/solidity-frontend/solidity_convert.cpp

@@ -1,5 +1,5 @@
 #include <solidity-frontend/solidity_convert.h>
-#include <solidity_template.h>
+#include <solidity-frontend/solidity_template.h>
 #include <solidity-frontend/typecast.h>
 #include <util/arith_tools.h>
 #include <util/bitvector.h>
@@ -88,6 +88,8 @@ bool solidity_convertert::convert()
     return true;
   is_builtin_members = false;
 
+  log_progress("Done conversion of intrinsics");
+
   // reasoning-based verification
 
   // populate exportedSymbolsList
@@ -247,6 +249,9 @@ bool solidity_convertert::convert_builtin_members()
   if (populate_builtin_functions(
         "", SolidityTemplate::addmod, SolidityTemplate::addmod_body))
     return true;
+  if (populate_builtin_functions(
+        "", SolidityTemplate::mulmod, SolidityTemplate::mulmod_body))
+    return true;
 
   return false;
 }
@@ -2329,7 +2334,8 @@ bool solidity_convertert::get_expr(
   }
   case SolidityGrammar::ExpressionT::SpecialMemberCall:
   {
-    // get_special_member_basename()
+    //!TODO
+    log_error("Unsupported built-in member call");
     abort();
     break;
     //
@@ -3700,7 +3706,7 @@ bool solidity_convertert::get_elementary_type_name(
   }
   case SolidityGrammar::ElementaryTypeNameT::BYTES:
   {
-    new_type = uint_type();
+    new_type = unsignedbv_typet(256);
     new_type.set("#sol_type", elementary_type_name_to_str(type));
 
     break;

src/solidity-frontend/solidity_language.cpp

@@ -7,6 +7,7 @@ CC_DIAGNOSTIC_POP()
 
 #include <solidity-frontend/solidity_language.h>
 #include <solidity-frontend/solidity_convert.h>
+#include <solidity-frontend/solidity_template.h>
 #include <clang-c-frontend/clang_c_main.h>
 #include <clang-cpp-frontend/clang_cpp_adjust.h>
 #include <clang-c-frontend/clang_c_convert.h>
@@ -119,7 +120,6 @@ bool solidity_languaget::typecheck(contextt &context, const std::string &module)
   contextt new_context;
   convert_intrinsics(
     new_context); // Add ESBMC and TACAS intrinsic symbols to the context
-  log_progress("Done conversion of intrinsics...");
 
   solidity_convertert converter(
     new_context, src_ast_json, func_name, smart_contract);
@@ -159,6 +159,7 @@ std::string solidity_languaget::temp_c_file()
 {
   // This function populates the temp file so that Clang has a compilation job.
   // Clang needs a job to convert the intrinsics.
-  std::string content = R"(int main() { return 0; } )";
+  std::string content =
+    R"(int main() { return 0; } )" + SolidityTemplate::sol_library;
   return content;
 }