cprover
jsil_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: Daiva Naudziuniene, daivan@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jsil_types.h"
13 
14 #include <algorithm>
15 
17 {
18  return jsil_union_typet(
20 }
21 
23 {
25 }
26 
28 {
30 }
31 
33 {
34  return jsil_union_typet(
38  jsil_object_type()});
39 }
40 
42 {
44 }
45 
47 {
48  return jsil_union_typet(
50 }
51 
53 {
54  return typet("jsil_member_reference_type");
55 }
56 
58 {
59  return typet("jsil_variable_reference_type");
60 }
61 
63 {
64  return jsil_union_typet(
66 }
67 
69 {
70  return typet("jsil_user_object_type");
71 }
72 
74 {
75  return typet("jsil_builtin_object_type");
76 }
77 
79 {
80  return typet("jsil_null_type");
81 }
82 
84 {
85  return typet("jsil_undefined_type");
86 }
87 
89 {
90  return typet("jsil_kind");
91 }
92 
94 {
95  return typet("jsil_empty_type");
96 }
97 
98 bool jsil_is_subtype(const typet &type1, const typet &type2)
99 {
100  if(type2.id()==ID_union)
101  {
102  const jsil_union_typet &type2_union=to_jsil_union_type(type2);
103 
104  if(type1.id()==ID_union)
105  return to_jsil_union_type(type1).is_subtype(type2_union);
106  else
107  return jsil_union_typet(type1).is_subtype(type2_union);
108  }
109  else
110  return type1.id()==type2.id();
111 }
112 
113 bool jsil_incompatible_types(const typet &type1, const typet &type2)
114 {
115  return jsil_union_typet(type1).intersect_with(
116  jsil_union_typet(type2)).components().empty();
117 }
118 
119 typet jsil_union(const typet &type1, const typet &type2)
120 {
121  return jsil_union_typet(type1)
123 }
124 
126  const union_typet::componentt &comp1,
127  const union_typet::componentt &comp2)
128 {
129  return comp1.type().id()<comp2.type().id();
130 }
131 
132 jsil_union_typet::jsil_union_typet(const std::vector<typet> &types):
133  union_typet()
134 {
135  auto &elements=components();
136  for(const auto &type : types)
137  {
138  if(type.id()==ID_union)
139  {
140  for(const auto &component : to_union_type(type).components())
141  elements.push_back(component);
142  }
143  else
144  elements.push_back(componentt(ID_anonymous, type));
145  }
146 
147  std::sort(elements.begin(), elements.end(), compare_components);
148 }
149 
151  const jsil_union_typet &other) const
152 {
153  auto &elements1=components();
154  auto &elements2=other.components();
155  jsil_union_typet result;
156  auto &elements=result.components();
157  elements.resize(elements1.size()+elements2.size());
158  std::vector<union_typet::componentt>::iterator it=std::set_union(
159  elements1.begin(), elements1.end(),
160  elements2.begin(), elements2.end(),
161  elements.begin(), compare_components);
162  elements.resize(it-elements.begin());
163 
164  return result;
165 }
166 
168  const jsil_union_typet &other) const
169 {
170  auto &elements1=components();
171  auto &elements2=other.components();
172  jsil_union_typet result;
173  auto &elements=result.components();
174  elements.resize(std::min(elements1.size(), elements2.size()));
175  std::vector<union_typet::componentt>::iterator it=std::set_intersection(
176  elements1.begin(), elements1.end(),
177  elements2.begin(), elements2.end(),
178  elements.begin(), compare_components);
179  elements.resize(it-elements.begin());
180 
181  return result;
182 }
183 
185 {
186  auto it=components().begin();
187  auto it2=other.components().begin();
188  while(it<components().end())
189  {
190  if(it2>=other.components().end())
191  {
192  // We haven't found all types, but the second array finishes
193  return false;
194  }
195 
196  if(it->type().id()==it2->type().id())
197  {
198  // Found the type
199  it++;
200  it2++;
201  }
202  else if(it->type().id()<it2->type().id())
203  {
204  // Missing type
205  return false;
206  }
207  else // it->type().id()>it2->type().id()
208  {
209  // Skip one element in the second array
210  it2++;
211  }
212  }
213 
214  return true;
215 }
216 
218 {
219  auto &elements=components();
220  if(elements.size()==1)
221  return elements[0].type();
222 
223  return *this;
224 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
typet
The type of an expression, extends irept.
Definition: type.h:29
jsil_union_typet::intersect_with
jsil_union_typet intersect_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:167
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
jsil_union_typet
Definition: jsil_types.h:85
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
bool_typet
The Boolean type.
Definition: std_types.h:37
jsil_types.h
Jsil Language.
jsil_union_typet::to_type
const typet & to_type() const
Definition: jsil_types.cpp:217
jsil_null_type
typet jsil_null_type()
Definition: jsil_types.cpp:78
jsil_builtin_object_type
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:73
jsil_incompatible_types
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:113
jsil_value_or_reference_type
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:27
compare_components
bool compare_components(const union_typet::componentt &comp1, const union_typet::componentt &comp2)
Definition: jsil_types.cpp:125
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
jsil_reference_type
typet jsil_reference_type()
Definition: jsil_types.cpp:46
jsil_union
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:119
jsil_variable_reference_type
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:57
jsil_any_type
typet jsil_any_type()
Definition: jsil_types.cpp:16
jsil_undefined_type
typet jsil_undefined_type()
Definition: jsil_types.cpp:83
irept::id
const irep_idt & id() const
Definition: irep.h:418
union_typet
The union type.
Definition: std_types.h:393
jsil_kind
typet jsil_kind()
Definition: jsil_types.cpp:88
jsil_union_typet::is_subtype
bool is_subtype(const jsil_union_typet &other) const
Definition: jsil_types.cpp:184
jsil_union_typet::jsil_union_typet
jsil_union_typet()
Definition: jsil_types.h:87
struct_union_typet::componentt
Definition: std_types.h:64
jsil_object_type
typet jsil_object_type()
Definition: jsil_types.cpp:62
jsil_member_reference_type
typet jsil_member_reference_type()
Definition: jsil_types.cpp:52
to_jsil_union_type
jsil_union_typet & to_jsil_union_type(typet &type)
Definition: jsil_types.h:103
jsil_empty_type
typet jsil_empty_type()
Definition: jsil_types.cpp:93
string_typet
String type.
Definition: std_types.h:1655
jsil_union_typet::union_with
jsil_union_typet union_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:150
jsil_is_subtype
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:98
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
jsil_value_type
typet jsil_value_type()
Definition: jsil_types.cpp:32
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
jsil_prim_type
typet jsil_prim_type()
Definition: jsil_types.cpp:41