cprover
jsil_typecheck.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: Michael Tautschnig, tautschn@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jsil_typecheck.h"
13 
14 #include <util/symbol_table.h>
15 #include <util/prefix.h>
16 #include <util/std_expr.h>
17 
18 #include "expr2jsil.h"
19 #include "jsil_types.h"
20 
21 std::string jsil_typecheckt::to_string(const exprt &expr)
22 {
23  return expr2jsil(expr, ns);
24 }
25 
26 std::string jsil_typecheckt::to_string(const typet &type)
27 {
28  return type2jsil(type, ns);
29 }
30 
33 {
34  return id2string(proc_name) + "::" + id2string(ds);
35 }
36 
38 {
39  expr.type()=type;
40 
41  if(expr.id()==ID_symbol)
42  {
43  const irep_idt &id=to_symbol_expr(expr).get_identifier();
44 
45  if(!symbol_table.has_symbol(id))
46  {
47  error() << "unexpected symbol: " << id << eom;
48  throw 0;
49  }
50 
52  if(s.type.id().empty() || s.type.is_nil())
53  s.type=type;
54  else
55  s.type=jsil_union(s.type, type);
56  }
57 }
58 
60  exprt &expr,
61  const typet &type,
62  bool must)
63 {
64  if(type.id().empty() || type.is_nil())
65  {
66  err_location(expr);
67  error() << "make_type_compatible got empty type: " << expr.pretty() << eom;
68  throw 0;
69  }
70 
71  if(expr.type().id().empty() || expr.type().is_nil())
72  {
73  // Type is not yet set
74  update_expr_type(expr, type);
75  return;
76  }
77 
78  if(must)
79  {
80  if(jsil_incompatible_types(expr.type(), type))
81  {
82  err_location(expr);
83  error() << "failed to typecheck expr "
84  << expr.pretty() << " with type "
85  << expr.type().pretty()
86  << "; required type " << type.pretty() << eom;
87  throw 0;
88  }
89  }
90  else if(!jsil_is_subtype(type, expr.type()))
91  {
92  // Types are not compatible
93  typet upper=jsil_union(expr.type(), type);
94  update_expr_type(expr, upper);
95  }
96 }
97 
99 {
100  if(type.id()==ID_code)
101  {
102  code_typet &parameters=to_code_type(type);
103 
104  for(code_typet::parametert &p : parameters.parameters())
105  {
106  // create new symbol
107  parameter_symbolt new_symbol;
108  new_symbol.base_name=p.get_identifier();
109 
110  // append procedure name to parameters
111  p.set_identifier(add_prefix(p.get_identifier()));
112  new_symbol.name=p.get_identifier();
113 
114  if(is_jsil_builtin_code_type(type))
115  new_symbol.type=jsil_value_or_empty_type();
116  else if(is_jsil_spec_code_type(type))
117  new_symbol.type=jsil_value_or_reference_type();
118  else
119  new_symbol.type=jsil_value_type(); // User defined function
120 
121  new_symbol.mode="jsil";
122 
123  // mark as already typechecked
124  new_symbol.is_extern=true;
125 
126  if(symbol_table.add(new_symbol))
127  {
128  error() << "failed to add parameter symbol `"
129  << new_symbol.name << "' in the symbol table" << eom;
130  throw 0;
131  }
132  }
133  }
134 }
135 
137 {
138  // first do sub-nodes
140 
141  // now do case-split
142  typecheck_expr_main(expr);
143 }
144 
146 {
147  Forall_operands(it, expr)
148  typecheck_expr(*it);
149 }
150 
152 {
153  if(expr.id()==ID_code)
154  {
155  err_location(expr);
156  error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
157  throw 0;
158  }
159  else if(expr.id()==ID_symbol)
161  else if(expr.id()==ID_constant)
162  {
163  }
164  else
165  {
166  // expressions are expected not to have type set just yet
167  assert(expr.type().is_nil() || expr.type().id().empty());
168 
169  if(expr.id()==ID_null ||
170  expr.id()=="undefined" ||
171  expr.id()==ID_empty)
173  else if(expr.id()=="null_type" ||
174  expr.id()=="undefined_type" ||
175  expr.id()==ID_boolean ||
176  expr.id()==ID_string ||
177  expr.id()=="number" ||
178  expr.id()=="builtin_object" ||
179  expr.id()=="user_object" ||
180  expr.id()=="object" ||
181  expr.id()==ID_reference ||
182  expr.id()==ID_member ||
183  expr.id()=="variable")
184  expr.type()=jsil_kind();
185  else if(expr.id()=="proto" ||
186  expr.id()=="fid" ||
187  expr.id()=="scope" ||
188  expr.id()=="constructid" ||
189  expr.id()=="primvalue" ||
190  expr.id()=="targetfunction" ||
191  expr.id()==ID_class)
192  {
193  // TODO: have a special type for builtin fields
194  expr.type()=string_typet();
195  }
196  else if(expr.id()==ID_not)
198  else if(expr.id()=="string_to_num")
200  else if(expr.id()==ID_unary_minus ||
201  expr.id()=="num_to_int32" ||
202  expr.id()=="num_to_uint32" ||
203  expr.id()==ID_bitnot)
204  {
206  expr.type()=floatbv_typet();
207  }
208  else if(expr.id()=="num_to_string")
209  {
211  expr.type()=string_typet();
212  }
213  else if(expr.id()==ID_equal)
215  else if(expr.id()==ID_lt ||
216  expr.id()==ID_le)
218  else if(expr.id()==ID_plus ||
219  expr.id()==ID_minus ||
220  expr.id()==ID_mult ||
221  expr.id()==ID_div ||
222  expr.id()==ID_mod ||
223  expr.id()==ID_bitand ||
224  expr.id()==ID_bitor ||
225  expr.id()==ID_bitxor ||
226  expr.id()==ID_shl ||
227  expr.id()==ID_shr ||
228  expr.id()==ID_lshr)
230  else if(expr.id()==ID_and ||
231  expr.id()==ID_or)
233  else if(expr.id()=="subtype_of")
235  else if(expr.id()==ID_concatenation)
237  else if(expr.id()=="ref")
238  typecheck_expr_ref(expr);
239  else if(expr.id()=="field")
240  typecheck_expr_field(expr);
241  else if(expr.id()==ID_base)
242  typecheck_expr_base(expr);
243  else if(expr.id()==ID_typeof)
244  expr.type()=jsil_kind();
245  else if(expr.id()=="new")
246  expr.type()=jsil_user_object_type();
247  else if(expr.id()=="hasField")
249  else if(expr.id()==ID_index)
250  typecheck_expr_index(expr);
251  else if(expr.id()=="delete")
252  typecheck_expr_delete(expr);
253  else if(expr.id()=="protoField")
255  else if(expr.id()=="protoObj")
257  else if(expr.id()==ID_side_effect)
259  else
260  {
261  err_location(expr);
262  error() << "unexpected expression: " << expr.pretty() << eom;
263  throw 0;
264  }
265  }
266 }
267 
270 {
271  irept &excep_list=expr.add(ID_exception_list);
272  assert(excep_list.id()==ID_symbol);
273  symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
275 }
276 
278 {
279  if(expr.id()==ID_null)
280  expr.type()=jsil_null_type();
281  else if(expr.id()=="undefined")
282  expr.type()=jsil_undefined_type();
283  else if(expr.id()==ID_empty)
284  expr.type()=jsil_empty_type();
285 }
286 
288 {
289  if(expr.operands().size()!=2)
290  {
291  err_location(expr);
292  error() << "operator `" << expr.id()
293  << "' expects two operands" << eom;
294  throw 0;
295  }
296 
297  make_type_compatible(expr.op0(), jsil_object_type(), true);
298  make_type_compatible(expr.op1(), string_typet(), true);
299 
301 }
302 
304 {
305  if(expr.operands().size()!=2)
306  {
307  err_location(expr);
308  error() << "operator `" << expr.id()
309  << "' expects two operands";
310  throw 0;
311  }
312 
313  make_type_compatible(expr.op0(), jsil_object_type(), true);
314  make_type_compatible(expr.op1(), jsil_object_type(), true);
315 
316  expr.type()=bool_typet();
317 }
318 
320 {
321  if(expr.operands().size()!=2)
322  {
323  err_location(expr);
324  error() << "operator `" << expr.id()
325  << "' expects two operands" << eom;
326  throw 0;
327  }
328 
329  make_type_compatible(expr.op0(), jsil_object_type(), true);
330  make_type_compatible(expr.op1(), string_typet(), true);
331 
332  expr.type()=bool_typet();
333 }
334 
336 {
337  if(expr.operands().size()!=2)
338  {
339  err_location(expr);
340  error() << "operator `" << expr.id()
341  << "' expects two operands" << eom;
342  throw 0;
343  }
344 
345  make_type_compatible(expr.op0(), jsil_object_type(), true);
346  make_type_compatible(expr.op1(), string_typet(), true);
347 
348  // special case for function identifiers
349  if(expr.op1().id()=="fid" || expr.op1().id()=="constructid")
350  expr.type()=code_typet();
351  else
352  expr.type()=jsil_value_type();
353 }
354 
356 {
357  if(expr.operands().size()!=2)
358  {
359  err_location(expr);
360  error() << "operator `" << expr.id()
361  << "' expects two operands" << eom;
362  throw 0;
363  }
364 
365  make_type_compatible(expr.op0(), jsil_object_type(), true);
366  make_type_compatible(expr.op1(), string_typet(), true);
367 
368  expr.type()=bool_typet();
369 }
370 
372 {
373  if(expr.operands().size()!=1)
374  {
375  err_location(expr);
376  error() << "operator `" << expr.id()
377  << "' expects single operand" << eom;
378  throw 0;
379  }
380 
382 
383  expr.type()=string_typet();
384 }
385 
387 {
388  if(expr.operands().size()!=1)
389  {
390  err_location(expr);
391  error() << "operator `" << expr.id()
392  << "' expects single operand" << eom;
393  throw 0;
394  }
395 
397 
398  expr.type()=jsil_value_type();
399 }
400 
402 {
403  if(expr.operands().size()!=3)
404  {
405  err_location(expr);
406  error() << "operator `" << expr.id()
407  << "' expects three operands" << eom;
408  throw 0;
409  }
410 
411  make_type_compatible(expr.op0(), jsil_value_type(), true);
412  make_type_compatible(expr.op1(), string_typet(), true);
413 
414  exprt &operand3=expr.op2();
415  make_type_compatible(operand3, jsil_kind(), true);
416 
417  if(operand3.id()==ID_member)
419  else if(operand3.id()=="variable")
421  else
422  {
423  err_location(expr);
424  error() << "operator `" << expr.id()
425  << "' expects reference type in the third parameter. Got:"
426  << operand3.pretty() << eom;
427  throw 0;
428  }
429 }
430 
432 {
433  if(expr.operands().size()!=2)
434  {
435  err_location(expr);
436  error() << "operator `" << expr.id()
437  << "' expects two operands" << eom;
438  throw 0;
439  }
440 
441  make_type_compatible(expr.op0(), string_typet(), true);
442  make_type_compatible(expr.op1(), string_typet(), true);
443 
444  expr.type()=string_typet();
445 }
446 
448 {
449  if(expr.operands().size()!=2)
450  {
451  err_location(expr);
452  error() << "operator `" << expr.id()
453  << "' expects two operands" << eom;
454  throw 0;
455  }
456 
457  make_type_compatible(expr.op0(), jsil_kind(), true);
458  make_type_compatible(expr.op1(), jsil_kind(), true);
459 
460  expr.type()=bool_typet();
461 }
462 
464 {
465  if(expr.operands().size()!=2)
466  {
467  err_location(expr);
468  error() << "operator `" << expr.id()
469  << "' expects two operands" << eom;
470  throw 0;
471  }
472 
473  make_type_compatible(expr.op0(), bool_typet(), true);
474  make_type_compatible(expr.op1(), bool_typet(), true);
475 
476  expr.type()=bool_typet();
477 }
478 
480 {
481  if(expr.operands().size()!=2)
482  {
483  err_location(expr);
484  error() << "operator `" << expr.id()
485  << "' expects two operands" << eom;
486  throw 0;
487  }
488 
489 
490  make_type_compatible(expr.op0(), floatbv_typet(), true);
491  make_type_compatible(expr.op1(), floatbv_typet(), true);
492 
493  expr.type()=floatbv_typet();
494 }
495 
497 {
498  if(expr.operands().size()!=2)
499  {
500  err_location(expr);
501  error() << "operator `" << expr.id()
502  << "' expects two operands" << eom;
503  throw 0;
504  }
505 
506  // operands can be of any types
507 
508  expr.type()=bool_typet();
509 }
510 
512 {
513  if(expr.operands().size()!=2)
514  {
515  err_location(expr);
516  error() << "operator `" << expr.id()
517  << "' expects two operands" << eom;
518  throw 0;
519  }
520 
521  make_type_compatible(expr.op0(), floatbv_typet(), true);
522  make_type_compatible(expr.op1(), floatbv_typet(), true);
523 
524  expr.type()=bool_typet();
525 }
526 
528 {
529  if(expr.operands().size()!=1)
530  {
531  err_location(expr);
532  error() << "operator `" << expr.id()
533  << "' expects one operand" << eom;
534  throw 0;
535  }
536 
537  make_type_compatible(expr.op0(), bool_typet(), true);
538 
539  expr.type()=bool_typet();
540 }
541 
543 {
544  if(expr.operands().size()!=1)
545  {
546  err_location(expr);
547  error() << "operator `" << expr.id()
548  << "' expects one operand" << eom;
549  throw 0;
550  }
551 
552  make_type_compatible(expr.op0(), string_typet(), true);
553 
554  expr.type()=floatbv_typet();
555 }
556 
558 {
559  if(expr.operands().size()!=1)
560  {
561  err_location(expr);
562  error() << "operator `" << expr.id()
563  << "' expects one operand" << eom;
564  throw 0;
565  }
566 
567  make_type_compatible(expr.op0(), floatbv_typet(), true);
568 }
569 
571 {
572  irep_idt identifier=symbol_expr.get_identifier();
573 
574  // if this is a built-in identifier, check if it exists in the
575  // symbol table and retrieve it's type
576  // TODO: add a flag for not needing to prefix internal symbols
577  // that do not start with hash
578  if(has_prefix(id2string(identifier), "#") ||
579  identifier=="eval" ||
580  identifier=="nan")
581  {
582  symbol_tablet::symbolst::const_iterator s_it=
583  symbol_table.symbols.find(identifier);
584 
585  if(s_it==symbol_table.symbols.end())
586  {
587  error() << "unexpected internal symbol: " << identifier << eom;
588  throw 0;
589  }
590  else
591  {
592  // symbol already exists
593  const symbolt &symbol=s_it->second;
594 
595  // type the expression
596  symbol_expr.type()=symbol.type;
597  }
598  }
599  else
600  {
601  // if this is a variable, we need to check if we already
602  // prefixed it and add to the symbol table if it is not there already
603  irep_idt identifier_base = identifier;
604  if(!has_prefix(id2string(identifier), id2string(proc_name)))
605  {
606  identifier = add_prefix(identifier);
607  symbol_expr.set_identifier(identifier);
608  }
609 
610  symbol_tablet::symbolst::const_iterator s_it=
611  symbol_table.symbols.find(identifier);
612 
613  if(s_it==symbol_table.symbols.end())
614  {
615  // create new symbol
616  symbolt new_symbol;
617  new_symbol.name=identifier;
618  new_symbol.type=symbol_expr.type();
619  new_symbol.base_name=identifier_base;
620  new_symbol.mode="jsil";
621  new_symbol.is_type=false;
622  new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
623 
624  // mark as already typechecked
625  new_symbol.is_extern=true;
626 
627  if(symbol_table.add(new_symbol))
628  {
629  error() << "failed to add symbol `"
630  << new_symbol.name << "' in the symbol table"
631  << eom;
632  throw 0;
633  }
634  }
635  else
636  {
637  // symbol already exists
638  assert(!s_it->second.is_type);
639 
640  const symbolt &symbol=s_it->second;
641 
642  // type the expression
643  symbol_expr.type()=symbol.type;
644  }
645  }
646 }
647 
649 {
650  const irep_idt &statement=code.get_statement();
651 
652  if(statement==ID_function_call)
654  else if(statement==ID_return)
656  else if(statement==ID_expression)
657  {
658  if(code.operands().size()!=1)
659  {
660  err_location(code);
661  error() << "expression statement expected to have one operand"
662  << eom;
663  throw 0;
664  }
665 
666  typecheck_expr(code.op0());
667  }
668  else if(statement==ID_label)
669  {
670  typecheck_code(to_code_label(code).code());
671  // TODO: produce defined label set
672  }
673  else if(statement==ID_block)
674  typecheck_block(code);
675  else if(statement==ID_ifthenelse)
677  else if(statement==ID_goto)
678  {
679  // TODO: produce used label set
680  }
681  else if(statement==ID_assign)
683  else if(statement==ID_try_catch)
685  else if(statement==ID_skip)
686  {
687  }
688  else
689  {
690  err_location(code);
691  error() << "unexpected statement: " << statement << eom;
692  throw 0;
693  }
694 }
695 
697 {
698  if(code.has_return_value())
700 }
701 
703 {
704  Forall_operands(it, code)
705  typecheck_code(to_code(*it));
706 }
707 
709 {
710  // A special case of try catch with one catch clause
711  if(code.operands().size()!=3)
712  {
713  err_location(code);
714  error() << "try_catch expected to have three operands" << eom;
715  throw 0;
716  }
717 
718  // function call
720 
721  // catch decl is not used, but is required by goto-programs
722 
724 }
725 
727  code_function_callt &call)
728 {
729  if(call.operands().size()!=3)
730  {
731  err_location(call);
732  error() << "function call expected to have three operands" << eom;
733  throw 0;
734  }
735 
736  exprt &lhs=call.lhs();
737  typecheck_expr(lhs);
738 
739  exprt &f=call.function();
740  typecheck_expr(f);
741 
742  for(auto &arg : call.arguments())
743  typecheck_expr(arg);
744 
745  // Look for a function declaration symbol in the symbol table
746  if(f.id()==ID_symbol)
747  {
748  const irep_idt &id=to_symbol_expr(f).get_identifier();
749 
750  if(symbol_table.has_symbol(id))
751  {
752  symbolt &s=symbol_table.lookup(id);
753 
754  if(s.type.id()==ID_code)
755  {
757 
758  for(std::size_t i=0; i<codet.parameters().size(); i++)
759  {
760  if(i>=call.arguments().size())
761  break;
762 
763  const typet &param_type=codet.parameters()[i].type();
764 
765  if(!param_type.id().empty() && param_type.is_not_nil())
766  {
767  // check argument's type if parameter's type is given
768  make_type_compatible(call.arguments()[i], param_type, true);
769  }
770  }
771 
772  // if there are too few arguments, add undefined
773  if(codet.parameters().size()>call.arguments().size())
774  {
775  for(std::size_t i=call.arguments().size();
776  i<codet.parameters().size();
777  ++i)
778  call.arguments().push_back(
779  exprt("undefined", jsil_undefined_type()));
780  }
781 
782  // if there are too many arguments, remove
783  while(codet.parameters().size()<call.arguments().size())
784  call.arguments().pop_back();
785 
786  // check return type if exists
787  if(!codet.return_type().id().empty() &&
788  codet.return_type().is_not_nil())
789  make_type_compatible(lhs, codet.return_type(), true);
790  else make_type_compatible(lhs, jsil_any_type(), true);
791  }
792  else
793  {
794  // TODO: a symbol can be a variable evaluating to a string
795  // which corresponds to a function identifier
796  make_type_compatible(lhs, jsil_any_type(), true);
797  }
798  }
799  else
800  {
801  // Should be function, declaration not found yet
802  symbolt new_symbol;
803  new_symbol.name=id;
804  new_symbol.type=code_typet();
805  new_symbol.mode="jsil";
806  new_symbol.is_type=false;
807  new_symbol.value=exprt("no-body-just-yet");
808 
809  make_type_compatible(lhs, jsil_any_type(), true);
810 
811  if(symbol_table.add(new_symbol))
812  {
813  error().source_location=new_symbol.location;
814  error() << "failed to add expression symbol to symbol table"
815  << eom;
816  throw 0;
817  }
818  }
819  }
820  else
821  {
822  // TODO: this might be a string literal
823  // which corresponds to a function identifier
824  make_type_compatible(lhs, jsil_any_type(), true);
825  }
826 }
827 
829 {
830  exprt &cond=code.cond();
831  typecheck_expr(cond);
832  make_type_compatible(cond, bool_typet(), true);
833 
835 
836  if(!code.else_case().is_nil())
838 }
839 
841 {
842  typecheck_expr(code.op0());
843  typecheck_expr(code.op1());
844 
845  make_type_compatible(code.op0(), code.op1().type(), false);
846 }
847 
852 {
853  assert(!symbol.is_type);
854 
855  // Using is_extern to check if symbol was already typechecked
856  if(symbol.is_extern)
857  return;
858  if(symbol.value.id()!="no-body-just-yet")
859  symbol.is_extern=true;
860 
861  proc_name=symbol.name;
862  typecheck_type(symbol.type);
863 
864  if(symbol.value.id()==ID_code)
865  typecheck_code(to_code(symbol.value));
866  else if(symbol.name=="eval")
867  {
868  // No code for eval. Do nothing
869  }
870  else if(symbol.value.id()=="no-body-just-yet")
871  {
872  // Do nothing
873  }
874  else
875  {
876  error().source_location=symbol.location;
877  error() << "non-type symbol value expected code, but got "
878  << symbol.value.pretty() << eom;
879  throw 0;
880  }
881 }
882 
884 {
885  // The hash table iterators are not stable,
886  // and we might add new symbols.
887 
888  std::vector<irep_idt> identifiers;
889  identifiers.reserve(symbol_table.symbols.size());
891  identifiers.push_back(s_it->first);
892 
893  // We first check all type symbols,
894  // recursively doing base classes first.
895  for(const irep_idt &id : identifiers)
896  {
897  symbolt &symbol=symbol_table.symbols[id];
898 
899  if(symbol.is_type)
900  typecheck_type_symbol(symbol);
901  }
902 
903  // We now check all non-type symbols
904  for(const irep_idt &id : identifiers)
905  {
906  symbolt &symbol=symbol_table.symbols[id];
907 
908  if(!symbol.is_type)
910  }
911 }
912 
916 {
917  jsil_typecheckt jsil_typecheck(symbol_table, message_handler);
918  return jsil_typecheck.typecheck_main();
919 }
920 
922  exprt &expr,
924  const namespacet &ns)
925 {
926  const unsigned errors_before=
927  message_handler.get_message_count(messaget::M_ERROR);
928 
930 
932  symbol_table,
933  message_handler);
934 
935  try
936  {
937  jsil_typecheck.typecheck_expr(expr);
938  }
939 
940  catch(int e)
941  {
942  jsil_typecheck.error();
943  }
944 
945  catch(const char *e)
946  {
947  jsil_typecheck.error() << e << messaget::eom;
948  }
949 
950  catch(const std::string &e)
951  {
952  jsil_typecheck.error() << e << messaget::eom;
953  }
954 
955  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
956 }
const irep_idt & get_statement() const
Definition: std_code.h:37
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_constant(exprt &expr)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const codet & then_case() const
Definition: std_code.h:370
const exprt & return_value() const
Definition: std_code.h:728
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Jsil Language.
void typecheck_expr_proto_obj(exprt &expr)
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Definition: expr2jsil.cpp:24
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:163
A try/catch block.
Definition: std_code.h:1160
void typecheck_expr_unary_num(exprt &expr)
codet & get_catch_code(unsigned i)
Definition: std_code.h:1190
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void typecheck_expr_base(exprt &expr)
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
irep_idt mode
Language mode.
Definition: symbol.h:55
const exprt & cond() const
Definition: std_code.h:360
void typecheck_expr_ref(exprt &expr)
void typecheck_expr_binary_arith(exprt &expr)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
void typecheck_assign(code_assignt &code)
Jsil Language.
exprt value
Initial value of symbol.
Definition: symbol.h:40
const namespacet ns
void typecheck_expr_main(exprt &expr)
typet & type()
Definition: expr.h:60
void typecheck_function_call(code_function_callt &function_call)
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
A side effect that throws an exception.
Definition: std_code.h:1100
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
irep_idt proc_name
void typecheck_exp_binary_equal(exprt &expr)
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:33
virtual std::string to_string(const exprt &expr)
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
typet jsil_null_type()
Definition: jsil_types.cpp:96
bool is_jsil_spec_code_type(const typet &type)
Definition: jsil_types.h:78
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_concatenation(exprt &expr)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
void typecheck_code(codet &code)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:131
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void typecheck_expr_unary_boolean(exprt &expr)
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:137
void typecheck_return(code_returnt &code)
source_locationt source_location
Definition: message.h:175
typet jsil_reference_type()
Definition: jsil_types.cpp:60
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
typet jsil_undefined_type()
Definition: jsil_types.cpp:101
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
void typecheck_type_symbol(symbolt &symbol)
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1114
typet jsil_any_type()
Definition: jsil_types.cpp:16
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
typet jsil_kind()
Definition: jsil_types.cpp:106
void err_location(const source_locationt &loc)
Definition: typecheck.h:27
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_subtype(exprt &expr)
Jsil Language.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:73
Symbol table.
void typecheck_expr_proto_field(exprt &expr)
bool has_return_value() const
Definition: std_code.h:738
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void typecheck_type(typet &type)
bool is_jsil_builtin_code_type(const typet &type)
Definition: jsil_types.h:55
bool is_extern
Definition: symbol.h:71
void make_type_compatible(exprt &expr, const typet &type, bool must)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
void typecheck_expr_unary_string(exprt &expr)
void typecheck_block(codet &code)
exprt & function()
Definition: std_code.h:677
typet jsil_object_type()
Definition: jsil_types.cpp:78
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:116
std::string type2jsil(const typet &type, const namespacet &ns)
Definition: expr2jsil.cpp:31
codet & try_code()
Definition: std_code.h:1168
Base class for all expressions.
Definition: expr.h:46
typet jsil_member_reference_type()
Definition: jsil_types.cpp:68
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void typecheck_expr_operands(exprt &expr)
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:25
typet jsil_value_type()
Definition: jsil_types.cpp:41
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
#define Forall_operands(it, expr)
Definition: expr.h:23
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
typet jsil_empty_type()
Definition: jsil_types.cpp:111
mstreamt & error()
Definition: message.h:223
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
symbol_tablet & symbol_table
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
typet jsil_user_object_type()
Definition: jsil_types.cpp:86
void typecheck_expr_delete(exprt &expr)
A statement in a programming language.
Definition: std_code.h:19
Return from a function.
Definition: std_code.h:714
bool is_type
Definition: symbol.h:66
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
operandst & operands()
Definition: expr.h:70
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:1210
const codet & else_case() const
Definition: std_code.h:380
message_handlert * message_handler
Definition: message.h:259
void typecheck_expr_binary_compare(exprt &expr)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
bool empty() const
Definition: dstring.h:61
void typecheck_ifthenelse(code_ifthenelset &code)
virtual bool typecheck_main()
Definition: typecheck.cpp:12
void typecheck_expr_field(exprt &expr)
const typet & return_type() const
Definition: std_types.h:831
Assignment.
Definition: std_code.h:144
void typecheck_expr_has_field(exprt &expr)
void typecheck_try_catch(code_try_catcht &code)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
virtual void typecheck()
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
bool is_lvalue
Definition: symbol.h:71
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_index(exprt &expr)
unsigned get_message_count(unsigned level) const
Definition: message.h:47