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  const auto maybe_symbol=symbol_table.get_writeable(id);
46  if(!maybe_symbol)
47  {
48  error() << "unexpected symbol: " << id << eom;
49  throw 0;
50  }
51 
52  symbolt &s=*maybe_symbol;
53  if(s.type.id().empty() || s.type.is_nil())
54  s.type=type;
55  else
56  s.type=jsil_union(s.type, type);
57  }
58 }
59 
61  exprt &expr,
62  const typet &type,
63  bool must)
64 {
65  if(type.id().empty() || type.is_nil())
66  {
68  error() << "make_type_compatible got empty type: " << expr.pretty() << eom;
69  throw 0;
70  }
71 
72  if(expr.type().id().empty() || expr.type().is_nil())
73  {
74  // Type is not yet set
75  update_expr_type(expr, type);
76  return;
77  }
78 
79  if(must)
80  {
81  if(jsil_incompatible_types(expr.type(), type))
82  {
84  error() << "failed to typecheck expr "
85  << expr.pretty() << " with type "
86  << expr.type().pretty()
87  << "; required type " << type.pretty() << eom;
88  throw 0;
89  }
90  }
91  else if(!jsil_is_subtype(type, expr.type()))
92  {
93  // Types are not compatible
94  typet upper=jsil_union(expr.type(), type);
95  update_expr_type(expr, upper);
96  }
97 }
98 
100 {
101  if(type.id()==ID_code)
102  {
103  code_typet &parameters=to_code_type(type);
104 
105  for(code_typet::parametert &p : parameters.parameters())
106  {
107  // create new symbol
108  parameter_symbolt new_symbol;
109  new_symbol.base_name=p.get_identifier();
110 
111  // append procedure name to parameters
112  p.set_identifier(add_prefix(p.get_identifier()));
113  new_symbol.name=p.get_identifier();
114 
115  if(is_jsil_builtin_code_type(type))
116  new_symbol.type=jsil_value_or_empty_type();
117  else if(is_jsil_spec_code_type(type))
118  new_symbol.type=jsil_value_or_reference_type();
119  else
120  new_symbol.type=jsil_value_type(); // User defined function
121 
122  new_symbol.mode="jsil";
123 
124  // mark as already typechecked
125  new_symbol.is_extern=true;
126 
127  if(symbol_table.add(new_symbol))
128  {
129  error() << "failed to add parameter symbol `"
130  << new_symbol.name << "' in the symbol table" << eom;
131  throw 0;
132  }
133  }
134  }
135 }
136 
138 {
139  // first do sub-nodes
141 
142  // now do case-split
143  typecheck_expr_main(expr);
144 }
145 
147 {
148  Forall_operands(it, expr)
149  typecheck_expr(*it);
150 }
151 
153 {
154  if(expr.id()==ID_code)
155  {
157  error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
158  throw 0;
159  }
160  else if(expr.id()==ID_symbol)
162  else if(expr.id()==ID_constant)
163  {
164  }
165  else
166  {
167  // expressions are expected not to have type set just yet
168  assert(expr.type().is_nil() || expr.type().id().empty());
169 
170  if(expr.id()==ID_null ||
171  expr.id()=="undefined" ||
172  expr.id()==ID_empty)
174  else if(expr.id()=="null_type" ||
175  expr.id()=="undefined_type" ||
176  expr.id()==ID_boolean ||
177  expr.id()==ID_string ||
178  expr.id()=="number" ||
179  expr.id()=="builtin_object" ||
180  expr.id()=="user_object" ||
181  expr.id()=="object" ||
182  expr.id()==ID_pointer ||
183  expr.id()==ID_member ||
184  expr.id()=="variable")
185  expr.type()=jsil_kind();
186  else if(expr.id()=="proto" ||
187  expr.id()=="fid" ||
188  expr.id()=="scope" ||
189  expr.id()=="constructid" ||
190  expr.id()=="primvalue" ||
191  expr.id()=="targetfunction" ||
192  expr.id()==ID_class)
193  {
194  // TODO: have a special type for builtin fields
195  expr.type()=string_typet();
196  }
197  else if(expr.id()==ID_not)
199  else if(expr.id()=="string_to_num")
201  else if(expr.id()==ID_unary_minus ||
202  expr.id()=="num_to_int32" ||
203  expr.id()=="num_to_uint32" ||
204  expr.id()==ID_bitnot)
205  {
207  expr.type()=floatbv_typet();
208  }
209  else if(expr.id()=="num_to_string")
210  {
212  expr.type()=string_typet();
213  }
214  else if(expr.id()==ID_equal)
216  else if(expr.id()==ID_lt ||
217  expr.id()==ID_le)
219  else if(expr.id()==ID_plus ||
220  expr.id()==ID_minus ||
221  expr.id()==ID_mult ||
222  expr.id()==ID_div ||
223  expr.id()==ID_mod ||
224  expr.id()==ID_bitand ||
225  expr.id()==ID_bitor ||
226  expr.id()==ID_bitxor ||
227  expr.id()==ID_shl ||
228  expr.id()==ID_shr ||
229  expr.id()==ID_lshr)
231  else if(expr.id()==ID_and ||
232  expr.id()==ID_or)
234  else if(expr.id()=="subtype_of")
236  else if(expr.id()==ID_concatenation)
238  else if(expr.id()=="ref")
239  typecheck_expr_ref(expr);
240  else if(expr.id()=="field")
241  typecheck_expr_field(expr);
242  else if(expr.id()==ID_base)
243  typecheck_expr_base(expr);
244  else if(expr.id()==ID_typeof)
245  expr.type()=jsil_kind();
246  else if(expr.id()=="new")
247  expr.type()=jsil_user_object_type();
248  else if(expr.id()=="hasField")
250  else if(expr.id()==ID_index)
251  typecheck_expr_index(expr);
252  else if(expr.id()=="delete")
253  typecheck_expr_delete(expr);
254  else if(expr.id()=="protoField")
256  else if(expr.id()=="protoObj")
258  else if(expr.id()==ID_side_effect)
260  else
261  {
263  error() << "unexpected expression: " << expr.pretty() << eom;
264  throw 0;
265  }
266  }
267 }
268 
271 {
272  irept &excep_list=expr.add(ID_exception_list);
273  assert(excep_list.id()==ID_symbol);
274  symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
276 }
277 
279 {
280  if(expr.id()==ID_null)
281  expr.type()=jsil_null_type();
282  else if(expr.id()=="undefined")
283  expr.type()=jsil_undefined_type();
284  else if(expr.id()==ID_empty)
285  expr.type()=jsil_empty_type();
286 }
287 
289 {
290  if(expr.operands().size()!=2)
291  {
293  error() << "operator `" << expr.id()
294  << "' expects two operands" << eom;
295  throw 0;
296  }
297 
298  make_type_compatible(expr.op0(), jsil_object_type(), true);
299  make_type_compatible(expr.op1(), string_typet(), true);
300 
302 }
303 
305 {
306  if(expr.operands().size()!=2)
307  {
309  error() << "operator `" << expr.id()
310  << "' expects two operands";
311  throw 0;
312  }
313 
314  make_type_compatible(expr.op0(), jsil_object_type(), true);
315  make_type_compatible(expr.op1(), jsil_object_type(), true);
316 
317  expr.type()=bool_typet();
318 }
319 
321 {
322  if(expr.operands().size()!=2)
323  {
325  error() << "operator `" << expr.id()
326  << "' expects two operands" << eom;
327  throw 0;
328  }
329 
330  make_type_compatible(expr.op0(), jsil_object_type(), true);
331  make_type_compatible(expr.op1(), string_typet(), true);
332 
333  expr.type()=bool_typet();
334 }
335 
337 {
338  if(expr.operands().size()!=2)
339  {
341  error() << "operator `" << expr.id()
342  << "' expects two operands" << eom;
343  throw 0;
344  }
345 
346  make_type_compatible(expr.op0(), jsil_object_type(), true);
347  make_type_compatible(expr.op1(), string_typet(), true);
348 
349  // special case for function identifiers
350  if(expr.op1().id()=="fid" || expr.op1().id()=="constructid")
351  expr.type()=code_typet();
352  else
353  expr.type()=jsil_value_type();
354 }
355 
357 {
358  if(expr.operands().size()!=2)
359  {
361  error() << "operator `" << expr.id()
362  << "' expects two operands" << eom;
363  throw 0;
364  }
365 
366  make_type_compatible(expr.op0(), jsil_object_type(), true);
367  make_type_compatible(expr.op1(), string_typet(), true);
368 
369  expr.type()=bool_typet();
370 }
371 
373 {
374  if(expr.operands().size()!=1)
375  {
377  error() << "operator `" << expr.id()
378  << "' expects single operand" << eom;
379  throw 0;
380  }
381 
383 
384  expr.type()=string_typet();
385 }
386 
388 {
389  if(expr.operands().size()!=1)
390  {
392  error() << "operator `" << expr.id()
393  << "' expects single operand" << eom;
394  throw 0;
395  }
396 
398 
399  expr.type()=jsil_value_type();
400 }
401 
403 {
404  if(expr.operands().size()!=3)
405  {
407  error() << "operator `" << expr.id()
408  << "' expects three operands" << eom;
409  throw 0;
410  }
411 
412  make_type_compatible(expr.op0(), jsil_value_type(), true);
413  make_type_compatible(expr.op1(), string_typet(), true);
414 
415  exprt &operand3=expr.op2();
416  make_type_compatible(operand3, jsil_kind(), true);
417 
418  if(operand3.id()==ID_member)
420  else if(operand3.id()=="variable")
422  else
423  {
425  error() << "operator `" << expr.id()
426  << "' expects reference type in the third parameter. Got:"
427  << operand3.pretty() << eom;
428  throw 0;
429  }
430 }
431 
433 {
434  if(expr.operands().size()!=2)
435  {
437  error() << "operator `" << expr.id()
438  << "' expects two operands" << eom;
439  throw 0;
440  }
441 
442  make_type_compatible(expr.op0(), string_typet(), true);
443  make_type_compatible(expr.op1(), string_typet(), true);
444 
445  expr.type()=string_typet();
446 }
447 
449 {
450  if(expr.operands().size()!=2)
451  {
453  error() << "operator `" << expr.id()
454  << "' expects two operands" << eom;
455  throw 0;
456  }
457 
458  make_type_compatible(expr.op0(), jsil_kind(), true);
459  make_type_compatible(expr.op1(), jsil_kind(), true);
460 
461  expr.type()=bool_typet();
462 }
463 
465 {
466  if(expr.operands().size()!=2)
467  {
469  error() << "operator `" << expr.id()
470  << "' expects two operands" << eom;
471  throw 0;
472  }
473 
474  make_type_compatible(expr.op0(), bool_typet(), true);
475  make_type_compatible(expr.op1(), bool_typet(), true);
476 
477  expr.type()=bool_typet();
478 }
479 
481 {
482  if(expr.operands().size()!=2)
483  {
485  error() << "operator `" << expr.id()
486  << "' expects two operands" << eom;
487  throw 0;
488  }
489 
490 
491  make_type_compatible(expr.op0(), floatbv_typet(), true);
492  make_type_compatible(expr.op1(), floatbv_typet(), true);
493 
494  expr.type()=floatbv_typet();
495 }
496 
498 {
499  if(expr.operands().size()!=2)
500  {
502  error() << "operator `" << expr.id()
503  << "' expects two operands" << eom;
504  throw 0;
505  }
506 
507  // operands can be of any types
508 
509  expr.type()=bool_typet();
510 }
511 
513 {
514  if(expr.operands().size()!=2)
515  {
517  error() << "operator `" << expr.id()
518  << "' expects two operands" << eom;
519  throw 0;
520  }
521 
522  make_type_compatible(expr.op0(), floatbv_typet(), true);
523  make_type_compatible(expr.op1(), floatbv_typet(), true);
524 
525  expr.type()=bool_typet();
526 }
527 
529 {
530  if(expr.operands().size()!=1)
531  {
533  error() << "operator `" << expr.id()
534  << "' expects one operand" << eom;
535  throw 0;
536  }
537 
538  make_type_compatible(expr.op0(), bool_typet(), true);
539 
540  expr.type()=bool_typet();
541 }
542 
544 {
545  if(expr.operands().size()!=1)
546  {
548  error() << "operator `" << expr.id()
549  << "' expects one operand" << eom;
550  throw 0;
551  }
552 
553  make_type_compatible(expr.op0(), string_typet(), true);
554 
555  expr.type()=floatbv_typet();
556 }
557 
559 {
560  if(expr.operands().size()!=1)
561  {
563  error() << "operator `" << expr.id()
564  << "' expects one operand" << eom;
565  throw 0;
566  }
567 
568  make_type_compatible(expr.op0(), floatbv_typet(), true);
569 }
570 
572 {
573  irep_idt identifier=symbol_expr.get_identifier();
574 
575  // if this is a built-in identifier, check if it exists in the
576  // symbol table and retrieve it's type
577  // TODO: add a flag for not needing to prefix internal symbols
578  // that do not start with hash
579  if(has_prefix(id2string(identifier), "#") ||
580  identifier=="eval" ||
581  identifier=="nan")
582  {
583  symbol_tablet::symbolst::const_iterator s_it=
584  symbol_table.symbols.find(identifier);
585 
586  if(s_it==symbol_table.symbols.end())
587  {
588  error() << "unexpected internal symbol: " << identifier << eom;
589  throw 0;
590  }
591  else
592  {
593  // symbol already exists
594  const symbolt &symbol=s_it->second;
595 
596  // type the expression
597  symbol_expr.type()=symbol.type;
598  }
599  }
600  else
601  {
602  // if this is a variable, we need to check if we already
603  // prefixed it and add to the symbol table if it is not there already
604  irep_idt identifier_base = identifier;
605  if(!has_prefix(id2string(identifier), id2string(proc_name)))
606  {
607  identifier = add_prefix(identifier);
608  symbol_expr.set_identifier(identifier);
609  }
610 
611  symbol_tablet::symbolst::const_iterator s_it=
612  symbol_table.symbols.find(identifier);
613 
614  if(s_it==symbol_table.symbols.end())
615  {
616  // create new symbol
617  symbolt new_symbol;
618  new_symbol.name=identifier;
619  new_symbol.type=symbol_expr.type();
620  new_symbol.base_name=identifier_base;
621  new_symbol.mode="jsil";
622  new_symbol.is_type=false;
623  new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
624 
625  // mark as already typechecked
626  new_symbol.is_extern=true;
627 
628  if(symbol_table.add(new_symbol))
629  {
630  error() << "failed to add symbol `"
631  << new_symbol.name << "' in the symbol table"
632  << eom;
633  throw 0;
634  }
635  }
636  else
637  {
638  // symbol already exists
639  assert(!s_it->second.is_type);
640 
641  const symbolt &symbol=s_it->second;
642 
643  // type the expression
644  symbol_expr.type()=symbol.type;
645  }
646  }
647 }
648 
650 {
651  const irep_idt &statement=code.get_statement();
652 
653  if(statement==ID_function_call)
655  else if(statement==ID_return)
657  else if(statement==ID_expression)
658  {
659  if(code.operands().size()!=1)
660  {
662  error() << "expression statement expected to have one operand"
663  << eom;
664  throw 0;
665  }
666 
667  typecheck_expr(code.op0());
668  }
669  else if(statement==ID_label)
670  {
671  typecheck_code(to_code_label(code).code());
672  // TODO: produce defined label set
673  }
674  else if(statement==ID_block)
675  typecheck_block(code);
676  else if(statement==ID_ifthenelse)
678  else if(statement==ID_goto)
679  {
680  // TODO: produce used label set
681  }
682  else if(statement==ID_assign)
684  else if(statement==ID_try_catch)
686  else if(statement==ID_skip)
687  {
688  }
689  else
690  {
692  error() << "unexpected statement: " << statement << eom;
693  throw 0;
694  }
695 }
696 
698 {
699  if(code.has_return_value())
701 }
702 
704 {
705  Forall_operands(it, code)
706  typecheck_code(to_code(*it));
707 }
708 
710 {
711  // A special case of try catch with one catch clause
712  if(code.operands().size()!=3)
713  {
715  error() << "try_catch expected to have three operands" << eom;
716  throw 0;
717  }
718 
719  // function call
721 
722  // catch decl is not used, but is required by goto-programs
723 
725 }
726 
728  code_function_callt &call)
729 {
730  if(call.operands().size()!=3)
731  {
733  error() << "function call expected to have three operands" << eom;
734  throw 0;
735  }
736 
737  exprt &lhs=call.lhs();
738  typecheck_expr(lhs);
739 
740  exprt &f=call.function();
741  typecheck_expr(f);
742 
743  for(auto &arg : call.arguments())
744  typecheck_expr(arg);
745 
746  // Look for a function declaration symbol in the symbol table
747  if(f.id()==ID_symbol)
748  {
749  const irep_idt &id=to_symbol_expr(f).get_identifier();
750 
751  if(const auto maybe_symbol=symbol_table.lookup(id))
752  {
753  const symbolt &s=*maybe_symbol;
754 
755  if(s.type.id()==ID_code)
756  {
757  const code_typet &codet=to_code_type(s.type);
758 
759  for(std::size_t i=0; i<codet.parameters().size(); i++)
760  {
761  if(i>=call.arguments().size())
762  break;
763 
764  const typet &param_type=codet.parameters()[i].type();
765 
766  if(!param_type.id().empty() && param_type.is_not_nil())
767  {
768  // check argument's type if parameter's type is given
769  make_type_compatible(call.arguments()[i], param_type, true);
770  }
771  }
772 
773  // if there are too few arguments, add undefined
774  if(codet.parameters().size()>call.arguments().size())
775  {
776  for(std::size_t i=call.arguments().size();
777  i<codet.parameters().size();
778  ++i)
779  call.arguments().push_back(
780  exprt("undefined", jsil_undefined_type()));
781  }
782 
783  // if there are too many arguments, remove
784  while(codet.parameters().size()<call.arguments().size())
785  call.arguments().pop_back();
786 
787  // check return type if exists
788  if(!codet.return_type().id().empty() &&
789  codet.return_type().is_not_nil())
790  make_type_compatible(lhs, codet.return_type(), true);
791  else make_type_compatible(lhs, jsil_any_type(), true);
792  }
793  else
794  {
795  // TODO: a symbol can be a variable evaluating to a string
796  // which corresponds to a function identifier
797  make_type_compatible(lhs, jsil_any_type(), true);
798  }
799  }
800  else
801  {
802  // Should be function, declaration not found yet
803  symbolt new_symbol;
804  new_symbol.name=id;
805  new_symbol.type=code_typet();
806  new_symbol.mode="jsil";
807  new_symbol.is_type=false;
808  new_symbol.value=exprt("no-body-just-yet");
809 
810  make_type_compatible(lhs, jsil_any_type(), true);
811 
812  if(symbol_table.add(new_symbol))
813  {
814  error().source_location=new_symbol.location;
815  error() << "failed to add expression symbol to symbol table"
816  << eom;
817  throw 0;
818  }
819  }
820  }
821  else
822  {
823  // TODO: this might be a string literal
824  // which corresponds to a function identifier
825  make_type_compatible(lhs, jsil_any_type(), true);
826  }
827 }
828 
830 {
831  exprt &cond=code.cond();
832  typecheck_expr(cond);
833  make_type_compatible(cond, bool_typet(), true);
834 
835  typecheck_code(code.then_case());
836 
837  if(!code.else_case().is_nil())
838  typecheck_code(code.else_case());
839 }
840 
842 {
843  typecheck_expr(code.op0());
844  typecheck_expr(code.op1());
845 
846  make_type_compatible(code.op0(), code.op1().type(), false);
847 }
848 
853 {
854  assert(!symbol.is_type);
855 
856  // Using is_extern to check if symbol was already typechecked
857  if(symbol.is_extern)
858  return;
859  if(symbol.value.id()!="no-body-just-yet")
860  symbol.is_extern=true;
861 
862  proc_name=symbol.name;
863  typecheck_type(symbol.type);
864 
865  if(symbol.value.id()==ID_code)
866  typecheck_code(to_code(symbol.value));
867  else if(symbol.name=="eval")
868  {
869  // No code for eval. Do nothing
870  }
871  else if(symbol.value.id()=="no-body-just-yet")
872  {
873  // Do nothing
874  }
875  else
876  {
877  error().source_location=symbol.location;
878  error() << "non-type symbol value expected code, but got "
879  << symbol.value.pretty() << eom;
880  throw 0;
881  }
882 }
883 
885 {
886  // The hash table iterators are not stable,
887  // and we might add new symbols.
888 
889  std::vector<irep_idt> identifiers;
890  identifiers.reserve(symbol_table.symbols.size());
891  for(const auto &symbol_pair : symbol_table.symbols)
892  {
893  identifiers.push_back(symbol_pair.first);
894  }
895 
896  // We first check all type symbols,
897  // recursively doing base classes first.
898  for(const irep_idt &id : identifiers)
899  {
900  symbolt &symbol=*symbol_table.get_writeable(id);
901  if(symbol.is_type)
902  typecheck_type_symbol(symbol);
903  }
904 
905  // We now check all non-type symbols
906  for(const irep_idt &id : identifiers)
907  {
908  symbolt &symbol=*symbol_table.get_writeable(id);
909  if(!symbol.is_type)
911  }
912 }
913 
915  symbol_tablet &symbol_table,
916  message_handlert &message_handler)
917 {
918  jsil_typecheckt jsil_typecheck(symbol_table, message_handler);
919  return jsil_typecheck.typecheck_main();
920 }
921 
923  exprt &expr,
924  message_handlert &message_handler,
925  const namespacet &)
926 {
927  const unsigned errors_before=
928  message_handler.get_message_count(messaget::M_ERROR);
929 
930  symbol_tablet symbol_table;
931 
933  symbol_table,
934  message_handler);
935 
936  try
937  {
938  jsil_typecheck.typecheck_expr(expr);
939  }
940 
941  catch(int)
942  {
943  jsil_typecheck.error();
944  }
945 
946  catch(const char *e)
947  {
948  jsil_typecheck.error() << e << messaget::eom;
949  }
950 
951  catch(const std::string &e)
952  {
953  jsil_typecheck.error() << e << messaget::eom;
954  }
955 
956  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
957 }
const irep_idt & get_statement() const
Definition: std_code.h:56
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_constant(exprt &expr)
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const codet & then_case() const
Definition: std_code.h:652
const exprt & return_value() const
Definition: std_code.h:1205
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
Jsil Language.
void typecheck_expr_proto_obj(exprt &expr)
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:172
codet representation of a try/catch block.
Definition: std_code.h:2007
void typecheck_expr_unary_num(exprt &expr)
codet & get_catch_code(unsigned i)
Definition: std_code.h:2044
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
void typecheck_expr_base(exprt &expr)
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
irep_idt mode
Language mode.
Definition: symbol.h:49
const exprt & cond() const
Definition: std_code.h:642
void typecheck_expr_ref(exprt &expr)
void typecheck_expr_binary_arith(exprt &expr)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_identifier() const
Definition: std_expr.h:176
void typecheck_assign(code_assignt &code)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
Jsil Language.
exprt value
Initial value of symbol.
Definition: symbol.h:34
const namespacet ns
void typecheck_expr_main(exprt &expr)
typet & type()
Return the type of the expression.
Definition: expr.h:68
void typecheck_function_call(code_function_callt &function_call)
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1792
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:27
virtual std::string to_string(const exprt &expr)
String type.
Definition: std_types.h:1662
typet jsil_null_type()
Definition: jsil_types.cpp:78
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:334
const irep_idt & id() const
Definition: irep.h:259
void typecheck_code(codet &code)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:113
argumentst & arguments()
Definition: std_code.h:1109
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:119
void typecheck_return(code_returnt &code)
source_locationt source_location
Definition: message.h:236
typet jsil_reference_type()
Definition: jsil_types.cpp:46
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:386
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
typet jsil_undefined_type()
Definition: jsil_types.cpp:83
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1819
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
typet jsil_any_type()
Definition: jsil_types.cpp:16
Base class for tree-like data structures with sharing.
Definition: irep.h:156
codet representation of a function call statement.
Definition: std_code.h:1036
typet jsil_kind()
Definition: jsil_types.cpp:88
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_subtype(exprt &expr)
Jsil Language.
void typecheck_type_symbol(symbolt &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:57
Author: Diffblue Ltd.
const symbolst & symbols
void typecheck_expr_proto_field(exprt &expr)
bool has_return_value() const
Definition: std_code.h:1215
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:66
static eomt eom
Definition: message.h:284
void make_type_compatible(exprt &expr, const typet &type, bool must)
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
void typecheck_expr_unary_string(exprt &expr)
void typecheck_block(codet &code)
symbol_table_baset & symbol_table
exprt & function()
Definition: std_code.h:1099
typet jsil_object_type()
Definition: jsil_types.cpp:62
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:98
std::string type2jsil(const typet &type, const namespacet &ns)
Definition: expr2jsil.cpp:31
codet & try_code()
Definition: std_code.h:2022
Base class for all expressions.
Definition: expr.h:54
typet jsil_member_reference_type()
Definition: jsil_types.cpp:52
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void typecheck_expr_operands(exprt &expr)
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:22
typet jsil_value_type()
Definition: jsil_types.cpp:32
const source_locationt & source_location() const
Definition: expr.h:228
std::size_t get_message_count(unsigned level) const
Definition: message.h:51
irept & add(const irep_namet &name)
Definition: irep.cpp:305
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
#define Forall_operands(it, expr)
Definition: expr.h:26
typet jsil_empty_type()
Definition: jsil_types.cpp:93
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
codet representation of an if-then-else statement.
Definition: std_code.h:614
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
typet jsil_user_object_type()
Definition: jsil_types.cpp:68
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void typecheck_expr_delete(exprt &expr)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
bool is_type
Definition: symbol.h:61
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1310
operandst & operands()
Definition: expr.h:78
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2072
const codet & else_case() const
Definition: std_code.h:662
void typecheck_expr_binary_compare(exprt &expr)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:688
bool empty() const
Definition: dstring.h:75
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_field(exprt &expr)
A codet representing an assignment in the program.
Definition: std_code.h:256
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:1173
virtual void typecheck()
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
bool is_lvalue
Definition: symbol.h:66
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_index(exprt &expr)