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({ // NOLINT(whitespace/braces)
22  });
23 }
24 
26 {
27  return jsil_union_typet({ // NOLINT(whitespace/braces)
30  });
31 }
32 
34 {
35  return jsil_union_typet({ // NOLINT(whitespace/braces)
38  });
39 }
40 
42 {
43  return jsil_union_typet({ // NOLINT(whitespace/braces)
48  });
49 }
50 
52 {
53  return jsil_union_typet({ // NOLINT(whitespace/braces)
54  floatbv_typet(),
55  string_typet(),
56  bool_typet()
57  });
58 }
59 
61 {
62  return jsil_union_typet({ // NOLINT(whitespace/braces)
65  });
66 }
67 
69 {
70  return typet("jsil_member_reference_type");
71 }
72 
74 {
75  return typet("jsil_variable_reference_type");
76 }
77 
79 {
80  return jsil_union_typet({ // NOLINT(whitespace/braces)
83  });
84 }
85 
87 {
88  return typet("jsil_user_object_type");
89 }
90 
92 {
93  return typet("jsil_builtin_object_type");
94 }
95 
97 {
98  return typet("jsil_null_type");
99 }
100 
102 {
103  return typet("jsil_undefined_type");
104 }
105 
107 {
108  return typet("jsil_kind");
109 }
110 
112 {
113  return typet("jsil_empty_type");
114 }
115 
116 bool jsil_is_subtype(const typet &type1, const typet &type2)
117 {
118  if(type2.id()==ID_union)
119  {
120  const jsil_union_typet &type2_union=to_jsil_union_type(type2);
121 
122  if(type1.id()==ID_union)
123  return to_jsil_union_type(type1).is_subtype(type2_union);
124  else
125  return jsil_union_typet(type1).is_subtype(type2_union);
126  }
127  else
128  return type1.id()==type2.id();
129 }
130 
131 bool jsil_incompatible_types(const typet &type1, const typet &type2)
132 {
133  return jsil_union_typet(type1).intersect_with(
134  jsil_union_typet(type2)).components().empty();
135 }
136 
137 typet jsil_union(const typet &type1, const typet &type2)
138 {
139  return jsil_union_typet(type1)
141 }
142 
144  const union_typet::componentt &comp1,
145  const union_typet::componentt &comp2)
146 {
147  return comp1.type().id()<comp2.type().id();
148 }
149 
150 jsil_union_typet::jsil_union_typet(const std::vector<typet> &types):
151  union_typet()
152 {
153  auto &elements=components();
154  for(const auto &type : types)
155  {
156  if(type.id()==ID_union)
157  {
158  for(const auto &component : to_union_type(type).components())
159  elements.push_back(component);
160  }
161  else
162  elements.push_back(componentt(ID_anonymous, type));
163  }
164 
165  std::sort(elements.begin(), elements.end(), compare_components);
166 }
167 
169  const jsil_union_typet &other) const
170 {
171  auto &elements1=components();
172  auto &elements2=other.components();
173  jsil_union_typet result;
174  auto &elements=result.components();
175  elements.resize(elements1.size()+elements2.size());
176  std::vector<union_typet::componentt>::iterator it=std::set_union(
177  elements1.begin(), elements1.end(),
178  elements2.begin(), elements2.end(),
179  elements.begin(), compare_components);
180  elements.resize(it-elements.begin());
181 
182  return result;
183 }
184 
186  const jsil_union_typet &other) const
187 {
188  auto &elements1=components();
189  auto &elements2=other.components();
190  jsil_union_typet result;
191  auto &elements=result.components();
192  elements.resize(std::min(elements1.size(), elements2.size()));
193  std::vector<union_typet::componentt>::iterator it=std::set_intersection(
194  elements1.begin(), elements1.end(),
195  elements2.begin(), elements2.end(),
196  elements.begin(), compare_components);
197  elements.resize(it-elements.begin());
198 
199  return result;
200 }
201 
203 {
204  auto it=components().begin();
205  auto it2=other.components().begin();
206  while(it<components().end())
207  {
208  if(it2>=other.components().end())
209  {
210  // We haven't found all types, but the second array finishes
211  return false;
212  }
213 
214  if(it->type().id()==it2->type().id())
215  {
216  // Found the type
217  it++;
218  it2++;
219  }
220  else if(it->type().id()<it2->type().id())
221  {
222  // Missing type
223  return false;
224  }
225  else // it->type().id()>it2->type().id()
226  {
227  // Skip one element in the second array
228  it2++;
229  }
230  }
231 
232  return true;
233 }
234 
236 {
237  auto &elements=components();
238  if(elements.size()==1)
239  return elements[0].type();
240 
241  return *this;
242 }
The type of an expression.
Definition: type.h:20
typet jsil_prim_type()
Definition: jsil_types.cpp:51
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
Jsil Language.
const componentst & components() const
Definition: std_types.h:242
jsil_union_typet intersect_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:185
jsil_union_typet union_with(const jsil_union_typet &other) const
Definition: jsil_types.cpp:168
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
typet jsil_value_or_reference_type()
Definition: jsil_types.cpp:33
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
typet jsil_null_type()
Definition: jsil_types.cpp:96
typet jsil_builtin_object_type()
Definition: jsil_types.cpp:91
const irep_idt & id() const
Definition: irep.h:189
bool jsil_incompatible_types(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:131
bool compare_components(const union_typet::componentt &comp1, const union_typet::componentt &comp2)
Definition: jsil_types.cpp:143
typet jsil_union(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:137
typet jsil_reference_type()
Definition: jsil_types.cpp:60
typet jsil_undefined_type()
Definition: jsil_types.cpp:101
typet jsil_any_type()
Definition: jsil_types.cpp:16
typet jsil_kind()
Definition: jsil_types.cpp:106
const typet & to_type() const
Definition: jsil_types.cpp:235
typet jsil_variable_reference_type()
Definition: jsil_types.cpp:73
typet jsil_object_type()
Definition: jsil_types.cpp:78
bool jsil_is_subtype(const typet &type1, const typet &type2)
Definition: jsil_types.cpp:116
The union type.
Definition: std_types.h:424
typet jsil_member_reference_type()
Definition: jsil_types.cpp:68
typet jsil_value_or_empty_type()
Definition: jsil_types.cpp:25
typet jsil_value_type()
Definition: jsil_types.cpp:41
typet jsil_empty_type()
Definition: jsil_types.cpp:111
typet jsil_user_object_type()
Definition: jsil_types.cpp:86
bool is_subtype(const jsil_union_typet &other) const
Definition: jsil_types.cpp:202
jsil_union_typet & to_jsil_union_type(typet &type)
Definition: jsil_types.h:103