Improvements to Jsil type checking

Catch decl in the try/catch is not used.
Making string constants to be ID_constant expressions with string_typet
Typecheking function call.
Added "nan" symbol. Assigning type to lhs after unknown function call.
White spaces, positioning { in new line.
Cleaning up the code. Correct includes.
Renaming jsil types.
Explicit constructors. Inlining expressions if used only once.
Asserting that expression does not have type set just yet.
More efficient implementation for is_subtype.
Introduced jsil_incompatible_types to hide low level implementation.
Fixed bug in is_subtype.
Typechecking throw and return labels.
Typechecking bitwise operators.
Avoiding duplicate type-checking by marking symbols as type-checked.
Add empty decl symbol. Special case for index expression. Clean up.
Converting all procedure declarations to symbols before typechecking.

Author: Daiva Naudziuniene

src/jsil/jsil_convert.cpp

@@ -56,6 +56,14 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree)
     if(convert_code(new_symbol, to_code(new_symbol.value)))
       return true;
 
+    if(symbol_table.has_symbol(new_symbol.name))
+    {
+      symbolt &s=symbol_table.lookup(new_symbol.name);
+      if(s.value.id()=="no-body-just-yet")
+      {
+        symbol_table.remove(s.name);
+      }
+    }
     if(symbol_table.add(new_symbol))
     {
       throw "duplicate symbol "+id2string(new_symbol.name);
@@ -104,7 +112,8 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
 
       code_try_catcht t_c;
       t_c.try_code().swap(t);
-      code_declt d(symbol.symbol_expr());
+      // Adding empty symbol to catch decl
+      code_declt d(symbol_exprt("decl_symbol"));
       t_c.add_catch(d, g);
       t_c.add_source_location()=code.source_location();
 

src/jsil/jsil_internal_additions.cpp

@@ -41,6 +41,8 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
     symbol.is_thread_local=true;
+    // mark as already typechecked
+    symbol.is_extern=true;
     dest.add(symbol);
   }
 
@@ -55,6 +57,8 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
     symbol.is_thread_local=true;
+    // mark as already typechecked
+    symbol.is_extern=true;
     dest.add(symbol);
   }
 
@@ -73,28 +77,57 @@ void jsil_internal_additions(symbol_tablet &dest)
     dest.add(symbol);
   }
 
+  // add nan
+
+  {
+    symbolt symbol;
+    symbol.base_name="nan";
+    symbol.name="nan";
+    symbol.type=floatbv_typet();
+    symbol.mode="jsil";
+    // mark as already typechecked
+    symbol.is_extern=true;
+    dest.add(symbol);
+  }
+
+  // add empty symbol used for decl statemements
+
+  {
+    symbolt symbol;
+    symbol.base_name="decl_symbol";
+    symbol.name="decl_symbol";
+    symbol.type=empty_typet();
+    symbol.mode="jsil";
+    // mark as already typechecked
+    symbol.is_extern=true;
+    dest.add(symbol);
+  }
+
   // add builtin objects
   const std::vector<std::string> builtin_objects=
-    { "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString",
-      "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp",
-      "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror",
-      "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp",
-      "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp",
-      "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp",
-      "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp",
-      "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp",
-      "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson"
-    };
-
-  for(const auto & identifier : builtin_objects)
+  {
+    "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString",
+    "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp",
+    "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror",
+    "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp",
+    "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp",
+    "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp",
+    "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp",
+    "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp",
+    "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson"
+  };
+
+  for(const auto &identifier : builtin_objects)
   {
     symbolt new_symbol;
     new_symbol.name=identifier;
-    new_symbol.type=jsil_builtin_objectt();
+    new_symbol.type=jsil_builtin_object_type();
     new_symbol.base_name=identifier;
     new_symbol.mode="jsil";
     new_symbol.is_type=false;
     new_symbol.is_lvalue=false;
+    // mark as already typechecked
+    new_symbol.is_extern=true;
     dest.add(new_symbol);
   }
 }

src/jsil/jsil_language.cpp

@@ -56,6 +56,27 @@ void jsil_languaget::modules_provided(std::set<std::string> &modules)
 
 /*******************************************************************\
 
+Function: jsil_languaget::interfaces
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Adding symbols for all procedure declarations
+
+\*******************************************************************/
+
+bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
+{
+  if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
+    return true;
+
+  jsil_internal_additions(symbol_table);
+  return false;
+}
+
+/*******************************************************************\
+
 Function: jsil_languaget::preprocess
 
   Inputs:
@@ -128,12 +149,6 @@ bool jsil_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
-    return true;
-
-  jsil_internal_additions(symbol_table);
-
-  // now typecheck
   if(jsil_typecheck(symbol_table, get_message_handler()))
     return true;
 

src/jsil/jsil_language.h

@@ -62,6 +62,7 @@ class jsil_languaget:public languaget
   virtual std::set<std::string> extensions() const;
 
   virtual void modules_provided(std::set<std::string> &modules);
+  virtual bool interfaces(symbol_tablet &symbol_table);
 
 protected:
   jsil_parse_treet parse_tree;

src/jsil/jsil_parse_tree.cpp

@@ -73,7 +73,7 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
   irep_idt proc_type=s.get("proc_type");
 
   if(proc_type=="builtin")
-	  symbol_type=jsil_builtin_code_typet(symbol_type);
+    symbol_type=jsil_builtin_code_typet(symbol_type);
   else if(proc_type=="spec")
     symbol_type=jsil_spec_code_typet(symbol_type);
 

src/jsil/jsil_parse_tree.h

@@ -47,12 +47,14 @@ class jsil_declarationt:public exprt
     add(ID_return).set(ID_label, label);
   }
 
-  const irep_idt &returns_value() const {
-	  return find(ID_return).get(ID_value);
+  const irep_idt &returns_value() const
+  {
+    return find(ID_return).get(ID_value);
   }
 
-  const irep_idt &returns_label() const {
-	  return find(ID_return).get(ID_label);
+  const irep_idt &returns_label() const
+  {
+    return find(ID_return).get(ID_label);
   }
 
   void add_throws(
@@ -63,25 +65,29 @@ class jsil_declarationt:public exprt
     add(ID_throw).set(ID_label, label);
   }
 
-  const irep_idt &throws_value() const {
-	  return find(ID_throw).get(ID_value);
+  const irep_idt &throws_value() const
+  {
+    return find(ID_throw).get(ID_value);
   }
 
-  const irep_idt &throws_label() const {
-	  return find(ID_throw).get(ID_label);
+  const irep_idt &throws_label() const
+  {
+    return find(ID_throw).get(ID_label);
   }
 
   void add_value(const code_blockt &code)
   {
     add(ID_value, code);
   }
 
-  const code_blockt &value() const {
-	  return static_cast<const code_blockt &> (find(ID_value));
+  const code_blockt &value() const
+  {
+    return static_cast<const code_blockt &>(find(ID_value));
   }
 
-  code_blockt &value() {
-	  return static_cast<code_blockt &> (add(ID_value));
+  code_blockt &value()
+  {
+    return static_cast<code_blockt &>(add(ID_value));
   }
 
   void to_symbol(symbolt &symbol) const;