Coverage for trlc/vcg.py: 97%
787 statements
« prev ^ index » next coverage.py v7.10.7, created at 2026-09-04 11:46 +0000
1#!/usr/bin/env python3
2#
3# TRLC - Treat Requirements Like Code
4# Copyright (C) 2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG)
5# Copyright (C) 2023-2025 Florian Schanda
6#
7# This file is part of the TRLC Python Reference Implementation.
8#
9# TRLC is free software: you can redistribute it and/or modify it
10# under the terms of the GNU General Public License as published by
11# the Free Software Foundation, either version 3 of the License, or
12# (at your option) any later version.
13#
14# TRLC is distributed in the hope that it will be useful, but WITHOUT
15# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
16# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
17# License for more details.
18#
19# You should have received a copy of the GNU General Public License
20# along with TRLC. If not, see <https://www.gnu.org/licenses/>.
22import subprocess
24from trlc.ast import *
25from trlc.errors import Location, Message_Handler
27try:
28 from pyvcg import smt
29 from pyvcg import graph
30 from pyvcg import vcg
31 from pyvcg.driver.file_smtlib import SMTLIB_Generator
33 VCG_AVAILABLE = True
34except ImportError: # pragma: no cover
35 VCG_AVAILABLE = False
37try:
38 from pyvcg.driver.cvc5_api import CVC5_Solver
40 CVC5_API_AVAILABLE = True
41except ImportError: # pragma: no cover
42 CVC5_API_AVAILABLE = False
44CVC5_OPTIONS = {
45 "tlimit-per": 2500,
46 "seed": 42,
47 "sat-random-seed": 42,
48}
51class Unsupported(Exception): # pragma: no cover
52 # lobster-exclude: Not safety relevant
53 def __init__(self, node, text):
54 assert isinstance(node, Node)
55 assert isinstance(text, str) or text is None
56 super().__init__()
57 self.message = "%s not yet supported in VCG" % (
58 text if text else node.__class__.__name__
59 )
60 self.location = node.location
63class Feedback:
64 # lobster-exclude: Not safety relevant
65 def __init__(self, node, message, kind, expect_unsat=True):
66 assert isinstance(node, Expression)
67 assert isinstance(message, str)
68 assert isinstance(kind, str)
69 assert isinstance(expect_unsat, bool)
70 self.node = node
71 self.message = message
72 self.kind = "vcg-" + kind
73 self.expect_unsat = expect_unsat
76class VCG:
77 # lobster-exclude: Not safety relevant
78 def __init__(self, mh, n_ctyp, debug):
79 assert VCG_AVAILABLE
80 assert isinstance(mh, Message_Handler)
81 assert isinstance(n_ctyp, Composite_Type)
82 assert isinstance(debug, bool)
84 self.mh = mh
85 self.n_ctyp = n_ctyp
86 self.debug = debug
88 self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name, n_ctyp.name)
90 self.tmp_id = 0
92 self.vcg = vcg.VCG()
93 self.graph = self.vcg.graph
94 self.start = self.vcg.start
95 # Current start node, we will update this as we go along.
96 self.preamble = None
97 # We do remember the first node where we put all our
98 # declarations, in case we need to add some more later.
100 self.constants = {}
101 self.enumerations = {}
102 self.tuples = {}
103 self.records = {}
104 self.arrays = {}
105 self.bound_vars = {}
106 self.qe_vars = {}
107 self.tuple_base = {}
108 self.uf_records = {}
110 self.uf_matches = None
111 # Pointer to the UF we use for matches. We only generate it
112 # when we must, as it may affect the logics selected due to
113 # string theory being used.
115 self.functional = False
116 # If set to true, then we ignore validity checks and do not
117 # create intermediates. We just build the value and validity
118 # expressions and return them.
120 self.emit_checks = True
121 # If set to false, we skip creating checks.
123 @staticmethod
124 def flag_unsupported(node, text=None): # pragma: no cover
125 assert isinstance(node, Node)
126 raise Unsupported(node, text)
128 def new_temp_name(self):
129 self.tmp_id += 1
130 return "tmp.%u" % self.tmp_id
132 def get_uf_matches(self):
133 if self.uf_matches is None:
134 self.uf_matches = smt.Function(
135 "trlc.matches",
136 smt.BUILTIN_BOOLEAN,
137 smt.Bound_Variable(smt.BUILTIN_STRING, "subject"),
138 smt.Bound_Variable(smt.BUILTIN_STRING, "regex"),
139 )
141 # Create UF for the matches function (for now, later we
142 # will deal with regex properly).
143 self.preamble.add_statement(smt.Function_Declaration(self.uf_matches))
145 return self.uf_matches
147 def create_return(self, node, s_value, s_valid=None):
148 assert isinstance(node, Expression)
149 assert isinstance(s_value, smt.Expression)
150 assert isinstance(s_valid, smt.Expression) or s_valid is None
152 if s_valid is None: 152 ↛ 155line 152 didn't jump to line 155 because the condition on line 152 was always true
153 s_valid = smt.Boolean_Literal(True)
155 if self.functional:
156 return s_value, s_valid
158 else:
159 sym_result = smt.Constant(s_value.sort, self.new_temp_name())
160 self.attach_temp_declaration(node, sym_result, s_value)
162 return sym_result, s_valid
164 def attach_validity_check(self, bool_expr, origin):
165 assert isinstance(bool_expr, smt.Expression)
166 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
167 assert isinstance(origin, Expression)
168 assert not self.functional
170 if not self.emit_checks:
171 return
173 # Attach new graph node advance start
174 if not bool_expr.is_static_true():
175 gn_check = graph.Check(self.graph)
176 gn_check.add_goal(
177 bool_expr,
178 Feedback(origin, "expression could be null", "evaluation-of-null"),
179 "validity check for %s" % origin.to_string(),
180 )
181 self.start.add_edge_to(gn_check)
182 self.start = gn_check
184 def attach_int_division_check(self, int_expr, origin):
185 assert isinstance(int_expr, smt.Expression)
186 assert int_expr.sort is smt.BUILTIN_INTEGER
187 assert isinstance(origin, Expression)
188 assert not self.functional
190 if not self.emit_checks: 190 ↛ 191line 190 didn't jump to line 191 because the condition on line 190 was never true
191 return
193 # Attach new graph node advance start
194 gn_check = graph.Check(self.graph)
195 gn_check.add_goal(
196 smt.Boolean_Negation(smt.Comparison("=", int_expr, smt.Integer_Literal(0))),
197 Feedback(origin, "divisor could be 0", "div-by-zero"),
198 "division by zero check for %s" % origin.to_string(),
199 )
200 self.start.add_edge_to(gn_check)
201 self.start = gn_check
203 def attach_real_division_check(self, real_expr, origin):
204 assert isinstance(real_expr, smt.Expression)
205 assert real_expr.sort is smt.BUILTIN_REAL
206 assert isinstance(origin, Expression)
207 assert not self.functional
209 if not self.emit_checks: 209 ↛ 210line 209 didn't jump to line 210 because the condition on line 209 was never true
210 return
212 # Attach new graph node advance start
213 gn_check = graph.Check(self.graph)
214 gn_check.add_goal(
215 smt.Boolean_Negation(smt.Comparison("=", real_expr, smt.Real_Literal(0))),
216 Feedback(origin, "divisor could be 0.0", "div-by-zero"),
217 "division by zero check for %s" % origin.to_string(),
218 )
219 self.start.add_edge_to(gn_check)
220 self.start = gn_check
222 def attach_index_check(self, seq_expr, index_expr, origin):
223 assert isinstance(seq_expr, smt.Expression)
224 assert isinstance(seq_expr.sort, smt.Sequence_Sort)
225 assert isinstance(index_expr, smt.Expression)
226 assert index_expr.sort is smt.BUILTIN_INTEGER
227 assert isinstance(origin, Binary_Expression)
228 assert origin.operator == Binary_Operator.INDEX
229 assert not self.functional
231 if not self.emit_checks: 231 ↛ 232line 231 didn't jump to line 232 because the condition on line 231 was never true
232 return
234 # Attach new graph node advance start
235 gn_check = graph.Check(self.graph)
236 gn_check.add_goal(
237 smt.Comparison(">=", index_expr, smt.Integer_Literal(0)),
238 Feedback(origin, "array index could be less than 0", "array-index"),
239 "index lower bound check for %s" % origin.to_string(),
240 )
241 gn_check.add_goal(
242 smt.Comparison("<", index_expr, smt.Sequence_Length(seq_expr)),
243 Feedback(
244 origin,
245 "array index could be larger than len(%s)" % origin.n_lhs.to_string(),
246 "array-index",
247 ),
248 "index lower bound check for %s" % origin.to_string(),
249 )
251 self.start.add_edge_to(gn_check)
252 self.start = gn_check
254 def attach_feasability_check(self, bool_expr, origin):
255 assert isinstance(bool_expr, smt.Expression)
256 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
257 assert isinstance(origin, Expression)
258 assert not self.functional
260 if not self.emit_checks:
261 return
263 # Attach new graph node advance start
264 gn_check = graph.Check(self.graph)
265 gn_check.add_goal(
266 bool_expr,
267 Feedback(
268 origin, "expression is always true", "always-true", expect_unsat=False
269 ),
270 "feasability check for %s" % origin.to_string(),
271 )
272 self.start.add_edge_to(gn_check)
274 def attach_assumption(self, bool_expr):
275 assert isinstance(bool_expr, smt.Expression)
276 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
277 assert not self.functional
279 # Attach new graph node advance start
280 gn_ass = graph.Assumption(self.graph)
281 gn_ass.add_statement(smt.Assertion(bool_expr))
282 self.start.add_edge_to(gn_ass)
283 self.start = gn_ass
285 def attach_temp_declaration(self, node, sym, value=None):
286 assert isinstance(node, (Expression, Action))
287 assert isinstance(sym, smt.Constant)
288 assert isinstance(value, smt.Expression) or value is None
289 assert not self.functional
291 # Attach new graph node advance start
292 gn_decl = graph.Assumption(self.graph)
293 gn_decl.add_statement(
294 smt.Constant_Declaration(
295 symbol=sym,
296 value=value,
297 comment="result of %s at %s"
298 % (node.to_string(), node.location.to_string()),
299 relevant=False,
300 )
301 )
302 self.start.add_edge_to(gn_decl)
303 self.start = gn_decl
305 def attach_empty_assumption(self):
306 assert not self.functional
308 # Attach new graph node advance start
309 gn_decl = graph.Assumption(self.graph)
310 self.start.add_edge_to(gn_decl)
311 self.start = gn_decl
313 def analyze(self):
314 try:
315 self.checks_on_composite_type(self.n_ctyp)
316 except Unsupported as exc: # pragma: no cover
317 self.mh.warning(exc.location, exc.message)
319 def checks_on_composite_type(self, n_ctyp):
320 assert isinstance(n_ctyp, Composite_Type)
322 # Create node for global declarations
323 gn_locals = graph.Assumption(self.graph)
324 self.start.add_edge_to(gn_locals)
325 self.start = gn_locals
326 self.preamble = gn_locals
328 # Create local variables
329 for n_component in n_ctyp.all_components():
330 self.tr_component_decl(n_component, self.start)
332 # Create paths for checks in two phases:
333 # Phase A ("at declaration"): checks that do not follow any
334 # record or union reference via field access. These are fully
335 # self-contained and are analyzed first.
336 # Phase B ("after references"): checks that dereference at
337 # least one record or union reference. They run after Phase A
338 # so that knowledge accumulated from Phase A fatal checks is
339 # available.
340 for phase in (False, True):
341 for n_check in n_ctyp.iter_checks():
342 if n_check.uses_field_access != phase:
343 continue
344 current_start = self.start
345 self.tr_check(n_check)
347 # Only fatal checks contribute to the total knowledge
348 if n_check.severity != "fatal":
349 self.start = current_start
351 # Emit debug graph
352 if self.debug: # pragma: no cover
353 subprocess.run(
354 ["dot", "-Tpdf", "-o%s.pdf" % self.vc_name],
355 input=self.graph.debug_render_dot(),
356 check=True,
357 encoding="UTF-8",
358 )
360 # Generate VCs
361 self.vcg.generate()
363 # Solve VCs and provide feedback
364 nok_feasibility_checks = []
365 ok_feasibility_checks = set()
366 nok_validity_checks = set()
368 for vc_id, vc in enumerate(self.vcg.vcs):
369 if self.debug: # pramga: no cover 369 ↛ 370line 369 didn't jump to line 370 because the condition on line 369 was never true
370 with open(
371 self.vc_name + "_%04u.smt2" % vc_id, "w", encoding="UTF-8"
372 ) as fd:
373 fd.write(vc["script"].generate_vc(SMTLIB_Generator()))
375 # Checks that have already failed don't need to be checked
376 # again on a different path
377 if vc["feedback"].expect_unsat and vc["feedback"] in nok_validity_checks:
378 continue
380 solver = CVC5_Solver()
381 for name, value in CVC5_OPTIONS.items():
382 solver.set_solver_option(name, value)
384 status, values = vc["script"].solve_vc(solver)
386 message = vc["feedback"].message
387 if self.debug: # pragma: no cover
388 message += " [vc_id = %u]" % vc_id
390 if vc["feedback"].expect_unsat:
391 if status != "unsat":
392 self.mh.check(
393 vc["feedback"].node.location,
394 message,
395 vc["feedback"].kind,
396 self.create_counterexample(status, values),
397 )
398 nok_validity_checks.add(vc["feedback"])
399 else:
400 if status == "unsat":
401 nok_feasibility_checks.append(vc["feedback"])
402 else:
403 ok_feasibility_checks.add(vc["feedback"])
405 # This is a bit wonky, but this way we make sure the ordering is
406 # consistent
407 for feedback in nok_feasibility_checks:
408 if feedback not in ok_feasibility_checks:
409 self.mh.check(feedback.node.location, feedback.message, feedback.kind)
410 ok_feasibility_checks.add(feedback)
412 def create_counterexample(self, status, values):
413 rv = [
414 "example %s triggering error:" % self.n_ctyp.__class__.__name__.lower(),
415 " %s bad_potato {" % self.n_ctyp.name,
416 ]
418 for n_component in self.n_ctyp.all_components():
419 id_value = self.tr_component_value_name(n_component)
420 id_valid = self.tr_component_valid_name(n_component)
421 if status == "unknown" and ( 421 ↛ 424line 421 didn't jump to line 424 because the condition on line 421 was never true
422 id_value not in values or id_valid not in values
423 ):
424 rv.append(" %s = ???" % n_component.name)
425 elif values.get(id_valid):
426 rv.append(
427 " %s = %s"
428 % (
429 n_component.name,
430 self.value_to_trlc(n_component.n_typ, values[id_value]),
431 )
432 )
433 else:
434 rv.append(" /* %s is null */" % n_component.name)
436 rv.append(" }")
437 if status == "unknown":
438 rv.append("/* note: counter-example is unreliable in this case */")
439 return "\n".join(rv)
441 def fraction_to_decimal_string(self, num, den):
442 assert isinstance(num, int)
443 assert isinstance(den, int) and den >= 1
445 tmp = den
446 if tmp > 2:
447 while tmp > 1:
448 if tmp % 2 == 0:
449 tmp = tmp // 2
450 elif tmp % 5 == 0:
451 tmp = tmp // 5
452 else:
453 return "%i / %u" % (num, den)
455 rv = str(abs(num) // den)
457 i = abs(num) % den
458 j = den
460 if i > 0:
461 rv += "."
462 while i > 0:
463 i *= 10
464 rv += str(i // j)
465 i = i % j
466 else:
467 rv += ".0"
469 if num < 0:
470 return "-" + rv
471 else:
472 return rv
474 def value_to_trlc(self, n_typ, value):
475 assert isinstance(n_typ, Type)
477 if isinstance(n_typ, Builtin_Integer):
478 return str(value)
480 elif isinstance(n_typ, Builtin_Decimal):
481 if isinstance(value, Fraction):
482 num, den = value.as_integer_ratio()
483 if den >= 1: 483 ↛ 486line 483 didn't jump to line 486 because the condition on line 483 was always true
484 return self.fraction_to_decimal_string(num, den)
485 else:
486 return self.fraction_to_decimal_string(-num, -den)
487 else:
488 return "/* unable to generate precise value */"
490 elif isinstance(n_typ, Builtin_Boolean):
491 return "true" if value else "false"
493 elif isinstance(n_typ, Enumeration_Type):
494 return n_typ.name + "." + value
496 elif isinstance(n_typ, Builtin_String):
497 if "\n" in value:
498 return "'''%s'''" % value
499 else:
500 return '"%s"' % value
502 elif isinstance(n_typ, (Record_Type, Union_Type)):
503 # lobster-trace: LRM.Union_Type_Equality
504 if value < 0:
505 instance_id = value * -2 - 1
506 else:
507 instance_id = value * 2
508 if isinstance(n_typ, Record_Type): 508 ↛ 518line 508 didn't jump to line 518 because the condition on line 508 was always true
509 if n_typ.n_package is self.n_ctyp.n_package:
510 return "%s_instance_%i" % (n_typ.name, instance_id)
511 else:
512 return "%s.%s_instance_%i" % (
513 n_typ.n_package.name,
514 n_typ.name,
515 instance_id,
516 )
517 else:
518 return "instance_%i" % instance_id
520 elif isinstance(n_typ, Tuple_Type):
521 parts = []
522 for n_item in n_typ.iter_sequence():
523 if isinstance(n_item, Composite_Component):
524 if n_item.optional and not value[n_item.name + ".valid"]:
525 parts.pop()
526 break
527 parts.append(
528 self.value_to_trlc(n_item.n_typ, value[n_item.name + ".value"])
529 )
531 else:
532 assert isinstance(n_item, Separator)
533 sep_text = {"AT": "@", "COLON": ":", "SEMICOLON": ";"}.get(
534 n_item.token.kind, n_item.token.value
535 )
536 parts.append(sep_text)
538 if n_typ.has_separators():
539 return "".join(parts)
540 else:
541 return "(%s)" % ", ".join(parts)
543 elif isinstance(n_typ, Array_Type):
544 return "[%s]" % ", ".join(
545 self.value_to_trlc(n_typ.element_type, item) for item in value
546 )
548 else: # pragma: no cover
549 self.flag_unsupported(n_typ, "back-conversion from %s" % n_typ.name)
551 def tr_component_value_name(self, n_component):
552 return (
553 n_component.member_of.fully_qualified_name()
554 + "."
555 + n_component.name
556 + ".value"
557 )
559 def tr_component_valid_name(self, n_component):
560 return (
561 n_component.member_of.fully_qualified_name()
562 + "."
563 + n_component.name
564 + ".valid"
565 )
567 def emit_tuple_constraints(self, n_tuple, s_sym):
568 assert isinstance(n_tuple, Tuple_Type)
569 assert isinstance(s_sym, smt.Constant)
571 old_functional, self.functional = self.functional, True
572 self.tuple_base[n_tuple] = s_sym
574 constraints = []
576 # The first tuple constraint is that all checks must have
577 # passed, otherwise the tool would just error. An error in a
578 # tuple is pretty much the same as a fatal in the enclosing
579 # record.
581 for n_check in n_tuple.iter_checks():
582 if n_check.severity == "warning":
583 continue
584 # We do consider both fatal and errors to be sources of
585 # truth here.
586 c_value, _ = self.tr_expression(n_check.n_expr)
587 constraints.append(c_value)
589 # The secopnd tuple constraint is that once you get a null
590 # field, all following fields must also be null.
592 components = n_tuple.all_components()
593 for i, component in enumerate(components):
594 if component.optional:
595 condition = smt.Boolean_Negation(
596 smt.Record_Access(s_sym, component.name + ".valid")
597 )
598 consequences = [
599 smt.Boolean_Negation(smt.Record_Access(s_sym, c.name + ".valid"))
600 for c in components[i + 1 :]
601 ]
602 if len(consequences) == 0:
603 break
604 elif len(consequences) == 1: 604 ↛ 607line 604 didn't jump to line 607 because the condition on line 604 was always true
605 consequence = consequences[0]
606 else:
607 consequence = smt.Conjunction(*consequences)
608 constraints.append(smt.Implication(condition, consequence))
610 del self.tuple_base[n_tuple]
611 self.functional = old_functional
613 for cons in constraints:
614 self.start.add_statement(smt.Assertion(cons))
616 def tr_component_decl(self, n_component, gn_locals):
617 assert isinstance(n_component, Composite_Component)
618 assert isinstance(gn_locals, graph.Assumption)
620 if isinstance(self.n_ctyp, Record_Type):
621 frozen = self.n_ctyp.is_frozen(n_component)
622 else:
623 frozen = False
625 id_value = self.tr_component_value_name(n_component)
626 s_sort = self.tr_type(n_component.n_typ)
627 s_sym = smt.Constant(s_sort, id_value)
628 if frozen:
629 old_functional, self.functional = self.functional, True
630 s_val, _ = self.tr_expression(
631 self.n_ctyp.get_freezing_expression(n_component)
632 )
633 self.functional = old_functional
634 else:
635 s_val = None
636 s_decl = smt.Constant_Declaration(
637 symbol=s_sym,
638 value=s_val,
639 comment="value for %s declared on %s"
640 % (n_component.name, n_component.location.to_string()),
641 relevant=True,
642 )
643 gn_locals.add_statement(s_decl)
644 self.constants[id_value] = s_sym
646 if isinstance(n_component.n_typ, Tuple_Type):
647 self.emit_tuple_constraints(n_component.n_typ, s_sym)
649 # For arrays we need to add additional constraints for the
650 # length
651 if isinstance(n_component.n_typ, Array_Type):
652 if n_component.n_typ.lower_bound > 0:
653 s_lower = smt.Integer_Literal(n_component.n_typ.lower_bound)
654 gn_locals.add_statement(
655 smt.Assertion(
656 smt.Comparison(">=", smt.Sequence_Length(s_sym), s_lower)
657 )
658 )
660 if n_component.n_typ.upper_bound is not None:
661 s_upper = smt.Integer_Literal(n_component.n_typ.upper_bound)
662 gn_locals.add_statement(
663 smt.Assertion(
664 smt.Comparison("<=", smt.Sequence_Length(s_sym), s_upper)
665 )
666 )
668 id_valid = self.tr_component_valid_name(n_component)
669 s_sym = smt.Constant(smt.BUILTIN_BOOLEAN, id_valid)
670 s_val = (
671 None if n_component.optional and not frozen else smt.Boolean_Literal(True)
672 )
673 s_decl = smt.Constant_Declaration(symbol=s_sym, value=s_val, relevant=True)
674 gn_locals.add_statement(s_decl)
675 self.constants[id_valid] = s_sym
677 def tr_type(self, n_type):
678 assert isinstance(n_type, Type)
680 if isinstance(n_type, Builtin_Boolean):
681 return smt.BUILTIN_BOOLEAN
683 elif isinstance(n_type, Builtin_Integer):
684 return smt.BUILTIN_INTEGER
686 elif isinstance(n_type, Builtin_Decimal):
687 return smt.BUILTIN_REAL
689 elif isinstance(n_type, Builtin_String):
690 return smt.BUILTIN_STRING
692 elif isinstance(n_type, Enumeration_Type):
693 if n_type not in self.enumerations:
694 s_sort = smt.Enumeration(n_type.n_package.name + "." + n_type.name)
695 for n_lit in n_type.literals.values():
696 s_sort.add_literal(n_lit.name)
697 self.enumerations[n_type] = s_sort
698 self.start.add_statement(
699 smt.Enumeration_Declaration(
700 s_sort,
701 "enumeration %s from %s"
702 % (n_type.name, n_type.location.to_string()),
703 )
704 )
705 return self.enumerations[n_type]
707 elif isinstance(n_type, Tuple_Type):
708 if n_type not in self.tuples:
709 s_sort = smt.Record(n_type.n_package.name + "." + n_type.name)
710 for n_component in n_type.all_components():
711 s_sort.add_component(
712 n_component.name + ".value", self.tr_type(n_component.n_typ)
713 )
714 if n_component.optional:
715 s_sort.add_component(
716 n_component.name + ".valid", smt.BUILTIN_BOOLEAN
717 )
718 self.tuples[n_type] = s_sort
719 self.start.add_statement(
720 smt.Record_Declaration(
721 s_sort,
722 "tuple %s from %s" % (n_type.name, n_type.location.to_string()),
723 )
724 )
726 return self.tuples[n_type]
728 elif isinstance(n_type, Array_Type):
729 if n_type not in self.arrays:
730 s_element_sort = self.tr_type(n_type.element_type)
731 s_sequence = smt.Sequence_Sort(s_element_sort)
732 self.arrays[n_type] = s_sequence
734 return self.arrays[n_type]
736 elif isinstance(n_type, (Record_Type, Union_Type)):
737 # lobster-trace: LRM.union_type
738 # Record and union references are modelled as a free
739 # integer. If we access their field then we use an
740 # uninterpreted function. Some of these have special
741 # meaning:
742 # 0 - the null reference
743 # 1 - the self reference
744 # anything else - uninterpreted
745 return smt.BUILTIN_INTEGER
747 else: # pragma: no cover
748 self.flag_unsupported(n_type)
750 def tr_check(self, n_check):
751 assert isinstance(n_check, Check)
753 # If the check belongs to a different type then we are looking
754 # at a type extension. In this case we do not create checks
755 # again, because if a check would fail it would already have
756 # failed.
757 if n_check.n_type is not self.n_ctyp:
758 old_emit, self.emit_checks = self.emit_checks, False
760 value, valid = self.tr_expression(n_check.n_expr)
761 self.attach_validity_check(valid, n_check.n_expr)
762 self.attach_feasability_check(value, n_check.n_expr)
763 self.attach_assumption(value)
765 if n_check.n_type is not self.n_ctyp:
766 self.emit_checks = old_emit
768 def tr_expression(self, n_expr):
769 value = None
771 if isinstance(n_expr, Name_Reference):
772 return self.tr_name_reference(n_expr)
774 elif isinstance(n_expr, Unary_Expression):
775 return self.tr_unary_expression(n_expr)
777 elif isinstance(n_expr, Binary_Expression):
778 return self.tr_binary_expression(n_expr)
780 elif isinstance(n_expr, Range_Test):
781 return self.tr_range_test(n_expr)
783 elif isinstance(n_expr, OneOf_Expression):
784 return self.tr_oneof_test(n_expr)
786 elif isinstance(n_expr, Conditional_Expression):
787 if self.functional:
788 return self.tr_conditional_expression_functional(n_expr)
789 else:
790 return self.tr_conditional_expression(n_expr)
792 elif isinstance(n_expr, Null_Literal):
793 return None, smt.Boolean_Literal(False)
795 elif isinstance(n_expr, Boolean_Literal):
796 value = smt.Boolean_Literal(n_expr.value)
798 elif isinstance(n_expr, Integer_Literal):
799 value = smt.Integer_Literal(n_expr.value)
801 elif isinstance(n_expr, Decimal_Literal):
802 value = smt.Real_Literal(n_expr.value)
804 elif isinstance(n_expr, Enumeration_Literal):
805 value = smt.Enumeration_Literal(self.tr_type(n_expr.typ), n_expr.value.name)
807 elif isinstance(n_expr, String_Literal):
808 value = smt.String_Literal(n_expr.value)
810 elif isinstance(n_expr, Quantified_Expression):
811 return self.tr_quantified_expression(n_expr)
813 elif isinstance(n_expr, Field_Access_Expression):
814 return self.tr_field_access_expression(n_expr)
816 else: # pragma: no cover
817 self.flag_unsupported(n_expr)
819 return value, smt.Boolean_Literal(True)
821 def tr_name_reference(self, n_ref):
822 assert isinstance(n_ref, Name_Reference)
824 if isinstance(n_ref.entity, Composite_Component):
825 if n_ref.entity.member_of in self.tuple_base:
826 sym = self.tuple_base[n_ref.entity.member_of]
827 if n_ref.entity.optional:
828 s_valid = smt.Record_Access(sym, n_ref.entity.name + ".valid")
829 else:
830 s_valid = smt.Boolean_Literal(True)
831 s_value = smt.Record_Access(sym, n_ref.entity.name + ".value")
832 return s_value, s_valid
834 else:
835 id_value = self.tr_component_value_name(n_ref.entity)
836 id_valid = self.tr_component_valid_name(n_ref.entity)
837 return self.constants[id_value], self.constants[id_valid]
839 else:
840 assert isinstance(n_ref.entity, Quantified_Variable)
841 if n_ref.entity in self.qe_vars:
842 return self.qe_vars[n_ref.entity], smt.Boolean_Literal(True)
843 else:
844 return self.bound_vars[n_ref.entity], smt.Boolean_Literal(True)
846 def tr_unary_expression(self, n_expr):
847 assert isinstance(n_expr, Unary_Expression)
849 operand_value, operand_valid = self.tr_expression(n_expr.n_operand)
850 if not self.functional:
851 self.attach_validity_check(operand_valid, n_expr.n_operand)
853 sym_value = None
855 if n_expr.operator == Unary_Operator.MINUS:
856 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
857 sym_value = smt.Unary_Int_Arithmetic_Op("-", operand_value)
858 else:
859 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
860 sym_value = smt.Unary_Real_Arithmetic_Op("-", operand_value)
862 elif n_expr.operator == Unary_Operator.PLUS:
863 sym_value = operand_value
865 elif n_expr.operator == Unary_Operator.LOGICAL_NOT:
866 sym_value = smt.Boolean_Negation(operand_value)
868 elif n_expr.operator == Unary_Operator.ABSOLUTE_VALUE:
869 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
870 sym_value = smt.Unary_Int_Arithmetic_Op("abs", operand_value)
872 else:
873 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
874 sym_value = smt.Unary_Real_Arithmetic_Op("abs", operand_value)
876 elif n_expr.operator == Unary_Operator.STRING_LENGTH:
877 sym_value = smt.String_Length(operand_value)
879 elif n_expr.operator == Unary_Operator.ARRAY_LENGTH:
880 sym_value = smt.Sequence_Length(operand_value)
882 elif n_expr.operator == Unary_Operator.CONVERSION_TO_DECIMAL:
883 sym_value = smt.Conversion_To_Real(operand_value)
885 elif n_expr.operator == Unary_Operator.CONVERSION_TO_INT:
886 sym_value = smt.Conversion_To_Integer("rna", operand_value)
888 else:
889 self.mh.ice_loc(
890 n_expr, "unexpected unary operator %s" % n_expr.operator.name
891 )
893 return self.create_return(n_expr, sym_value)
895 def tr_binary_expression(self, n_expr):
896 assert isinstance(n_expr, Binary_Expression)
898 # Some operators deal with validity in a different way. We
899 # deal with them first and then exit.
900 if n_expr.operator in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ):
901 return self.tr_op_equality(n_expr)
903 elif n_expr.operator == Binary_Operator.LOGICAL_IMPLIES:
904 return self.tr_op_implication(n_expr)
906 elif n_expr.operator == Binary_Operator.LOGICAL_AND:
907 return self.tr_op_and(n_expr)
909 elif n_expr.operator == Binary_Operator.LOGICAL_OR:
910 return self.tr_op_or(n_expr)
912 # The remaining operators always check for validity, so we can
913 # obtain the values of both sides now.
914 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
915 if not self.functional:
916 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
917 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
918 if not self.functional:
919 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
920 sym_value = None
922 if n_expr.operator == Binary_Operator.LOGICAL_XOR:
923 sym_value = smt.Exclusive_Disjunction(lhs_value, rhs_value)
925 elif n_expr.operator in (
926 Binary_Operator.PLUS,
927 Binary_Operator.MINUS,
928 Binary_Operator.TIMES,
929 Binary_Operator.DIVIDE,
930 Binary_Operator.REMAINDER,
931 ):
932 if isinstance(n_expr.n_lhs.typ, Builtin_String):
933 assert n_expr.operator == Binary_Operator.PLUS
934 sym_value = smt.String_Concatenation(lhs_value, rhs_value)
936 elif isinstance(n_expr.n_lhs.typ, Builtin_Integer):
937 if n_expr.operator in (
938 Binary_Operator.DIVIDE,
939 Binary_Operator.REMAINDER,
940 ):
941 self.attach_int_division_check(rhs_value, n_expr)
943 smt_op = {
944 Binary_Operator.PLUS: "+",
945 Binary_Operator.MINUS: "-",
946 Binary_Operator.TIMES: "*",
947 Binary_Operator.DIVIDE: "floor_div",
948 Binary_Operator.REMAINDER: "ada_remainder",
949 }[n_expr.operator]
951 sym_value = smt.Binary_Int_Arithmetic_Op(smt_op, lhs_value, rhs_value)
953 else:
954 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
955 if n_expr.operator == Binary_Operator.DIVIDE:
956 self.attach_real_division_check(rhs_value, n_expr)
958 smt_op = {
959 Binary_Operator.PLUS: "+",
960 Binary_Operator.MINUS: "-",
961 Binary_Operator.TIMES: "*",
962 Binary_Operator.DIVIDE: "/",
963 }[n_expr.operator]
965 sym_value = smt.Binary_Real_Arithmetic_Op(smt_op, lhs_value, rhs_value)
967 elif n_expr.operator in (
968 Binary_Operator.COMP_LT,
969 Binary_Operator.COMP_LEQ,
970 Binary_Operator.COMP_GT,
971 Binary_Operator.COMP_GEQ,
972 ):
973 smt_op = {
974 Binary_Operator.COMP_LT: "<",
975 Binary_Operator.COMP_LEQ: "<=",
976 Binary_Operator.COMP_GT: ">",
977 Binary_Operator.COMP_GEQ: ">=",
978 }[n_expr.operator]
980 sym_value = smt.Comparison(smt_op, lhs_value, rhs_value)
982 elif n_expr.operator in (
983 Binary_Operator.STRING_CONTAINS,
984 Binary_Operator.STRING_STARTSWITH,
985 Binary_Operator.STRING_ENDSWITH,
986 ):
987 smt_op = {
988 Binary_Operator.STRING_CONTAINS: "contains",
989 Binary_Operator.STRING_STARTSWITH: "prefixof",
990 Binary_Operator.STRING_ENDSWITH: "suffixof",
991 }
993 # LHS / RHS ordering is not a mistake, in SMTLIB it's the
994 # other way around than in TRLC.
995 sym_value = smt.String_Predicate(
996 smt_op[n_expr.operator], rhs_value, lhs_value
997 )
999 elif n_expr.operator == Binary_Operator.STRING_REGEX:
1000 rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None, None).value
1001 assert isinstance(rhs_evaluation, str)
1003 sym_value = smt.Function_Application(
1004 self.get_uf_matches(), lhs_value, smt.String_Literal(rhs_evaluation)
1005 )
1007 elif n_expr.operator == Binary_Operator.INDEX:
1008 self.attach_index_check(lhs_value, rhs_value, n_expr)
1009 sym_value = smt.Sequence_Index(lhs_value, rhs_value)
1011 elif n_expr.operator == Binary_Operator.ARRAY_CONTAINS:
1012 sym_value = smt.Sequence_Contains(rhs_value, lhs_value)
1014 elif n_expr.operator == Binary_Operator.POWER:
1015 # LRM says that the exponent is always static and an
1016 # integer
1017 static_value = n_expr.n_rhs.evaluate(self.mh, None, None).value
1018 assert isinstance(static_value, int) and static_value >= 0
1020 if static_value == 0: 1020 ↛ 1021line 1020 didn't jump to line 1021 because the condition on line 1020 was never true
1021 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1022 sym_value = smt.Integer_Literal(1)
1023 else:
1024 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1025 sym_value = smt.Real_Literal(1)
1027 else:
1028 sym_value = lhs_value
1029 for _ in range(1, static_value):
1030 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1031 sym_value = smt.Binary_Int_Arithmetic_Op(
1032 "*", sym_value, lhs_value
1033 )
1034 else:
1035 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1036 sym_value = smt.Binary_Real_Arithmetic_Op(
1037 "*", sym_value, lhs_value
1038 )
1040 else: # pragma: no cover
1041 self.flag_unsupported(n_expr, n_expr.operator.name)
1043 return self.create_return(n_expr, sym_value)
1045 def tr_range_test(self, n_expr):
1046 assert isinstance(n_expr, Range_Test)
1048 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1049 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1050 lower_value, lower_valid = self.tr_expression(n_expr.n_lower)
1051 self.attach_validity_check(lower_valid, n_expr.n_lower)
1052 upper_value, upper_valid = self.tr_expression(n_expr.n_upper)
1053 self.attach_validity_check(upper_valid, n_expr.n_upper)
1055 sym_value = smt.Conjunction(
1056 smt.Comparison(">=", lhs_value, lower_value),
1057 smt.Comparison("<=", lhs_value, upper_value),
1058 )
1060 return self.create_return(n_expr, sym_value)
1062 def tr_oneof_test(self, n_expr):
1063 assert isinstance(n_expr, OneOf_Expression)
1065 choices = []
1066 for n_choice in n_expr.choices:
1067 c_value, c_valid = self.tr_expression(n_choice)
1068 self.attach_validity_check(c_valid, n_choice)
1069 choices.append(c_value)
1071 negated_choices = [smt.Boolean_Negation(c) for c in choices]
1073 # pylint: disable=consider-using-enumerate
1075 if len(choices) == 1:
1076 result = choices[0]
1077 elif len(choices) == 2:
1078 result = smt.Exclusive_Disjunction(choices[0], choices[1])
1079 else:
1080 assert len(choices) >= 3
1081 values = []
1082 for choice_id in range(len(choices)):
1083 sequence = []
1084 for other_id in range(len(choices)):
1085 if other_id == choice_id:
1086 sequence.append(choices[other_id])
1087 else:
1088 sequence.append(negated_choices[other_id])
1089 values.append(smt.Conjunction(*sequence))
1090 result = smt.Disjunction(*values)
1092 return self.create_return(n_expr, result)
1094 def tr_conditional_expression_functional(self, n_expr):
1095 assert isinstance(n_expr, Conditional_Expression)
1097 s_result, _ = self.tr_expression(n_expr.else_expr)
1098 for n_action in reversed(n_expr.actions):
1099 s_condition, _ = self.tr_expression(n_action.n_cond)
1100 s_true, _ = self.tr_expression(n_action.n_expr)
1101 s_result = smt.Conditional(s_condition, s_true, s_result)
1103 return self.create_return(n_expr, s_result)
1105 def tr_conditional_expression(self, n_expr):
1106 assert isinstance(n_expr, Conditional_Expression)
1107 assert not self.functional
1109 gn_end = graph.Node(self.graph)
1110 sym_result = smt.Constant(self.tr_type(n_expr.typ), self.new_temp_name())
1112 for n_action in n_expr.actions:
1113 test_value, test_valid = self.tr_expression(n_action.n_cond)
1114 self.attach_validity_check(test_valid, n_action.n_cond)
1115 current_start = self.start
1117 # Create path where action is true
1118 self.attach_assumption(test_value)
1119 res_value, res_valid = self.tr_expression(n_action.n_expr)
1120 self.attach_validity_check(res_valid, n_action.n_expr)
1121 self.attach_temp_declaration(n_action, sym_result, res_value)
1122 self.start.add_edge_to(gn_end)
1124 # Reset to test and proceed with the other actions
1125 self.start = current_start
1126 self.attach_assumption(smt.Boolean_Negation(test_value))
1128 # Finally execute the else part
1129 res_value, res_valid = self.tr_expression(n_expr.else_expr)
1130 self.attach_validity_check(res_valid, n_expr.else_expr)
1131 self.attach_temp_declaration(n_expr, sym_result, res_value)
1132 self.start.add_edge_to(gn_end)
1134 # And join
1135 self.start = gn_end
1136 return sym_result, smt.Boolean_Literal(True)
1138 def tr_op_implication(self, n_expr):
1139 assert isinstance(n_expr, Binary_Expression)
1140 assert n_expr.operator == Binary_Operator.LOGICAL_IMPLIES
1142 if self.functional:
1143 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1144 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1145 return self.create_return(n_expr, smt.Implication(lhs_value, rhs_value))
1147 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1148 # Emit VC for validity
1149 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1151 # Split into two paths.
1152 current_start = self.start
1153 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN, self.new_temp_name())
1154 gn_end = graph.Node(self.graph)
1156 ### 1: Implication is not valid
1157 self.start = current_start
1158 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1159 self.attach_temp_declaration(n_expr, sym_result, smt.Boolean_Literal(True))
1160 self.start.add_edge_to(gn_end)
1162 ### 2: Implication is valid.
1163 self.start = current_start
1164 self.attach_assumption(lhs_value)
1165 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1166 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1167 self.attach_temp_declaration(n_expr, sym_result, rhs_value)
1168 self.start.add_edge_to(gn_end)
1170 # Join paths
1171 self.start = gn_end
1173 return sym_result, smt.Boolean_Literal(True)
1175 def tr_op_and(self, n_expr):
1176 assert isinstance(n_expr, Binary_Expression)
1177 assert n_expr.operator == Binary_Operator.LOGICAL_AND
1179 if self.functional:
1180 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1181 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1182 return self.create_return(n_expr, smt.Conjunction(lhs_value, rhs_value))
1184 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1185 # Emit VC for validity
1186 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1188 # Split into two paths.
1189 current_start = self.start
1190 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN, self.new_temp_name())
1191 gn_end = graph.Node(self.graph)
1193 ### 1: LHS is not true
1194 self.start = current_start
1195 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1196 self.attach_temp_declaration(n_expr, sym_result, smt.Boolean_Literal(False))
1197 self.start.add_edge_to(gn_end)
1199 ### 2: LHS is true
1200 self.start = current_start
1201 self.attach_assumption(lhs_value)
1202 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1203 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1204 self.attach_temp_declaration(n_expr, sym_result, rhs_value)
1205 self.start.add_edge_to(gn_end)
1207 # Join paths
1208 self.start = gn_end
1210 return sym_result, smt.Boolean_Literal(True)
1212 def tr_op_or(self, n_expr):
1213 assert isinstance(n_expr, Binary_Expression)
1214 assert n_expr.operator == Binary_Operator.LOGICAL_OR
1216 if self.functional: 1216 ↛ 1217line 1216 didn't jump to line 1217 because the condition on line 1216 was never true
1217 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1218 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1219 return self.create_return(n_expr, smt.Disjunction(lhs_value, rhs_value))
1221 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1222 # Emit VC for validity
1223 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1225 # Split into two paths.
1226 current_start = self.start
1227 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN, self.new_temp_name())
1228 gn_end = graph.Node(self.graph)
1230 ### 1: LHS is true
1231 self.start = current_start
1232 self.attach_assumption(lhs_value)
1233 self.attach_temp_declaration(n_expr, sym_result, smt.Boolean_Literal(True))
1234 self.start.add_edge_to(gn_end)
1236 ### 2: LHS is not true
1237 self.start = current_start
1238 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1239 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1240 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1241 self.attach_temp_declaration(n_expr, sym_result, rhs_value)
1242 self.start.add_edge_to(gn_end)
1244 # Join paths
1245 self.start = gn_end
1247 return sym_result, smt.Boolean_Literal(True)
1249 def tr_core_equality_tuple_component(self, n_component, lhs, rhs):
1250 assert isinstance(n_component, Composite_Component)
1251 assert isinstance(lhs, smt.Expression)
1252 assert isinstance(rhs, smt.Expression)
1254 value_lhs = smt.Record_Access(lhs, n_component.name + ".value")
1255 value_rhs = smt.Record_Access(rhs, n_component.name + ".value")
1256 valid_equal = self.tr_core_equality(n_component.n_typ, value_lhs, value_rhs)
1258 if not n_component.optional:
1259 return valid_equal
1261 valid_lhs = smt.Record_Access(lhs, n_component.name + ".valid")
1262 valid_rhs = smt.Record_Access(rhs, n_component.name + ".valid")
1264 return smt.Conjunction(
1265 smt.Comparison("=", valid_lhs, valid_rhs),
1266 smt.Implication(valid_lhs, valid_equal),
1267 )
1269 def tr_core_equality(self, n_typ, lhs, rhs):
1270 assert isinstance(n_typ, Type)
1271 assert isinstance(lhs, smt.Expression)
1272 assert isinstance(rhs, smt.Expression)
1274 if isinstance(n_typ, Tuple_Type):
1275 parts = []
1276 for n_component in n_typ.all_components():
1277 parts.append(
1278 self.tr_core_equality_tuple_component(n_component, lhs, rhs)
1279 )
1281 if len(parts) == 0: 1281 ↛ 1282line 1281 didn't jump to line 1282 because the condition on line 1281 was never true
1282 return smt.Boolean_Literal(True)
1283 elif len(parts) == 1: 1283 ↛ 1284line 1283 didn't jump to line 1284 because the condition on line 1283 was never true
1284 return parts[0]
1285 else:
1286 result = smt.Conjunction(parts[0], parts[1])
1287 for part in parts[2:]:
1288 result = smt.Conjunction(result, part)
1289 return result
1291 else:
1292 return smt.Comparison("=", lhs, rhs)
1294 def tr_op_equality(self, n_expr):
1295 assert isinstance(n_expr, Binary_Expression)
1296 assert n_expr.operator in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ)
1298 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1299 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1301 if lhs_value is None:
1302 comp_typ = n_expr.n_rhs.typ
1303 else:
1304 comp_typ = n_expr.n_lhs.typ
1306 if lhs_valid.is_static_true() and rhs_valid.is_static_true():
1307 # Simplified form, this is just x == y
1308 result = self.tr_core_equality(comp_typ, lhs_value, rhs_value)
1310 elif lhs_valid.is_static_false() and rhs_valid.is_static_false():
1311 # This is null == null, so true
1312 result = smt.Boolean_Literal(True)
1314 elif lhs_value is None: 1314 ↛ 1316line 1314 didn't jump to line 1316 because the condition on line 1314 was never true
1315 # This is null == <expr>, true iff rhs is null
1316 result = smt.Boolean_Negation(rhs_valid)
1318 elif rhs_value is None:
1319 # This is <expr> == null, true iff lhs is null
1320 result = smt.Boolean_Negation(lhs_valid)
1322 else:
1323 # This is <expr> == <expr> without shortcuts
1324 result = smt.Conjunction(
1325 smt.Comparison("=", lhs_valid, rhs_valid),
1326 smt.Implication(
1327 lhs_valid, self.tr_core_equality(comp_typ, lhs_value, rhs_value)
1328 ),
1329 )
1331 if n_expr.operator == Binary_Operator.COMP_NEQ:
1332 result = smt.Boolean_Negation(result)
1334 return self.create_return(n_expr, result)
1336 def tr_quantified_expression(self, n_expr):
1337 assert isinstance(n_expr, Quantified_Expression)
1339 # Nested quantifiers are not supported yet
1340 if self.functional: # pragma: no cover
1341 self.flag_unsupported(n_expr, "functional evaluation of quantifier")
1343 # TRLC quantifier
1344 # (forall x in arr_name => body)
1345 #
1346 # SMT quantifier
1347 # (forall ((i Int))
1348 # (=> (and (>= i 0) (< i (seq.len arr_name)))
1349 # (... (seq.nth arr_name i) ... )))
1350 #
1351 # There is an alternative which is:
1352 # (forall ((element ElementSort))
1353 # (=> (seq.contains arr_name (seq.unit element))
1354 # (... element ...)
1355 #
1356 # However it looks like for CVC5 at least this generates more
1357 # unknown and less unsat if a check depends on the explicit
1358 # value of some sequence member.
1360 # Evaluate subject first and creat a null check
1361 s_subject_value, s_subject_valid = self.tr_name_reference(n_expr.n_source)
1362 self.attach_validity_check(s_subject_valid, n_expr.n_source)
1364 # Create validity checks for the body. We do this by creating
1365 # a new branch and eliminating the quantifier; pretending it's
1366 # a forall (since we want to show that for all evaluations
1367 # it's valid).
1368 current_start = self.start
1369 self.attach_empty_assumption()
1370 src_typ = n_expr.n_source.typ
1371 assert isinstance(src_typ, Array_Type)
1372 s_qe_index = smt.Constant(smt.BUILTIN_INTEGER, self.new_temp_name())
1373 self.start.add_statement(
1374 smt.Constant_Declaration(
1375 symbol=s_qe_index,
1376 comment=(
1377 "quantifier elimination (index) for %s at %s"
1378 % (n_expr.to_string(), n_expr.location.to_string())
1379 ),
1380 )
1381 )
1382 self.start.add_statement(
1383 smt.Assertion(smt.Comparison(">=", s_qe_index, smt.Integer_Literal(0)))
1384 )
1385 self.start.add_statement(
1386 smt.Assertion(
1387 smt.Comparison("<", s_qe_index, smt.Sequence_Length(s_subject_value))
1388 )
1389 )
1390 s_qe_sym = smt.Constant(
1391 self.tr_type(src_typ.element_type), self.new_temp_name()
1392 )
1393 self.start.add_statement(
1394 smt.Constant_Declaration(
1395 symbol=s_qe_sym,
1396 value=smt.Sequence_Index(s_subject_value, s_qe_index),
1397 comment=(
1398 "quantifier elimination (symbol) for %s at %s"
1399 % (n_expr.to_string(), n_expr.location.to_string())
1400 ),
1401 )
1402 )
1403 self.qe_vars[n_expr.n_var] = s_qe_sym
1405 _, b_valid = self.tr_expression(n_expr.n_expr)
1406 self.attach_validity_check(b_valid, n_expr.n_expr)
1408 self.start = current_start
1409 del self.qe_vars[n_expr.n_var]
1411 # We have now shown that any path in the quantifier cannot
1412 # raise exception. Asserting the actual value of the
1413 # quantifier is more awkward.
1415 s_q_idx = smt.Bound_Variable(smt.BUILTIN_INTEGER, self.new_temp_name())
1416 s_q_sym = smt.Sequence_Index(s_subject_value, s_q_idx)
1417 self.bound_vars[n_expr.n_var] = s_q_sym
1419 temp, self.functional = self.functional, True
1420 b_value, _ = self.tr_expression(n_expr.n_expr)
1421 self.functional = temp
1423 bounds_expr = smt.Conjunction(
1424 smt.Comparison(">=", s_q_idx, smt.Integer_Literal(0)),
1425 smt.Comparison("<", s_q_idx, smt.Sequence_Length(s_subject_value)),
1426 )
1427 if n_expr.universal:
1428 value = smt.Quantifier(
1429 "forall", [s_q_idx], smt.Implication(bounds_expr, b_value)
1430 )
1431 else:
1432 value = smt.Quantifier(
1433 "exists", [s_q_idx], smt.Conjunction(bounds_expr, b_value)
1434 )
1436 return value, smt.Boolean_Literal(True)
1438 def _ensure_record_deref(self, type_key, sort_name, uf_name, components):
1439 """Lazily create an SMT record sort and uninterpreted function
1440 for dereferencing integer-encoded references.
1442 :param type_key: cache key; always the canonical sort_name string
1443 :param sort_name: name for the SMT Record sort
1444 :param uf_name: name for the UF mapping integer to sort
1445 :param components: iterable of (field_name, smt_sort, needs_valid)
1446 :returns: (record_sort, to_record_uf)
1447 """
1448 if type_key in self.records:
1449 return self.records[type_key], self.uf_records[type_key]
1451 record_sort = smt.Record(sort_name)
1452 for field_name, field_sort, needs_valid in components:
1453 record_sort.add_component(field_name + ".value", field_sort)
1454 if needs_valid:
1455 record_sort.add_component(field_name + ".valid", smt.BUILTIN_BOOLEAN)
1456 self.records[type_key] = record_sort
1457 self.preamble.add_statement(smt.Record_Declaration(record_sort, sort_name))
1459 to_record_uf = smt.Function(
1460 uf_name, record_sort, smt.Bound_Variable(smt.BUILTIN_INTEGER, "ref")
1461 )
1462 self.preamble.add_statement(smt.Function_Declaration(to_record_uf))
1463 self.uf_records[type_key] = to_record_uf
1465 return record_sort, to_record_uf
1467 def tr_field_access_expression(self, n_expr):
1468 assert isinstance(n_expr, Field_Access_Expression)
1470 prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix)
1471 prefix_typ = n_expr.n_prefix.typ
1472 if not self.functional:
1473 self.attach_validity_check(prefix_valid, n_expr.n_prefix)
1475 if isinstance(prefix_typ, Tuple_Type):
1476 field_value = smt.Record_Access(
1477 prefix_value, n_expr.n_field.name + ".value"
1478 )
1479 if n_expr.n_field.optional:
1480 field_valid = smt.Record_Access(
1481 prefix_value, n_expr.n_field.name + ".valid"
1482 )
1483 else:
1484 field_valid = smt.Boolean_Literal(True)
1486 elif isinstance(prefix_typ, (Record_Type, Union_Type)):
1487 # lobster-trace: LRM.Union_Type_Field_Access
1488 # lobster-trace: LRM.Union_Type_Partial_Field_Access
1489 # lobster-trace: LRM.Union_Type_Partial_Field_Null
1490 # Both Record_Type and Union_Type are represented as
1491 # integers. We create a record sort with accessible
1492 # fields and a UF to dereference the integer.
1493 if isinstance(prefix_typ, Record_Type):
1494 components = [
1495 (c.name, self.tr_type(c.n_typ), c.optional)
1496 for c in prefix_typ.all_components()
1497 ]
1498 sort_name = "%s.%s" % (prefix_typ.n_package.name, prefix_typ.name)
1499 uf_name = "access.%s.%s" % (prefix_typ.n_package.name, prefix_typ.name)
1500 else:
1501 field_map = prefix_typ.get_field_map()
1502 union_id = "_".join(t.fully_qualified_name() for t in prefix_typ.types)
1503 components = [
1504 (
1505 name,
1506 self.tr_type(info["n_typ"]),
1507 info["count"] != info["total"] or info["optional_in_any"],
1508 )
1509 for name, info in field_map.items()
1510 if info["n_typ"] is not None
1511 ]
1512 sort_name = "union." + union_id
1513 uf_name = "access.union." + union_id
1515 _, to_record_uf = self._ensure_record_deref(
1516 sort_name, sort_name, uf_name, components
1517 )
1518 dereference = smt.Function_Application(to_record_uf, prefix_value)
1520 # Perform the field access on the dereferenced record
1521 field_value = smt.Record_Access(dereference, n_expr.n_field.name + ".value")
1522 if isinstance(prefix_typ, Union_Type):
1523 info = prefix_typ.get_field_map()[n_expr.n_field.name]
1524 has_valid = info["count"] != info["total"] or info["optional_in_any"]
1525 else:
1526 has_valid = n_expr.n_field.optional
1528 if has_valid:
1529 field_valid = smt.Record_Access(
1530 dereference, n_expr.n_field.name + ".valid"
1531 )
1532 else:
1533 field_valid = smt.Boolean_Literal(True)
1535 else:
1536 self.mh.ice_loc(
1537 n_expr.n_prefix.location,
1538 "unexpected type %s as prefix of field access"
1539 % n_expr.n_prefix.typ.__class__.__name__,
1540 )
1542 # pylint: disable=possibly-used-before-assignment
1543 return field_value, field_valid