cprover
Loading...
Searching...
No Matches
jsil_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Daiva Naudziuniene, daivan@amazon.com
6
7\*******************************************************************/
8
11
12#include "jsil_types.h"
13
15
16#include <algorithm>
17
23
28
33
42
47
53
55{
56 return typet("jsil_member_reference_type");
57}
58
60{
61 return typet("jsil_variable_reference_type");
62}
63
69
71{
72 return typet("jsil_user_object_type");
73}
74
76{
77 return typet("jsil_builtin_object_type");
78}
79
81{
82 return typet("jsil_null_type");
83}
84
86{
87 return typet("jsil_undefined_type");
88}
89
91{
92 return typet("jsil_kind");
93}
94
96{
97 return typet("jsil_empty_type");
98}
99
101{
102 if(type2.id()==ID_union)
103 {
105
106 if(type1.id()==ID_union)
108 else
110 }
111 else
112 return type1.id()==type2.id();
113}
114
120
126
130{
131 return comp1.type().id()<comp2.type().id();
132}
133
134jsil_union_typet::jsil_union_typet(const std::vector<typet> &types):
136{
137 auto &elements=components();
138 for(const auto &type : types)
139 {
140 if(type.id()==ID_union)
141 {
142 for(const auto &component : to_union_type(type).components())
143 elements.push_back(component);
144 }
145 else
146 elements.push_back(componentt(ID_anonymous, type));
147 }
148
149 std::sort(elements.begin(), elements.end(), compare_components);
150}
151
153 const jsil_union_typet &other) const
154{
155 auto &elements1=components();
156 auto &elements2=other.components();
157 jsil_union_typet result;
158 auto &elements=result.components();
159 elements.resize(elements1.size()+elements2.size());
160 std::vector<union_typet::componentt>::iterator it=std::set_union(
161 elements1.begin(), elements1.end(),
162 elements2.begin(), elements2.end(),
163 elements.begin(), compare_components);
164 elements.resize(it-elements.begin());
165
166 return result;
167}
168
170 const jsil_union_typet &other) const
171{
172 auto &elements1=components();
173 auto &elements2=other.components();
174 jsil_union_typet result;
175 auto &elements=result.components();
176 elements.resize(std::min(elements1.size(), elements2.size()));
177 std::vector<union_typet::componentt>::iterator it=std::set_intersection(
178 elements1.begin(), elements1.end(),
179 elements2.begin(), elements2.end(),
180 elements.begin(), compare_components);
181 elements.resize(it-elements.begin());
182
183 return result;
184}
185
187{
188 auto it=components().begin();
189 auto it2=other.components().begin();
190 while(it<components().end())
191 {
192 if(it2>=other.components().end())
193 {
194 // We haven't found all types, but the second array finishes
195 return false;
196 }
197
198 if(it->type().id()==it2->type().id())
199 {
200 // Found the type
201 it++;
202 it2++;
203 }
204 else if(it->type().id()<it2->type().id())
205 {
206 // Missing type
207 return false;
208 }
209 else // it->type().id()>it2->type().id()
210 {
211 // Skip one element in the second array
212 it2++;
213 }
214 }
215
216 return true;
217}
218
220{
221 auto &elements=components();
222 if(elements.size()==1)
223 return elements[0].type();
224
225 return *this;
226}
Pre-defined bitvector types.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
The Boolean type.
Definition std_types.h:36
Fixed-width bit-vector with IEEE floating-point interpretation.
jsil_union_typet union_with(const jsil_union_typet &other) const
jsil_union_typet intersect_with(const jsil_union_typet &other) const
bool is_subtype(const jsil_union_typet &other) const
const typet & to_type() const
String type.
Definition std_types.h:901
const componentst & components() const
Definition std_types.h:147
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:125
bool compare_components(const union_typet::componentt &comp1, const union_typet::componentt &comp2)
typet jsil_value_or_empty_type()
typet jsil_empty_type()
typet jsil_undefined_type()
typet jsil_null_type()
typet jsil_variable_reference_type()
bool jsil_is_subtype(const typet &type1, const typet &type2)
typet jsil_kind()
typet jsil_builtin_object_type()
typet jsil_user_object_type()
typet jsil_union(const typet &type1, const typet &type2)
bool jsil_incompatible_types(const typet &type1, const typet &type2)
typet jsil_prim_type()
typet jsil_any_type()
typet jsil_reference_type()
typet jsil_member_reference_type()
typet jsil_value_or_reference_type()
typet jsil_value_type()
typet jsil_object_type()
Jsil Language.
jsil_union_typet & to_jsil_union_type(typet &type)
Definition jsil_types.h:102
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48