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