1/* Symbolic offsets and ranges.
2 Copyright (C) 2023-2025 Free Software Foundation, Inc.
3 Contributed by David Malcolm <dmalcolm@redhat.com>.
4
5This file is part of GCC.
6
7GCC is free software; you can redistribute it and/or modify it
8under the terms of the GNU General Public License as published by
9the Free Software Foundation; either version 3, or (at your option)
10any later version.
11
12GCC is distributed in the hope that it will be useful, but
13WITHOUT ANY WARRANTY; without even the implied warranty of
14MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15General Public License for more details.
16
17You should have received a copy of the GNU General Public License
18along with GCC; see the file COPYING3. If not see
19<http://www.gnu.org/licenses/>. */
20
21#include "analyzer/common.h"
22
23#include "sbitmap.h"
24#include "ordered-hash-map.h"
25
26#include "analyzer/analyzer-logging.h"
27#include "analyzer/supergraph.h"
28#include "analyzer/call-string.h"
29#include "analyzer/program-point.h"
30#include "analyzer/store.h"
31#include "analyzer/region-model.h"
32#include "analyzer/constraint-manager.h"
33#include "analyzer/analyzer-selftests.h"
34#include "analyzer/ranges.h"
35
36#if ENABLE_ANALYZER
37
38namespace ana {
39
40/* class symbolic_byte_offset. */
41
42symbolic_byte_offset::symbolic_byte_offset (int i, region_model_manager &mgr)
43: m_num_bytes_sval (mgr.get_or_create_int_cst (size_type_node, cst: i))
44{
45}
46
47symbolic_byte_offset::symbolic_byte_offset (const svalue *num_bytes_sval)
48: m_num_bytes_sval (num_bytes_sval)
49{
50}
51
52symbolic_byte_offset::symbolic_byte_offset (region_offset offset,
53 region_model_manager &mgr)
54{
55 if (offset.concrete_p ())
56 {
57 bit_offset_t num_bits = offset.get_bit_offset ();
58 gcc_assert (num_bits % BITS_PER_UNIT == 0);
59 byte_offset_t num_bytes = num_bits / BITS_PER_UNIT;
60 m_num_bytes_sval = mgr.get_or_create_int_cst (size_type_node, cst: num_bytes);
61 }
62 else
63 m_num_bytes_sval = offset.get_symbolic_byte_offset ();
64}
65
66void
67symbolic_byte_offset::dump_to_pp (pretty_printer *pp, bool simple) const
68{
69 pp_string (pp, "byte ");
70 m_num_bytes_sval->dump_to_pp (pp, simple);
71}
72
73void
74symbolic_byte_offset::dump (bool simple) const
75{
76 tree_dump_pretty_printer pp (stderr);
77 dump_to_pp (pp: &pp, simple);
78 pp_newline (&pp);
79}
80
81std::unique_ptr<json::value>
82symbolic_byte_offset::to_json () const
83{
84 return m_num_bytes_sval->to_json ();
85}
86
87tree
88symbolic_byte_offset::maybe_get_constant () const
89{
90 return m_num_bytes_sval->maybe_get_constant ();
91}
92
93/* class symbolic_byte_range. */
94
95symbolic_byte_range::symbolic_byte_range (region_offset start,
96 const svalue *num_bytes,
97 region_model_manager &mgr)
98: m_start (start, mgr),
99 m_size (num_bytes)
100{
101}
102
103void
104symbolic_byte_range::dump_to_pp (pretty_printer *pp,
105 bool simple,
106 region_model_manager &mgr) const
107{
108 if (empty_p ())
109 {
110 pp_string (pp, "empty");
111 return;
112 }
113
114 if (tree size_cst = m_size.maybe_get_constant ())
115 if (integer_onep (size_cst))
116 {
117 pp_string (pp, "byte ");
118 m_start.get_svalue ()->dump_to_pp (pp, simple);
119 return;
120 }
121
122 pp_string (pp, "bytes ");
123 m_start.get_svalue ()->dump_to_pp (pp, simple);
124 pp_string (pp, " to ");
125 get_last_byte_offset (mgr).get_svalue ()->dump_to_pp (pp, simple);
126}
127
128void
129symbolic_byte_range::dump (bool simple, region_model_manager &mgr) const
130{
131 tree_dump_pretty_printer pp (stderr);
132 dump_to_pp (pp: &pp, simple, mgr);
133 pp_newline (&pp);
134}
135
136std::unique_ptr<json::value>
137symbolic_byte_range::to_json () const
138{
139 auto obj = std::make_unique<json::object> ();
140 obj->set (key: "start", v: m_start.to_json ());
141 obj->set (key: "size", v: m_size.to_json ());
142 return obj;
143}
144
145bool
146symbolic_byte_range::empty_p () const
147{
148 tree cst = m_size.maybe_get_constant ();
149 if (!cst)
150 return false;
151 return zerop (cst);
152}
153
154symbolic_byte_offset
155symbolic_byte_range::get_last_byte_offset (region_model_manager &mgr) const
156{
157 gcc_assert (!empty_p ());
158 const symbolic_byte_offset one (1, mgr);
159 return symbolic_byte_offset
160 (mgr.get_or_create_binop (size_type_node,
161 op: MINUS_EXPR,
162 arg0: get_next_byte_offset (mgr).get_svalue (),
163 arg1: one.get_svalue ()));
164}
165
166symbolic_byte_offset
167symbolic_byte_range::get_next_byte_offset (region_model_manager &mgr) const
168{
169 return symbolic_byte_offset (mgr.get_or_create_binop (size_type_node,
170 op: PLUS_EXPR,
171 arg0: m_start.get_svalue (),
172 arg1: m_size.get_svalue ()));
173}
174
175/* Attempt to determine if THIS range intersects OTHER,
176 using constraints from MODEL. */
177
178tristate
179symbolic_byte_range::intersection (const symbolic_byte_range &other,
180 const region_model &model) const
181{
182 /* If either is empty, then there is no intersection. */
183 if (empty_p ())
184 return tristate::TS_FALSE;
185 if (other.empty_p ())
186 return tristate::TS_FALSE;
187
188 /* For brevity, consider THIS to be "range A", and OTHER to be "range B". */
189
190 region_model_manager *mgr = model.get_manager ();
191
192 const svalue *first_sval_a = m_start.get_svalue ();
193 const svalue *first_sval_b = other.m_start.get_svalue ();
194 const svalue *last_sval_a = get_last_byte_offset (mgr&: *mgr).get_svalue ();
195 const svalue *last_sval_b = other.get_last_byte_offset (mgr&: *mgr).get_svalue ();
196
197 if (m_size.get_svalue ()->get_kind () == SK_UNKNOWN
198 || other.m_size.get_svalue ()->get_kind () == SK_UNKNOWN)
199 {
200 if (first_sval_a == first_sval_b)
201 return tristate::TS_TRUE;
202 else
203 return tristate::TS_UNKNOWN;
204 }
205
206 if (first_sval_a == first_sval_b)
207 return tristate::TS_TRUE;
208
209 /* Is B fully before A? */
210 tristate b_fully_before_a = model.eval_condition (lhs: last_sval_b,
211 op: LT_EXPR,
212 rhs: first_sval_a);
213 /* Is B fully after A? */
214 tristate b_fully_after_a = model.eval_condition (lhs: first_sval_b,
215 op: GT_EXPR,
216 rhs: last_sval_a);
217
218 if (b_fully_before_a.is_true ()
219 || b_fully_after_a.is_true ())
220 return tristate::TS_FALSE;
221
222 if (b_fully_before_a.is_unknown ()
223 || b_fully_after_a.is_unknown ())
224 return tristate::TS_UNKNOWN;
225
226 return tristate::TS_TRUE;
227}
228
229#if CHECKING_P
230
231namespace selftest {
232
233static void test_intersects (void)
234{
235 region_model_manager mgr;
236 region_model m (&mgr);
237
238 /* Test various concrete ranges. */
239 symbolic_byte_offset zero (0, mgr);
240 symbolic_byte_offset one (1, mgr);
241 symbolic_byte_offset five (5, mgr);
242 symbolic_byte_offset nine (9, mgr);
243 symbolic_byte_offset ten (10, mgr);
244
245 symbolic_byte_range r0_9 (zero, ten);
246 symbolic_byte_range r0 (zero, one);
247 symbolic_byte_range r5_9 (five, five);
248 symbolic_byte_range r9 (nine, one);
249 symbolic_byte_range r10 (ten, one);
250 symbolic_byte_range r10_19 (ten, ten);
251
252 ASSERT_EQ (r0_9.get_start_byte_offset (), zero);
253 ASSERT_EQ (r0_9.get_size_in_bytes (), ten);
254 ASSERT_EQ (r0_9.get_next_byte_offset (mgr), ten);
255 ASSERT_EQ (r0_9.get_last_byte_offset (mgr), nine);
256
257 symbolic_byte_range concrete_empty (zero, zero);
258 ASSERT_TRUE (concrete_empty.empty_p ());
259
260 ASSERT_EQ (r0_9.intersection (r0, m), tristate::TS_TRUE);
261 ASSERT_EQ (r0.intersection (r0_9, m), tristate::TS_TRUE);
262 ASSERT_EQ (r0_9.intersection (r9, m), tristate::TS_TRUE);
263 ASSERT_EQ (r9.intersection (r0_9, m), tristate::TS_TRUE);
264 ASSERT_EQ (r0_9.intersection (r10, m), tristate::TS_FALSE);
265 ASSERT_EQ (r10.intersection (r0_9, m), tristate::TS_FALSE);
266 ASSERT_EQ (concrete_empty.intersection (r0_9, m), tristate::TS_FALSE);
267 ASSERT_EQ (r0_9.intersection (concrete_empty, m), tristate::TS_FALSE);
268
269 ASSERT_EQ (r5_9.intersection (r0, m), tristate::TS_FALSE);
270 ASSERT_EQ (r0.intersection (r5_9, m), tristate::TS_FALSE);
271 ASSERT_EQ (r9.intersection (r5_9, m), tristate::TS_TRUE);
272 ASSERT_EQ (r10.intersection (r5_9, m), tristate::TS_FALSE);
273
274 /* Test various symbolic ranges. */
275 tree x = build_global_decl (name: "x", size_type_node);
276 const svalue *x_init_sval = m.get_rvalue (expr: x, ctxt: nullptr);
277 tree y = build_global_decl (name: "y", size_type_node);
278 const svalue *y_init_sval = m.get_rvalue (expr: y, ctxt: nullptr);
279
280 symbolic_byte_range r0_x_minus_1 (zero, x_init_sval);
281 symbolic_byte_range rx (x_init_sval, one);
282 symbolic_byte_range r0_y_minus_1 (zero, y_init_sval);
283 symbolic_byte_range ry (y_init_sval, one);
284 symbolic_byte_range rx_x_plus_y_minus_1 (x_init_sval, y_init_sval);
285
286 symbolic_byte_range symbolic_empty (x_init_sval, zero);
287 ASSERT_TRUE (symbolic_empty.empty_p ());
288
289 ASSERT_EQ (rx_x_plus_y_minus_1.get_start_byte_offset (), x_init_sval);
290 ASSERT_EQ (rx_x_plus_y_minus_1.get_size_in_bytes (), y_init_sval);
291 ASSERT_EQ
292 (rx_x_plus_y_minus_1.get_next_byte_offset (mgr).get_svalue ()->get_kind (),
293 SK_BINOP);
294 ASSERT_EQ
295 (rx_x_plus_y_minus_1.get_last_byte_offset (mgr).get_svalue ()->get_kind (),
296 SK_BINOP);
297
298 ASSERT_EQ (rx.intersection (ry, m), tristate::TS_UNKNOWN);
299 ASSERT_EQ (rx.intersection (concrete_empty, m), tristate::TS_FALSE);
300 ASSERT_EQ (concrete_empty.intersection (rx, m), tristate::TS_FALSE);
301 ASSERT_EQ (rx.intersection (symbolic_empty, m), tristate::TS_FALSE);
302 ASSERT_EQ (symbolic_empty.intersection (rx, m), tristate::TS_FALSE);
303 ASSERT_EQ (r0_x_minus_1.intersection (r0, m), tristate::TS_TRUE);
304#if 0
305 ASSERT_EQ (r0_x_minus_1.intersection (rx, m), tristate::TS_FALSE);
306 /* Fails (with UNKNOWN): b_fully_after_a is UNKNOWN, when it could
307 be TRUE: last of A is (x - 1), but it's not necessarily true that
308 X > (x - 1), for the case where x is (unsigned)0. */
309#endif
310 ASSERT_EQ (r0_x_minus_1.intersection (r0_y_minus_1, m), tristate::TS_TRUE);
311 // TODO: etc
312}
313
314/* Run all of the selftests within this file. */
315
316void
317analyzer_ranges_cc_tests ()
318{
319 test_intersects ();
320}
321
322} // namespace selftest
323
324#endif /* CHECKING_P */
325
326} // namespace ana
327
328#endif /* #if ENABLE_ANALYZER */
329

source code of gcc/analyzer/ranges.cc