Merge pull request #91 from tautschnig/jsil-type-checking

Started type checking jsil programs

Author: Daniel Kroening

src/goto-analyzer/taint_analysis.cpp

@@ -134,7 +134,8 @@ void taint_analysist::instrument(
           {
             bool match=false;
             for(const auto & i : identifiers)
-              if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":"))
+              if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":") ||
+                 id2string(i)==id2string(rule.function_identifier))
               {
                 match=true;
                 break;

src/goto-programs/goto_convert_functions.cpp

@@ -80,7 +80,8 @@ void goto_convert_functionst::goto_convert()
        it->second.type.id()==ID_code &&
        (it->second.mode==ID_C ||
         it->second.mode==ID_cpp ||
-        it->second.mode==ID_java))
+        it->second.mode==ID_java ||
+        it->second.mode=="jsil"))
       symbol_list.push_back(it->first);
   }
 

src/jsil/Makefile

@@ -1,5 +1,5 @@
 SRC =  jsil_y.tab.cpp jsil_lex.yy.cpp \
-       jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp \
+       jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp jsil_types.cpp \
        jsil_parser.cpp jsil_typecheck.cpp expr2jsil.cpp \
        jsil_entry_point.cpp jsil_internal_additions.cpp
 

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

@@ -12,6 +12,8 @@ Author: Michael Tautschnig, [email protected]
 
 #include <ansi-c/c_types.h>
 
+#include "jsil_types.h"
+
 #include "jsil_internal_additions.h"
 
 /*******************************************************************\
@@ -39,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);
   }
 
@@ -53,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);
   }
 
@@ -70,4 +76,58 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.mode="jsil";
     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)
+  {
+    symbolt new_symbol;
+    new_symbol.name=identifier;
+    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:
@@ -120,18 +141,14 @@ Function: jsil_languaget::typecheck
 
  Outputs:
 
- Purpose:
+ Purpose: Converting from parse tree and type checking.
 
 \*******************************************************************/
 
 bool jsil_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
-    return true;
-
-  // now typecheck
   if(jsil_typecheck(symbol_table, get_message_handler()))
     return true;
 
@@ -152,7 +169,6 @@ Function: jsil_languaget::final
 
 bool jsil_languaget::final(symbol_tablet &symbol_table)
 {
-  jsil_internal_additions(symbol_table);
 
   if(jsil_entry_point(
       symbol_table,

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

@@ -8,6 +8,8 @@ Author: Michael Tautschnig, [email protected]
 
 #include <util/symbol.h>
 
+#include "jsil_types.h"
+
 #include "jsil_parse_tree.h"
 
 /*******************************************************************\
@@ -66,10 +68,19 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
   symbol_exprt s(to_symbol_expr(
       static_cast<const exprt&>(find(ID_declarator))));
 
+  code_typet symbol_type=to_code_type(s.type());
+
+  irep_idt proc_type=s.get("proc_type");
+
+  if(proc_type=="builtin")
+    symbol_type=jsil_builtin_code_typet(symbol_type);
+  else if(proc_type=="spec")
+    symbol_type=jsil_spec_code_typet(symbol_type);
+
   symbol.name=s.get_identifier();
   symbol.base_name=s.get_identifier();
   symbol.mode="jsil";
-  symbol.type=s.type();
+  symbol.type=symbol_type;
   symbol.location=s.source_location();
 
   code_blockt code(to_code_block(
@@ -133,4 +144,3 @@ void jsil_parse_treet::output(std::ostream &out) const
     out << "\n";
   }
 }
-

src/jsil/jsil_parse_tree.h

@@ -29,6 +29,16 @@ class jsil_declarationt:public exprt
     add(ID_declarator, expr);
   }
 
+  const symbol_exprt &declarator() const
+  {
+    return static_cast<const symbol_exprt &>(find(ID_declarator));
+  }
+
+  symbol_exprt &declarator()
+  {
+    return static_cast<symbol_exprt &>(add(ID_declarator));
+  }
+
   void add_returns(
     const irep_idt &value,
     const irep_idt &label)
@@ -37,6 +47,16 @@ 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_label() const
+  {
+    return find(ID_return).get(ID_label);
+  }
+
   void add_throws(
     const irep_idt &value,
     const irep_idt &label)
@@ -45,11 +65,31 @@ 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_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));
+  }
+
+  code_blockt &value()
+  {
+    return static_cast<code_blockt &>(add(ID_value));
+  }
+
   void to_symbol(symbolt &symbol) const;
 
   void output(std::ostream &) const;