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 '" << new_symbol.name
130  << "' 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() << "' expects two operands" << eom;
294  throw 0;
295  }
296 
298  make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true);
299 
301 }
302 
304 {
305  if(expr.operands().size()!=2)
306  {
308  error() << "operator '" << expr.id() << "' expects two operands";
309  throw 0;
310  }
311 
314 
315  expr.type()=bool_typet();
316 }
317 
319 {
320  if(expr.operands().size()!=2)
321  {
323  error() << "operator '" << expr.id() << "' expects two operands" << eom;
324  throw 0;
325  }
326 
328  make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true);
329 
330  expr.type()=bool_typet();
331 }
332 
334 {
335  if(expr.operands().size()!=2)
336  {
338  error() << "operator '" << expr.id() << "' expects two operands" << eom;
339  throw 0;
340  }
341 
343  make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true);
344 
345  // special case for function identifiers
346  if(
347  to_binary_expr(expr).op1().id() == "fid" ||
348  to_binary_expr(expr).op1().id() == "constructid")
349  expr.type() = code_typet({}, typet());
350  else
351  expr.type()=jsil_value_type();
352 }
353 
355 {
356  if(expr.operands().size()!=2)
357  {
359  error() << "operator '" << expr.id() << "' expects two operands" << eom;
360  throw 0;
361  }
362 
364  make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true);
365 
366  expr.type()=bool_typet();
367 }
368 
370 {
371  if(expr.operands().size()!=1)
372  {
374  error() << "operator '" << expr.id() << "' expects single operand" << eom;
375  throw 0;
376  }
377 
379 
380  expr.type()=string_typet();
381 }
382 
384 {
385  if(expr.operands().size()!=1)
386  {
388  error() << "operator '" << expr.id() << "' expects single operand" << eom;
389  throw 0;
390  }
391 
393 
394  expr.type()=jsil_value_type();
395 }
396 
398 {
399  if(expr.operands().size()!=3)
400  {
402  error() << "operator '" << expr.id() << "' expects three operands" << eom;
403  throw 0;
404  }
405 
408 
409  exprt &operand3 = to_multi_ary_expr(expr).op2();
410  make_type_compatible(operand3, jsil_kind(), true);
411 
412  if(operand3.id()==ID_member)
414  else if(operand3.id()=="variable")
416  else
417  {
419  error() << "operator '" << expr.id()
420  << "' expects reference type in the third parameter. Got:"
421  << operand3.pretty() << eom;
422  throw 0;
423  }
424 }
425 
427 {
428  if(expr.operands().size()!=2)
429  {
431  error() << "operator '" << expr.id() << "' expects two operands" << eom;
432  throw 0;
433  }
434 
435  make_type_compatible(to_binary_expr(expr).op0(), string_typet(), true);
436  make_type_compatible(to_binary_expr(expr).op1(), string_typet(), true);
437 
438  expr.type()=string_typet();
439 }
440 
442 {
443  if(expr.operands().size()!=2)
444  {
446  error() << "operator '" << expr.id() << "' expects two operands" << eom;
447  throw 0;
448  }
449 
450  make_type_compatible(to_binary_expr(expr).op0(), jsil_kind(), true);
451  make_type_compatible(to_binary_expr(expr).op1(), jsil_kind(), true);
452 
453  expr.type()=bool_typet();
454 }
455 
457 {
458  if(expr.operands().size()!=2)
459  {
461  error() << "operator '" << expr.id() << "' expects two operands" << eom;
462  throw 0;
463  }
464 
465  make_type_compatible(to_binary_expr(expr).op0(), bool_typet(), true);
466  make_type_compatible(to_binary_expr(expr).op1(), bool_typet(), true);
467 
468  expr.type()=bool_typet();
469 }
470 
472 {
473  if(expr.operands().size()!=2)
474  {
476  error() << "operator '" << expr.id() << "' expects two operands" << eom;
477  throw 0;
478  }
479 
480  make_type_compatible(to_binary_expr(expr).op0(), floatbv_typet(), true);
481  make_type_compatible(to_binary_expr(expr).op1(), floatbv_typet(), true);
482 
483  expr.type()=floatbv_typet();
484 }
485 
487 {
488  if(expr.operands().size()!=2)
489  {
491  error() << "operator '" << expr.id() << "' expects two operands" << eom;
492  throw 0;
493  }
494 
495  // operands can be of any types
496 
497  expr.type()=bool_typet();
498 }
499 
501 {
502  if(expr.operands().size()!=2)
503  {
505  error() << "operator '" << expr.id() << "' expects two operands" << eom;
506  throw 0;
507  }
508 
509  make_type_compatible(to_binary_expr(expr).op0(), floatbv_typet(), true);
510  make_type_compatible(to_binary_expr(expr).op1(), floatbv_typet(), true);
511 
512  expr.type()=bool_typet();
513 }
514 
516 {
517  if(expr.operands().size()!=1)
518  {
520  error() << "operator '" << expr.id() << "' expects one operand" << eom;
521  throw 0;
522  }
523 
524  make_type_compatible(to_unary_expr(expr).op(), bool_typet(), true);
525 
526  expr.type()=bool_typet();
527 }
528 
530 {
531  if(expr.operands().size()!=1)
532  {
534  error() << "operator '" << expr.id() << "' expects one operand" << eom;
535  throw 0;
536  }
537 
538  make_type_compatible(to_unary_expr(expr).op(), string_typet(), true);
539 
540  expr.type()=floatbv_typet();
541 }
542 
544 {
545  if(expr.operands().size()!=1)
546  {
548  error() << "operator '" << expr.id() << "' expects one operand" << eom;
549  throw 0;
550  }
551 
552  make_type_compatible(to_unary_expr(expr).op(), floatbv_typet(), true);
553 }
554 
556 {
557  irep_idt identifier=symbol_expr.get_identifier();
558 
559  // if this is a built-in identifier, check if it exists in the
560  // symbol table and retrieve it's type
561  // TODO: add a flag for not needing to prefix internal symbols
562  // that do not start with hash
563  if(has_prefix(id2string(identifier), "#") ||
564  identifier=="eval" ||
565  identifier=="nan")
566  {
567  symbol_tablet::symbolst::const_iterator s_it=
568  symbol_table.symbols.find(identifier);
569 
570  if(s_it==symbol_table.symbols.end())
571  {
572  error() << "unexpected internal symbol: " << identifier << eom;
573  throw 0;
574  }
575  else
576  {
577  // symbol already exists
578  const symbolt &symbol=s_it->second;
579 
580  // type the expression
581  symbol_expr.type()=symbol.type;
582  }
583  }
584  else
585  {
586  // if this is a variable, we need to check if we already
587  // prefixed it and add to the symbol table if it is not there already
588  irep_idt identifier_base = identifier;
589  if(!has_prefix(id2string(identifier), id2string(proc_name)))
590  {
591  identifier = add_prefix(identifier);
592  symbol_expr.set_identifier(identifier);
593  }
594 
595  symbol_tablet::symbolst::const_iterator s_it=
596  symbol_table.symbols.find(identifier);
597 
598  if(s_it==symbol_table.symbols.end())
599  {
600  // create new symbol
601  symbolt new_symbol;
602  new_symbol.name=identifier;
603  new_symbol.type=symbol_expr.type();
604  new_symbol.base_name=identifier_base;
605  new_symbol.mode="jsil";
606  new_symbol.is_type=false;
607  new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
608 
609  // mark as already typechecked
610  new_symbol.is_extern=true;
611 
612  if(symbol_table.add(new_symbol))
613  {
614  error() << "failed to add symbol '" << new_symbol.name
615  << "' in the symbol table" << eom;
616  throw 0;
617  }
618  }
619  else
620  {
621  // symbol already exists
622  assert(!s_it->second.is_type);
623 
624  const symbolt &symbol=s_it->second;
625 
626  // type the expression
627  symbol_expr.type()=symbol.type;
628  }
629  }
630 }
631 
633 {
634  const irep_idt &statement=code.get_statement();
635 
636  if(statement==ID_function_call)
638  else if(statement==ID_return)
640  else if(statement==ID_expression)
641  {
642  if(code.operands().size()!=1)
643  {
645  error() << "expression statement expected to have one operand"
646  << eom;
647  throw 0;
648  }
649 
650  typecheck_expr(code.op0());
651  }
652  else if(statement==ID_label)
653  {
654  typecheck_code(to_code_label(code).code());
655  // TODO: produce defined label set
656  }
657  else if(statement==ID_block)
658  typecheck_block(code);
659  else if(statement==ID_ifthenelse)
661  else if(statement==ID_goto)
662  {
663  // TODO: produce used label set
664  }
665  else if(statement==ID_assign)
667  else if(statement==ID_try_catch)
669  else if(statement==ID_skip)
670  {
671  }
672  else
673  {
675  error() << "unexpected statement: " << statement << eom;
676  throw 0;
677  }
678 }
679 
681 {
682  if(code.has_return_value())
684 }
685 
687 {
688  Forall_operands(it, code)
689  typecheck_code(to_code(*it));
690 }
691 
693 {
694  // A special case of try catch with one catch clause
695  if(code.operands().size()!=3)
696  {
698  error() << "try_catch expected to have three operands" << eom;
699  throw 0;
700  }
701 
702  // function call
704 
705  // catch decl is not used, but is required by goto-programs
706 
708 }
709 
711  code_function_callt &call)
712 {
713  if(call.operands().size()!=3)
714  {
716  error() << "function call expected to have three operands" << eom;
717  throw 0;
718  }
719 
720  exprt &lhs=call.lhs();
721  typecheck_expr(lhs);
722 
723  exprt &f=call.function();
724  typecheck_expr(f);
725 
726  for(auto &arg : call.arguments())
727  typecheck_expr(arg);
728 
729  // Look for a function declaration symbol in the symbol table
730  if(f.id()==ID_symbol)
731  {
732  const irep_idt &id=to_symbol_expr(f).get_identifier();
733 
734  if(const auto maybe_symbol=symbol_table.lookup(id))
735  {
736  const symbolt &s=*maybe_symbol;
737 
738  if(s.type.id()==ID_code)
739  {
740  const code_typet &codet=to_code_type(s.type);
741 
742  for(std::size_t i=0; i<codet.parameters().size(); i++)
743  {
744  if(i>=call.arguments().size())
745  break;
746 
747  const typet &param_type=codet.parameters()[i].type();
748 
749  if(!param_type.id().empty() && param_type.is_not_nil())
750  {
751  // check argument's type if parameter's type is given
752  make_type_compatible(call.arguments()[i], param_type, true);
753  }
754  }
755 
756  // if there are too few arguments, add undefined
757  if(codet.parameters().size()>call.arguments().size())
758  {
759  for(std::size_t i=call.arguments().size();
760  i<codet.parameters().size();
761  ++i)
762  call.arguments().push_back(
763  exprt("undefined", jsil_undefined_type()));
764  }
765 
766  // if there are too many arguments, remove
767  while(codet.parameters().size()<call.arguments().size())
768  call.arguments().pop_back();
769 
770  // check return type if exists
771  if(!codet.return_type().id().empty() &&
772  codet.return_type().is_not_nil())
773  make_type_compatible(lhs, codet.return_type(), true);
774  else make_type_compatible(lhs, jsil_any_type(), true);
775  }
776  else
777  {
778  // TODO: a symbol can be a variable evaluating to a string
779  // which corresponds to a function identifier
780  make_type_compatible(lhs, jsil_any_type(), true);
781  }
782  }
783  else
784  {
785  // Should be function, declaration not found yet
786  symbolt new_symbol;
787  new_symbol.name=id;
788  new_symbol.type = code_typet({}, typet());
789  new_symbol.mode="jsil";
790  new_symbol.is_type=false;
791  new_symbol.value=exprt("no-body-just-yet");
792 
793  make_type_compatible(lhs, jsil_any_type(), true);
794 
795  if(symbol_table.add(new_symbol))
796  {
797  error().source_location=new_symbol.location;
798  error() << "failed to add expression symbol to symbol table"
799  << eom;
800  throw 0;
801  }
802  }
803  }
804  else
805  {
806  // TODO: this might be a string literal
807  // which corresponds to a function identifier
808  make_type_compatible(lhs, jsil_any_type(), true);
809  }
810 }
811 
813 {
814  exprt &cond=code.cond();
815  typecheck_expr(cond);
816  make_type_compatible(cond, bool_typet(), true);
817 
818  typecheck_code(code.then_case());
819 
820  if(!code.else_case().is_nil())
821  typecheck_code(code.else_case());
822 }
823 
825 {
826  typecheck_expr(code.lhs());
827  typecheck_expr(code.rhs());
828 
829  make_type_compatible(code.lhs(), code.rhs().type(), false);
830 }
831 
836 {
837  assert(!symbol.is_type);
838 
839  // Using is_extern to check if symbol was already typechecked
840  if(symbol.is_extern)
841  return;
842  if(symbol.value.id()!="no-body-just-yet")
843  symbol.is_extern=true;
844 
845  proc_name=symbol.name;
846  typecheck_type(symbol.type);
847 
848  if(symbol.value.id()==ID_code)
849  typecheck_code(to_code(symbol.value));
850  else if(symbol.name=="eval")
851  {
852  // No code for eval. Do nothing
853  }
854  else if(symbol.value.id()=="no-body-just-yet")
855  {
856  // Do nothing
857  }
858  else
859  {
860  error().source_location=symbol.location;
861  error() << "non-type symbol value expected code, but got "
862  << symbol.value.pretty() << eom;
863  throw 0;
864  }
865 }
866 
868 {
869  // The hash table iterators are not stable,
870  // and we might add new symbols.
871 
872  std::vector<irep_idt> identifiers;
873  identifiers.reserve(symbol_table.symbols.size());
874  for(const auto &symbol_pair : symbol_table.symbols)
875  {
876  identifiers.push_back(symbol_pair.first);
877  }
878 
879  // We first check all type symbols,
880  // recursively doing base classes first.
881  for(const irep_idt &id : identifiers)
882  {
883  symbolt &symbol = symbol_table.get_writeable_ref(id);
884  if(symbol.is_type)
885  typecheck_type_symbol(symbol);
886  }
887 
888  // We now check all non-type symbols
889  for(const irep_idt &id : identifiers)
890  {
891  symbolt &symbol = symbol_table.get_writeable_ref(id);
892  if(!symbol.is_type)
894  }
895 }
896 
898  symbol_tablet &symbol_table,
899  message_handlert &message_handler)
900 {
901  jsil_typecheckt jsil_typecheck(symbol_table, message_handler);
902  return jsil_typecheck.typecheck_main();
903 }
904 
906  exprt &expr,
907  message_handlert &message_handler,
908  const namespacet &)
909 {
910  const unsigned errors_before=
911  message_handler.get_message_count(messaget::M_ERROR);
912 
913  symbol_tablet symbol_table;
914 
916  symbol_table,
917  message_handler);
918 
919  try
920  {
921  jsil_typecheck.typecheck_expr(expr);
922  }
923 
924  catch(int)
925  {
926  jsil_typecheck.error();
927  }
928 
929  catch(const char *e)
930  {
931  jsil_typecheck.error() << e << messaget::eom;
932  }
933 
934  catch(const std::string &e)
935  {
936  jsil_typecheck.error() << e << messaget::eom;
937  }
938 
939  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
940 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
jsil_typecheckt::typecheck_expr_operands
void typecheck_expr_operands(exprt &expr)
Definition: jsil_typecheck.cpp:146
jsil_typecheckt::update_expr_type
void update_expr_type(exprt &expr, const typet &type)
Definition: jsil_typecheck.cpp:37
jsil_typecheckt::typecheck_expr_has_field
void typecheck_expr_has_field(exprt &expr)
Definition: jsil_typecheck.cpp:354
expr2jsil.h
Jsil Language.
symbol_table_baset::get_writeable
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
jsil_typecheckt::typecheck_expr_binary_compare
void typecheck_expr_binary_compare(exprt &expr)
Definition: jsil_typecheck.cpp:500
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
codet::op0
exprt & op0()
Definition: expr.h:102
jsil_typecheckt::typecheck_expr_unary_string
void typecheck_expr_unary_string(exprt &expr)
Definition: jsil_typecheck.cpp:529
jsil_typecheckt::typecheck_expr_ref
void typecheck_expr_ref(exprt &expr)
Definition: jsil_typecheck.cpp:397
jsil_typecheckt::typecheck_function_call
void typecheck_function_call(code_function_callt &function_call)
Definition: jsil_typecheck.cpp:710
jsil_typecheckt::to_string
virtual std::string to_string(const exprt &expr)
Definition: jsil_typecheck.cpp:21
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:774
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
jsil_typecheckt::typecheck_assign
void typecheck_assign(code_assignt &code)
Definition: jsil_typecheck.cpp:824
jsil_typecheckt::typecheck_expr_base
void typecheck_expr_base(exprt &expr)
Definition: jsil_typecheck.cpp:383
code_try_catcht
codet representation of a try/catch block.
Definition: std_code.h:2429
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
jsil_typecheck
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: jsil_typecheck.cpp:897
code_try_catcht::get_catch_code
codet & get_catch_code(unsigned i)
Definition: std_code.h:2459
jsil_typecheckt::typecheck_try_catch
void typecheck_try_catch(code_try_catcht &code)
Definition: jsil_typecheck.cpp:692
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
prefix.h
jsil_typecheckt
Definition: jsil_typecheck.h:35
jsil_typecheckt::typecheck_type
void typecheck_type(typet &type)
Definition: jsil_typecheck.cpp:99
jsil_typecheckt::typecheck_expr_index
void typecheck_expr_index(exprt &expr)
Definition: jsil_typecheck.cpp:333
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
to_side_effect_expr_throw
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:2221
jsil_typecheckt::typecheck_code
void typecheck_code(codet &code)
Definition: jsil_typecheck.cpp:632
bool_typet
The Boolean type.
Definition: std_types.h:37
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:764
messaget::eom
static eomt eom
Definition: message.h:297
jsil_types.h
Jsil Language.
jsil_null_type
typet jsil_null_type()
Definition: jsil_types.cpp:78
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:823
jsil_typecheckt::typecheck_return
void typecheck_return(code_returnt &code)
Definition: jsil_typecheck.cpp:680
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
jsil_incompatible_types
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:113
jsil_typecheckt::typecheck_expr_side_effect_throw
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
Definition: jsil_typecheck.cpp:269
jsil_typecheckt::typecheck_expr_unary_num
void typecheck_expr_unary_num(exprt &expr)
Definition: jsil_typecheck.cpp:543
jsil_value_or_reference_type
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:27
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
jsil_reference_type
typet jsil_reference_type()
Definition: jsil_types.cpp:46
jsil_typecheckt::typecheck_non_type_symbol
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
Definition: jsil_typecheck.cpp:835
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
jsil_typecheckt::typecheck_expr_main
void typecheck_expr_main(exprt &expr)
Definition: jsil_typecheck.cpp:152
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
type2jsil
std::string type2jsil(const typet &type, const namespacet &ns)
Definition: expr2jsil.cpp:31
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
jsil_union
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:119
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:816
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1420
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
messaget::M_ERROR
@ M_ERROR
Definition: message.h:170
jsil_variable_reference_type
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:57
jsil_typecheckt::typecheck_expr_unary_boolean
void typecheck_expr_unary_boolean(exprt &expr)
Definition: jsil_typecheck.cpp:515
jsil_typecheckt::typecheck_expr_proto_field
void typecheck_expr_proto_field(exprt &expr)
Definition: jsil_typecheck.cpp:288
jsil_any_type
typet jsil_any_type()
Definition: jsil_types.cpp:16
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
jsil_undefined_type
typet jsil_undefined_type()
Definition: jsil_types.cpp:83
jsil_typecheckt::typecheck_ifthenelse
void typecheck_ifthenelse(code_ifthenelset &code)
Definition: jsil_typecheck.cpp:812
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
dstringt::empty
bool empty() const
Definition: dstring.h:88
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
jsil_kind
typet jsil_kind()
Definition: jsil_types.cpp:88
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
jsil_typecheckt::typecheck_expr_proto_obj
void typecheck_expr_proto_obj(exprt &expr)
Definition: jsil_typecheck.cpp:303
jsil_typecheckt::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: jsil_typecheck.cpp:137
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
jsil_typecheckt::typecheck_expr_binary_boolean
void typecheck_expr_binary_boolean(exprt &expr)
Definition: jsil_typecheck.cpp:456
to_code_try_catch
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2493
jsil_typecheckt::typecheck_symbol_expr
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
Definition: jsil_typecheck.cpp:555
jsil_typecheckt::symbol_table
symbol_table_baset & symbol_table
Definition: jsil_typecheck.h:53
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
jsil_typecheckt::typecheck_expr_constant
void typecheck_expr_constant(exprt &expr)
Definition: jsil_typecheck.cpp:278
jsil_object_type
typet jsil_object_type()
Definition: jsil_types.cpp:62
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1330
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
jsil_member_reference_type
typet jsil_member_reference_type()
Definition: jsil_types.cpp:52
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
jsil_typecheckt::ns
const namespacet ns
Definition: jsil_typecheck.h:54
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
is_jsil_builtin_code_type
bool is_jsil_builtin_code_type(const typet &type)
Definition: jsil_types.h:55
jsil_typecheckt::typecheck_type_symbol
void typecheck_type_symbol(symbolt &)
Definition: jsil_typecheck.h:60
jsil_typecheckt::typecheck_expr_concatenation
void typecheck_expr_concatenation(exprt &expr)
Definition: jsil_typecheck.cpp:426
symbolt
Symbol table entry.
Definition: symbol.h:28
jsil_empty_type
typet jsil_empty_type()
Definition: jsil_types.cpp:93
expr2jsil
std::string expr2jsil(const exprt &expr, const namespacet &ns)
Definition: expr2jsil.cpp:24
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
string_typet
String type.
Definition: std_types.h:1655
jsil_typecheckt::typecheck_block
void typecheck_block(codet &code)
Definition: jsil_typecheck.cpp:686
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:784
jsil_typecheck.h
Jsil Language.
code_typet::parametert
Definition: std_types.h:753
jsil_is_subtype
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:98
jsil_typecheckt::proc_name
irep_idt proc_name
Definition: jsil_typecheck.h:56
code_try_catcht::try_code
codet & try_code()
Definition: std_code.h:2437
is_jsil_spec_code_type
bool is_jsil_spec_code_type(const typet &type)
Definition: jsil_types.h:78
jsil_typecheckt::typecheck_expr_binary_arith
void typecheck_expr_binary_arith(exprt &expr)
Definition: jsil_typecheck.cpp:471
jsil_user_object_type
typet jsil_user_object_type()
Definition: jsil_types.cpp:68
jsil_value_or_empty_type
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:22
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2200
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
jsil_value_type
typet jsil_value_type()
Definition: jsil_types.cpp:32
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
jsil_typecheckt::typecheck_expr_subtype
void typecheck_expr_subtype(exprt &expr)
Definition: jsil_typecheck.cpp:441
exprt::operands
operandst & operands()
Definition: expr.h:95
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
jsil_typecheckt::typecheck
virtual void typecheck()
Definition: jsil_typecheck.cpp:867
jsil_typecheckt::typecheck_expr_field
void typecheck_expr_field(exprt &expr)
Definition: jsil_typecheck.cpp:369
symbol_table.h
Author: Diffblue Ltd.
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
jsil_typecheckt::add_prefix
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
Definition: jsil_typecheck.cpp:32
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
jsil_typecheckt::typecheck_exp_binary_equal
void typecheck_exp_binary_equal(exprt &expr)
Definition: jsil_typecheck.cpp:486
jsil_typecheckt::make_type_compatible
void make_type_compatible(exprt &expr, const typet &type, bool must)
Definition: jsil_typecheck.cpp:60
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
jsil_typecheckt::typecheck_expr_delete
void typecheck_expr_delete(exprt &expr)
Definition: jsil_typecheck.cpp:318
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35