Coverage for trlc/vcg.py: 97%
773 statements
« prev ^ index » next coverage.py v7.10.7, created at 2026-01-15 09:56 +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
32 from pyvcg.driver.cvc5_smtlib import CVC5_File_Solver
33 VCG_AVAILABLE = True
34except ImportError: # pragma: no cover
35 VCG_AVAILABLE = False
37try:
38 from pyvcg.driver.cvc5_api import CVC5_Solver
39 CVC5_API_AVAILABLE = True
40except ImportError: # pragma: no cover
41 CVC5_API_AVAILABLE = False
43CVC5_OPTIONS = {
44 "tlimit-per" : 2500,
45 "seed" : 42,
46 "sat-random-seed" : 42,
47}
50class Unsupported(Exception): # pragma: no cover
51 # lobster-exclude: Not safety relevant
52 def __init__(self, node, text):
53 assert isinstance(node, Node)
54 assert isinstance(text, str) or text is None
55 super().__init__()
56 self.message = "%s not yet supported in VCG" % \
57 (text if text else node.__class__.__name__)
58 self.location = node.location
61class Feedback:
62 # lobster-exclude: Not safety relevant
63 def __init__(self, node, message, kind, expect_unsat=True):
64 assert isinstance(node, Expression)
65 assert isinstance(message, str)
66 assert isinstance(kind, str)
67 assert isinstance(expect_unsat, bool)
68 self.node = node
69 self.message = message
70 self.kind = "vcg-" + kind
71 self.expect_unsat = expect_unsat
74class VCG:
75 # lobster-exclude: Not safety relevant
76 def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None):
77 assert VCG_AVAILABLE
78 assert isinstance(mh, Message_Handler)
79 assert isinstance(n_ctyp, Composite_Type)
80 assert isinstance(debug, bool)
81 assert isinstance(use_api, bool)
82 assert use_api or isinstance(cvc5_binary, str)
84 self.mh = mh
85 self.n_ctyp = n_ctyp
86 self.debug = debug
87 self.use_api = use_api
88 self.cvc5_bin = cvc5_binary
90 self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name,
91 n_ctyp.name)
93 self.tmp_id = 0
95 self.vcg = vcg.VCG()
96 self.graph = self.vcg.graph
97 self.start = self.vcg.start
98 # Current start node, we will update this as we go along.
99 self.preamble = None
100 # We do remember the first node where we put all our
101 # declarations, in case we need to add some more later.
103 self.constants = {}
104 self.enumerations = {}
105 self.tuples = {}
106 self.records = {}
107 self.arrays = {}
108 self.bound_vars = {}
109 self.qe_vars = {}
110 self.tuple_base = {}
111 self.uf_records = {}
113 self.uf_matches = None
114 # Pointer to the UF we use for matches. We only generate it
115 # when we must, as it may affect the logics selected due to
116 # string theory being used.
118 self.functional = False
119 # If set to true, then we ignore validity checks and do not
120 # create intermediates. We just build the value and validity
121 # expresions and return them.
123 self.emit_checks = True
124 # If set to false, we skip creating checks.
126 @staticmethod
127 def flag_unsupported(node, text=None): # pragma: no cover
128 assert isinstance(node, Node)
129 raise Unsupported(node, text)
131 def new_temp_name(self):
132 self.tmp_id += 1
133 return "tmp.%u" % self.tmp_id
135 def get_uf_matches(self):
136 if self.uf_matches is None:
137 self.uf_matches = \
138 smt.Function("trlc.matches",
139 smt.BUILTIN_BOOLEAN,
140 smt.Bound_Variable(smt.BUILTIN_STRING,
141 "subject"),
142 smt.Bound_Variable(smt.BUILTIN_STRING,
143 "regex"))
145 # Create UF for the matches function (for now, later we
146 # will deal with regex properly).
147 self.preamble.add_statement(
148 smt.Function_Declaration(self.uf_matches))
150 return self.uf_matches
152 def create_return(self, node, s_value, s_valid=None):
153 assert isinstance(node, Expression)
154 assert isinstance(s_value, smt.Expression)
155 assert isinstance(s_valid, smt.Expression) or s_valid is None
157 if s_valid is None: 157 ↛ 160line 157 didn't jump to line 160 because the condition on line 157 was always true
158 s_valid = smt.Boolean_Literal(True)
160 if self.functional:
161 return s_value, s_valid
163 else:
164 sym_result = smt.Constant(s_value.sort,
165 self.new_temp_name())
166 self.attach_temp_declaration(node, sym_result, s_value)
168 return sym_result, s_valid
170 def attach_validity_check(self, bool_expr, origin):
171 assert isinstance(bool_expr, smt.Expression)
172 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
173 assert isinstance(origin, Expression)
174 assert not self.functional
176 if not self.emit_checks:
177 return
179 # Attach new graph node advance start
180 if not bool_expr.is_static_true():
181 gn_check = graph.Check(self.graph)
182 gn_check.add_goal(bool_expr,
183 Feedback(origin,
184 "expression could be null",
185 "evaluation-of-null"),
186 "validity check for %s" % origin.to_string())
187 self.start.add_edge_to(gn_check)
188 self.start = gn_check
190 def attach_int_division_check(self, int_expr, origin):
191 assert isinstance(int_expr, smt.Expression)
192 assert int_expr.sort is smt.BUILTIN_INTEGER
193 assert isinstance(origin, Expression)
194 assert not self.functional
196 if not self.emit_checks: 196 ↛ 197line 196 didn't jump to line 197 because the condition on line 196 was never true
197 return
199 # Attach new graph node advance start
200 gn_check = graph.Check(self.graph)
201 gn_check.add_goal(
202 smt.Boolean_Negation(
203 smt.Comparison("=", int_expr, smt.Integer_Literal(0))),
204 Feedback(origin,
205 "divisor could be 0",
206 "div-by-zero"),
207 "division by zero check for %s" % origin.to_string())
208 self.start.add_edge_to(gn_check)
209 self.start = gn_check
211 def attach_real_division_check(self, real_expr, origin):
212 assert isinstance(real_expr, smt.Expression)
213 assert real_expr.sort is smt.BUILTIN_REAL
214 assert isinstance(origin, Expression)
215 assert not self.functional
217 if not self.emit_checks: 217 ↛ 218line 217 didn't jump to line 218 because the condition on line 217 was never true
218 return
220 # Attach new graph node advance start
221 gn_check = graph.Check(self.graph)
222 gn_check.add_goal(
223 smt.Boolean_Negation(
224 smt.Comparison("=", real_expr, smt.Real_Literal(0))),
225 Feedback(origin,
226 "divisor could be 0.0",
227 "div-by-zero"),
228 "division by zero check for %s" % origin.to_string())
229 self.start.add_edge_to(gn_check)
230 self.start = gn_check
232 def attach_index_check(self, seq_expr, index_expr, origin):
233 assert isinstance(seq_expr, smt.Expression)
234 assert isinstance(seq_expr.sort, smt.Sequence_Sort)
235 assert isinstance(index_expr, smt.Expression)
236 assert index_expr.sort is smt.BUILTIN_INTEGER
237 assert isinstance(origin, Binary_Expression)
238 assert origin.operator == Binary_Operator.INDEX
239 assert not self.functional
241 if not self.emit_checks: 241 ↛ 242line 241 didn't jump to line 242 because the condition on line 241 was never true
242 return
244 # Attach new graph node advance start
245 gn_check = graph.Check(self.graph)
246 gn_check.add_goal(
247 smt.Comparison(">=", index_expr, smt.Integer_Literal(0)),
248 Feedback(origin,
249 "array index could be less than 0",
250 "array-index"),
251 "index lower bound check for %s" % origin.to_string())
252 gn_check.add_goal(
253 smt.Comparison("<",
254 index_expr,
255 smt.Sequence_Length(seq_expr)),
256 Feedback(origin,
257 "array index could be larger than len(%s)" %
258 origin.n_lhs.to_string(),
259 "array-index"),
260 "index lower bound check for %s" % origin.to_string())
262 self.start.add_edge_to(gn_check)
263 self.start = gn_check
265 def attach_feasability_check(self, bool_expr, origin):
266 assert isinstance(bool_expr, smt.Expression)
267 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
268 assert isinstance(origin, Expression)
269 assert not self.functional
271 if not self.emit_checks:
272 return
274 # Attach new graph node advance start
275 gn_check = graph.Check(self.graph)
276 gn_check.add_goal(bool_expr,
277 Feedback(origin,
278 "expression is always true",
279 "always-true",
280 expect_unsat = False),
281 "feasability check for %s" % origin.to_string())
282 self.start.add_edge_to(gn_check)
284 def attach_assumption(self, bool_expr):
285 assert isinstance(bool_expr, smt.Expression)
286 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
287 assert not self.functional
289 # Attach new graph node advance start
290 gn_ass = graph.Assumption(self.graph)
291 gn_ass.add_statement(smt.Assertion(bool_expr))
292 self.start.add_edge_to(gn_ass)
293 self.start = gn_ass
295 def attach_temp_declaration(self, node, sym, value=None):
296 assert isinstance(node, (Expression, Action))
297 assert isinstance(sym, smt.Constant)
298 assert isinstance(value, smt.Expression) or value is None
299 assert not self.functional
301 # Attach new graph node advance start
302 gn_decl = graph.Assumption(self.graph)
303 gn_decl.add_statement(
304 smt.Constant_Declaration(
305 symbol = sym,
306 value = value,
307 comment = "result of %s at %s" % (node.to_string(),
308 node.location.to_string()),
309 relevant = False))
310 self.start.add_edge_to(gn_decl)
311 self.start = gn_decl
313 def attach_empty_assumption(self):
314 assert not self.functional
316 # Attach new graph node advance start
317 gn_decl = graph.Assumption(self.graph)
318 self.start.add_edge_to(gn_decl)
319 self.start = gn_decl
321 def analyze(self):
322 try:
323 self.checks_on_composite_type(self.n_ctyp)
324 except Unsupported as exc: # pragma: no cover
325 self.mh.warning(exc.location,
326 exc.message)
328 def checks_on_composite_type(self, n_ctyp):
329 assert isinstance(n_ctyp, Composite_Type)
331 # Create node for global declarations
332 gn_locals = graph.Assumption(self.graph)
333 self.start.add_edge_to(gn_locals)
334 self.start = gn_locals
335 self.preamble = gn_locals
337 # Create local variables
338 for n_component in n_ctyp.all_components():
339 self.tr_component_decl(n_component, self.start)
341 # Create paths for checks
342 for n_check in n_ctyp.iter_checks():
343 current_start = self.start
344 self.tr_check(n_check)
346 # Only fatal checks contribute to the total knowledge
347 if n_check.severity != "fatal":
348 self.start = current_start
350 # Emit debug graph
351 if self.debug: # pragma: no cover
352 subprocess.run(["dot", "-Tpdf", "-o%s.pdf" % self.vc_name],
353 input = self.graph.debug_render_dot(),
354 check = True,
355 encoding = "UTF-8")
357 # Generate VCs
358 self.vcg.generate()
360 # Solve VCs and provide feedback
361 nok_feasibility_checks = []
362 ok_feasibility_checks = set()
363 nok_validity_checks = set()
365 for vc_id, vc in enumerate(self.vcg.vcs):
366 if self.debug: # pramga: no cover 366 ↛ 367line 366 didn't jump to line 367 because the condition on line 366 was never true
367 with open(self.vc_name + "_%04u.smt2" % vc_id, "w",
368 encoding="UTF-8") as fd:
369 fd.write(vc["script"].generate_vc(SMTLIB_Generator()))
371 # Checks that have already failed don't need to be checked
372 # again on a different path
373 if vc["feedback"].expect_unsat and \
374 vc["feedback"] in nok_validity_checks:
375 continue
377 if self.use_api:
378 solver = CVC5_Solver()
379 else:
380 solver = CVC5_File_Solver(self.cvc5_bin)
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(vc["feedback"].node.location,
393 message,
394 vc["feedback"].kind,
395 self.create_counterexample(status,
396 values))
397 nok_validity_checks.add(vc["feedback"])
398 else:
399 if status == "unsat":
400 nok_feasibility_checks.append(vc["feedback"])
401 else:
402 ok_feasibility_checks.add(vc["feedback"])
404 # This is a bit wonky, but this way we make sure the ording is
405 # consistent
406 for feedback in nok_feasibility_checks:
407 if feedback not in ok_feasibility_checks:
408 self.mh.check(feedback.node.location,
409 feedback.message,
410 feedback.kind)
411 ok_feasibility_checks.add(feedback)
413 def create_counterexample(self, status, values):
414 rv = [
415 "example %s triggering error:" %
416 self.n_ctyp.__class__.__name__.lower(),
417 " %s bad_potato {" % self.n_ctyp.name
418 ]
420 for n_component in self.n_ctyp.all_components():
421 id_value = self.tr_component_value_name(n_component)
422 id_valid = self.tr_component_valid_name(n_component)
423 if status == "unknown" and (id_value not in values or 423 ↛ 425line 423 didn't jump to line 425 because the condition on line 423 was never true
424 id_valid not in values):
425 rv.append(" %s = ???" % n_component.name)
426 elif values.get(id_valid):
427 rv.append(" %s = %s" %
428 (n_component.name,
429 self.value_to_trlc(n_component.n_typ,
430 values[id_value])))
431 else:
432 rv.append(" /* %s is null */" % n_component.name)
434 rv.append(" }")
435 if status == "unknown":
436 rv.append("/* note: counter-example is unreliable in this case */")
437 return "\n".join(rv)
439 def fraction_to_decimal_string(self, num, den):
440 assert isinstance(num, int)
441 assert isinstance(den, int) and den >= 1
443 tmp = den
444 if tmp > 2:
445 while tmp > 1:
446 if tmp % 2 == 0:
447 tmp = tmp // 2
448 elif tmp % 5 == 0:
449 tmp = tmp // 5
450 else:
451 return "%i / %u" % (num, den)
453 rv = str(abs(num) // den)
455 i = abs(num) % den
456 j = den
458 if i > 0:
459 rv += "."
460 while i > 0:
461 i *= 10
462 rv += str(i // j)
463 i = i % j
464 else:
465 rv += ".0"
467 if num < 0:
468 return "-" + rv
469 else:
470 return rv
472 def value_to_trlc(self, n_typ, value):
473 assert isinstance(n_typ, Type)
475 if isinstance(n_typ, Builtin_Integer):
476 return str(value)
478 elif isinstance(n_typ, Builtin_Decimal):
479 if isinstance(value, Fraction):
480 num, den = value.as_integer_ratio()
481 if den >= 1: 481 ↛ 484line 481 didn't jump to line 484 because the condition on line 481 was always true
482 return self.fraction_to_decimal_string(num, den)
483 else:
484 return self.fraction_to_decimal_string(-num, -den)
485 else:
486 return "/* unable to generate precise value */"
488 elif isinstance(n_typ, Builtin_Boolean):
489 return "true" if value else "false"
491 elif isinstance(n_typ, Enumeration_Type):
492 return n_typ.name + "." + value
494 elif isinstance(n_typ, Builtin_String):
495 if "\n" in value:
496 return "'''%s'''" % value
497 else:
498 return '"%s"' % value
500 elif isinstance(n_typ, Record_Type):
501 if value < 0:
502 instance_id = value * -2 - 1
503 else:
504 instance_id = value * 2
505 if n_typ.n_package is self.n_ctyp.n_package:
506 return "%s_instance_%i" % (n_typ.name, instance_id)
507 else:
508 return "%s.%s_instance_%i" % (n_typ.n_package.name,
509 n_typ.name,
510 instance_id)
512 elif isinstance(n_typ, Tuple_Type):
513 parts = []
514 for n_item in n_typ.iter_sequence():
515 if isinstance(n_item, Composite_Component):
516 if n_item.optional and not value[n_item.name + ".valid"]:
517 parts.pop()
518 break
519 parts.append(
520 self.value_to_trlc(n_item.n_typ,
521 value[n_item.name + ".value"]))
523 else:
524 assert isinstance(n_item, Separator)
525 sep_text = {
526 "AT" : "@",
527 "COLON" : ":",
528 "SEMICOLON" : ";"
529 }.get(n_item.token.kind, n_item.token.value)
530 parts.append(sep_text)
532 if n_typ.has_separators(): 532 ↛ 535line 532 didn't jump to line 535 because the condition on line 532 was always true
533 return "".join(parts)
534 else:
535 return "(%s)" % ", ".join(parts)
537 elif isinstance(n_typ, Array_Type):
538 return "[%s]" % ", ".join(self.value_to_trlc(n_typ.element_type,
539 item)
540 for item in value)
542 else: # pragma: no cover
543 self.flag_unsupported(n_typ,
544 "back-conversion from %s" % n_typ.name)
546 def tr_component_value_name(self, n_component):
547 return n_component.member_of.fully_qualified_name() + \
548 "." + n_component.name + ".value"
550 def tr_component_valid_name(self, n_component):
551 return n_component.member_of.fully_qualified_name() + \
552 "." + n_component.name + ".valid"
554 def emit_tuple_constraints(self, n_tuple, s_sym):
555 assert isinstance(n_tuple, Tuple_Type)
556 assert isinstance(s_sym, smt.Constant)
558 old_functional, self.functional = self.functional, True
559 self.tuple_base[n_tuple] = s_sym
561 constraints = []
563 # The first tuple constraint is that all checks must have
564 # passed, otherwise the tool would just error. An error in a
565 # tuple is pretty much the same as a fatal in the enclosing
566 # record.
568 for n_check in n_tuple.iter_checks():
569 if n_check.severity == "warning":
570 continue
571 # We do consider both fatal and errors to be sources of
572 # truth here.
573 c_value, _ = self.tr_expression(n_check.n_expr)
574 constraints.append(c_value)
576 # The secopnd tuple constraint is that once you get a null
577 # field, all following fields must also be null.
579 components = n_tuple.all_components()
580 for i, component in enumerate(components):
581 if component.optional:
582 condition = smt.Boolean_Negation(
583 smt.Record_Access(s_sym,
584 component.name + ".valid"))
585 consequences = [
586 smt.Boolean_Negation(
587 smt.Record_Access(s_sym,
588 c.name + ".valid"))
589 for c in components[i + 1:]
590 ]
591 if len(consequences) == 0:
592 break
593 elif len(consequences) == 1: 593 ↛ 596line 593 didn't jump to line 596 because the condition on line 593 was always true
594 consequence = consequences[0]
595 else:
596 consequence = smt.Conjunction(*consequences)
597 constraints.append(smt.Implication(condition, consequence))
599 del self.tuple_base[n_tuple]
600 self.functional = old_functional
602 for cons in constraints:
603 self.start.add_statement(smt.Assertion(cons))
605 def tr_component_decl(self, n_component, gn_locals):
606 assert isinstance(n_component, Composite_Component)
607 assert isinstance(gn_locals, graph.Assumption)
609 if isinstance(self.n_ctyp, Record_Type):
610 frozen = self.n_ctyp.is_frozen(n_component)
611 else:
612 frozen = False
614 id_value = self.tr_component_value_name(n_component)
615 s_sort = self.tr_type(n_component.n_typ)
616 s_sym = smt.Constant(s_sort, id_value)
617 if frozen:
618 old_functional, self.functional = self.functional, True
619 s_val, _ = self.tr_expression(
620 self.n_ctyp.get_freezing_expression(n_component))
621 self.functional = old_functional
622 else:
623 s_val = None
624 s_decl = smt.Constant_Declaration(
625 symbol = s_sym,
626 value = s_val,
627 comment = "value for %s declared on %s" % (
628 n_component.name,
629 n_component.location.to_string()),
630 relevant = True)
631 gn_locals.add_statement(s_decl)
632 self.constants[id_value] = s_sym
634 if isinstance(n_component.n_typ, Tuple_Type):
635 self.emit_tuple_constraints(n_component.n_typ, s_sym)
637 # For arrays we need to add additional constraints for the
638 # length
639 if isinstance(n_component.n_typ, Array_Type):
640 if n_component.n_typ.lower_bound > 0:
641 s_lower = smt.Integer_Literal(n_component.n_typ.lower_bound)
642 gn_locals.add_statement(
643 smt.Assertion(
644 smt.Comparison(">=",
645 smt.Sequence_Length(s_sym),
646 s_lower)))
648 if n_component.n_typ.upper_bound is not None:
649 s_upper = smt.Integer_Literal(n_component.n_typ.upper_bound)
650 gn_locals.add_statement(
651 smt.Assertion(
652 smt.Comparison("<=",
653 smt.Sequence_Length(s_sym),
654 s_upper)))
656 id_valid = self.tr_component_valid_name(n_component)
657 s_sym = smt.Constant(smt.BUILTIN_BOOLEAN, id_valid)
658 s_val = (None
659 if n_component.optional and not frozen
660 else smt.Boolean_Literal(True))
661 s_decl = smt.Constant_Declaration(
662 symbol = s_sym,
663 value = s_val,
664 relevant = True)
665 gn_locals.add_statement(s_decl)
666 self.constants[id_valid] = s_sym
668 def tr_type(self, n_type):
669 assert isinstance(n_type, Type)
671 if isinstance(n_type, Builtin_Boolean):
672 return smt.BUILTIN_BOOLEAN
674 elif isinstance(n_type, Builtin_Integer):
675 return smt.BUILTIN_INTEGER
677 elif isinstance(n_type, Builtin_Decimal):
678 return smt.BUILTIN_REAL
680 elif isinstance(n_type, Builtin_String):
681 return smt.BUILTIN_STRING
683 elif isinstance(n_type, Enumeration_Type):
684 if n_type not in self.enumerations:
685 s_sort = smt.Enumeration(n_type.n_package.name +
686 "." + n_type.name)
687 for n_lit in n_type.literals.values():
688 s_sort.add_literal(n_lit.name)
689 self.enumerations[n_type] = s_sort
690 self.start.add_statement(
691 smt.Enumeration_Declaration(
692 s_sort,
693 "enumeration %s from %s" % (
694 n_type.name,
695 n_type.location.to_string())))
696 return self.enumerations[n_type]
698 elif isinstance(n_type, Tuple_Type):
699 if n_type not in self.tuples:
700 s_sort = smt.Record(n_type.n_package.name +
701 "." + n_type.name)
702 for n_component in n_type.all_components():
703 s_sort.add_component(n_component.name + ".value",
704 self.tr_type(n_component.n_typ))
705 if n_component.optional:
706 s_sort.add_component(n_component.name + ".valid",
707 smt.BUILTIN_BOOLEAN)
708 self.tuples[n_type] = s_sort
709 self.start.add_statement(
710 smt.Record_Declaration(
711 s_sort,
712 "tuple %s from %s" % (
713 n_type.name,
714 n_type.location.to_string())))
716 return self.tuples[n_type]
718 elif isinstance(n_type, Array_Type):
719 if n_type not in self.arrays:
720 s_element_sort = self.tr_type(n_type.element_type)
721 s_sequence = smt.Sequence_Sort(s_element_sort)
722 self.arrays[n_type] = s_sequence
724 return self.arrays[n_type]
726 elif isinstance(n_type, Record_Type):
727 # Record references are modelled as a free integer. If we
728 # access their field then we use an uninterpreted
729 # function. Some of these have special meaning:
730 # 0 - the null reference
731 # 1 - the self reference
732 # anything else - uninterpreted
733 return smt.BUILTIN_INTEGER
735 else: # pragma: no cover
736 self.flag_unsupported(n_type)
738 def tr_check(self, n_check):
739 assert isinstance(n_check, Check)
741 # If the check belongs to a different type then we are looking
742 # at a type extension. In this case we do not create checks
743 # again, because if a check would fail it would already have
744 # failed.
745 if n_check.n_type is not self.n_ctyp:
746 old_emit, self.emit_checks = self.emit_checks, False
748 value, valid = self.tr_expression(n_check.n_expr)
749 self.attach_validity_check(valid, n_check.n_expr)
750 self.attach_feasability_check(value, n_check.n_expr)
751 self.attach_assumption(value)
753 if n_check.n_type is not self.n_ctyp:
754 self.emit_checks = old_emit
756 def tr_expression(self, n_expr):
757 value = None
759 if isinstance(n_expr, Name_Reference):
760 return self.tr_name_reference(n_expr)
762 elif isinstance(n_expr, Unary_Expression):
763 return self.tr_unary_expression(n_expr)
765 elif isinstance(n_expr, Binary_Expression):
766 return self.tr_binary_expression(n_expr)
768 elif isinstance(n_expr, Range_Test):
769 return self.tr_range_test(n_expr)
771 elif isinstance(n_expr, OneOf_Expression):
772 return self.tr_oneof_test(n_expr)
774 elif isinstance(n_expr, Conditional_Expression):
775 if self.functional:
776 return self.tr_conditional_expression_functional(n_expr)
777 else:
778 return self.tr_conditional_expression(n_expr)
780 elif isinstance(n_expr, Null_Literal):
781 return None, smt.Boolean_Literal(False)
783 elif isinstance(n_expr, Boolean_Literal):
784 value = smt.Boolean_Literal(n_expr.value)
786 elif isinstance(n_expr, Integer_Literal):
787 value = smt.Integer_Literal(n_expr.value)
789 elif isinstance(n_expr, Decimal_Literal):
790 value = smt.Real_Literal(n_expr.value)
792 elif isinstance(n_expr, Enumeration_Literal):
793 value = smt.Enumeration_Literal(self.tr_type(n_expr.typ),
794 n_expr.value.name)
796 elif isinstance(n_expr, String_Literal):
797 value = smt.String_Literal(n_expr.value)
799 elif isinstance(n_expr, Quantified_Expression):
800 return self.tr_quantified_expression(n_expr)
802 elif isinstance(n_expr, Field_Access_Expression):
803 return self.tr_field_access_expression(n_expr)
805 else: # pragma: no cover
806 self.flag_unsupported(n_expr)
808 return value, smt.Boolean_Literal(True)
810 def tr_name_reference(self, n_ref):
811 assert isinstance(n_ref, Name_Reference)
813 if isinstance(n_ref.entity, Composite_Component):
814 if n_ref.entity.member_of in self.tuple_base:
815 sym = self.tuple_base[n_ref.entity.member_of]
816 if n_ref.entity.optional:
817 s_valid = smt.Record_Access(sym,
818 n_ref.entity.name + ".valid")
819 else:
820 s_valid = smt.Boolean_Literal(True)
821 s_value = smt.Record_Access(sym,
822 n_ref.entity.name + ".value")
823 return s_value, s_valid
825 else:
826 id_value = self.tr_component_value_name(n_ref.entity)
827 id_valid = self.tr_component_valid_name(n_ref.entity)
828 return self.constants[id_value], self.constants[id_valid]
830 else:
831 assert isinstance(n_ref.entity, Quantified_Variable)
832 if n_ref.entity in self.qe_vars:
833 return self.qe_vars[n_ref.entity], smt.Boolean_Literal(True)
834 else:
835 return self.bound_vars[n_ref.entity], smt.Boolean_Literal(True)
837 def tr_unary_expression(self, n_expr):
838 assert isinstance(n_expr, Unary_Expression)
840 operand_value, operand_valid = self.tr_expression(n_expr.n_operand)
841 if not self.functional:
842 self.attach_validity_check(operand_valid, n_expr.n_operand)
844 sym_value = None
846 if n_expr.operator == Unary_Operator.MINUS:
847 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
848 sym_value = smt.Unary_Int_Arithmetic_Op("-",
849 operand_value)
850 else:
851 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
852 sym_value = smt.Unary_Real_Arithmetic_Op("-",
853 operand_value)
855 elif n_expr.operator == Unary_Operator.PLUS:
856 sym_value = operand_value
858 elif n_expr.operator == Unary_Operator.LOGICAL_NOT:
859 sym_value = smt.Boolean_Negation(operand_value)
861 elif n_expr.operator == Unary_Operator.ABSOLUTE_VALUE:
862 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
863 sym_value = smt.Unary_Int_Arithmetic_Op("abs",
864 operand_value)
866 else:
867 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
868 sym_value = smt.Unary_Real_Arithmetic_Op("abs",
869 operand_value)
871 elif n_expr.operator == Unary_Operator.STRING_LENGTH:
872 sym_value = smt.String_Length(operand_value)
874 elif n_expr.operator == Unary_Operator.ARRAY_LENGTH:
875 sym_value = smt.Sequence_Length(operand_value)
877 elif n_expr.operator == Unary_Operator.CONVERSION_TO_DECIMAL:
878 sym_value = smt.Conversion_To_Real(operand_value)
880 elif n_expr.operator == Unary_Operator.CONVERSION_TO_INT:
881 sym_value = smt.Conversion_To_Integer("rna", operand_value)
883 else:
884 self.mh.ice_loc(n_expr,
885 "unexpected unary operator %s" %
886 n_expr.operator.name)
888 return self.create_return(n_expr, sym_value)
890 def tr_binary_expression(self, n_expr):
891 assert isinstance(n_expr, Binary_Expression)
893 # Some operators deal with validity in a different way. We
894 # deal with them first and then exit.
895 if n_expr.operator in (Binary_Operator.COMP_EQ,
896 Binary_Operator.COMP_NEQ):
897 return self.tr_op_equality(n_expr)
899 elif n_expr.operator == Binary_Operator.LOGICAL_IMPLIES:
900 return self.tr_op_implication(n_expr)
902 elif n_expr.operator == Binary_Operator.LOGICAL_AND:
903 return self.tr_op_and(n_expr)
905 elif n_expr.operator == Binary_Operator.LOGICAL_OR:
906 return self.tr_op_or(n_expr)
908 # The remaining operators always check for validity, so we can
909 # obtain the values of both sides now.
910 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
911 if not self.functional:
912 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
913 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
914 if not self.functional:
915 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
916 sym_value = None
918 if n_expr.operator == Binary_Operator.LOGICAL_XOR:
919 sym_value = smt.Exclusive_Disjunction(lhs_value, rhs_value)
921 elif n_expr.operator in (Binary_Operator.PLUS,
922 Binary_Operator.MINUS,
923 Binary_Operator.TIMES,
924 Binary_Operator.DIVIDE,
925 Binary_Operator.REMAINDER):
927 if isinstance(n_expr.n_lhs.typ, Builtin_String):
928 assert n_expr.operator == Binary_Operator.PLUS
929 sym_value = smt.String_Concatenation(lhs_value, rhs_value)
931 elif isinstance(n_expr.n_lhs.typ, Builtin_Integer):
932 if n_expr.operator in (Binary_Operator.DIVIDE,
933 Binary_Operator.REMAINDER):
934 self.attach_int_division_check(rhs_value, n_expr)
936 smt_op = {
937 Binary_Operator.PLUS : "+",
938 Binary_Operator.MINUS : "-",
939 Binary_Operator.TIMES : "*",
940 Binary_Operator.DIVIDE : "floor_div",
941 Binary_Operator.REMAINDER : "ada_remainder",
942 }[n_expr.operator]
944 sym_value = smt.Binary_Int_Arithmetic_Op(smt_op,
945 lhs_value,
946 rhs_value)
948 else:
949 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
950 if n_expr.operator == Binary_Operator.DIVIDE:
951 self.attach_real_division_check(rhs_value, n_expr)
953 smt_op = {
954 Binary_Operator.PLUS : "+",
955 Binary_Operator.MINUS : "-",
956 Binary_Operator.TIMES : "*",
957 Binary_Operator.DIVIDE : "/",
958 }[n_expr.operator]
960 sym_value = smt.Binary_Real_Arithmetic_Op(smt_op,
961 lhs_value,
962 rhs_value)
964 elif n_expr.operator in (Binary_Operator.COMP_LT,
965 Binary_Operator.COMP_LEQ,
966 Binary_Operator.COMP_GT,
967 Binary_Operator.COMP_GEQ):
968 smt_op = {
969 Binary_Operator.COMP_LT : "<",
970 Binary_Operator.COMP_LEQ : "<=",
971 Binary_Operator.COMP_GT : ">",
972 Binary_Operator.COMP_GEQ : ">=",
973 }[n_expr.operator]
975 sym_value = smt.Comparison(smt_op, lhs_value, rhs_value)
977 elif n_expr.operator in (Binary_Operator.STRING_CONTAINS,
978 Binary_Operator.STRING_STARTSWITH,
979 Binary_Operator.STRING_ENDSWITH):
981 smt_op = {
982 Binary_Operator.STRING_CONTAINS : "contains",
983 Binary_Operator.STRING_STARTSWITH : "prefixof",
984 Binary_Operator.STRING_ENDSWITH : "suffixof"
985 }
987 # LHS / RHS ordering is not a mistake, in SMTLIB it's the
988 # other way around than in TRLC.
989 sym_value = smt.String_Predicate(smt_op[n_expr.operator],
990 rhs_value,
991 lhs_value)
993 elif n_expr.operator == Binary_Operator.STRING_REGEX:
994 rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None, None).value
995 assert isinstance(rhs_evaluation, str)
997 sym_value = smt.Function_Application(
998 self.get_uf_matches(),
999 lhs_value,
1000 smt.String_Literal(rhs_evaluation))
1002 elif n_expr.operator == Binary_Operator.INDEX:
1003 self.attach_index_check(lhs_value, rhs_value, n_expr)
1004 sym_value = smt.Sequence_Index(lhs_value, rhs_value)
1006 elif n_expr.operator == Binary_Operator.ARRAY_CONTAINS:
1007 sym_value = smt.Sequence_Contains(rhs_value, lhs_value)
1009 elif n_expr.operator == Binary_Operator.POWER:
1010 # LRM says that the exponent is always static and an
1011 # integer
1012 static_value = n_expr.n_rhs.evaluate(self.mh, None, None).value
1013 assert isinstance(static_value, int) and static_value >= 0
1015 if static_value == 0: 1015 ↛ 1016line 1015 didn't jump to line 1016 because the condition on line 1015 was never true
1016 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1017 sym_value = smt.Integer_Literal(1)
1018 else:
1019 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1020 sym_value = smt.Real_Literal(1)
1022 else:
1023 sym_value = lhs_value
1024 for _ in range(1, static_value):
1025 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1026 sym_value = smt.Binary_Int_Arithmetic_Op("*",
1027 sym_value,
1028 lhs_value)
1029 else:
1030 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1031 sym_value = smt.Binary_Real_Arithmetic_Op("*",
1032 sym_value,
1033 lhs_value)
1035 else: # pragma: no cover
1036 self.flag_unsupported(n_expr, n_expr.operator.name)
1038 return self.create_return(n_expr, sym_value)
1040 def tr_range_test(self, n_expr):
1041 assert isinstance(n_expr, Range_Test)
1043 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1044 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1045 lower_value, lower_valid = self.tr_expression(n_expr.n_lower)
1046 self.attach_validity_check(lower_valid, n_expr.n_lower)
1047 upper_value, upper_valid = self.tr_expression(n_expr.n_upper)
1048 self.attach_validity_check(upper_valid, n_expr.n_upper)
1050 sym_value = smt.Conjunction(
1051 smt.Comparison(">=", lhs_value, lower_value),
1052 smt.Comparison("<=", lhs_value, upper_value))
1054 return self.create_return(n_expr, sym_value)
1056 def tr_oneof_test(self, n_expr):
1057 assert isinstance(n_expr, OneOf_Expression)
1059 choices = []
1060 for n_choice in n_expr.choices:
1061 c_value, c_valid = self.tr_expression(n_choice)
1062 self.attach_validity_check(c_valid, n_choice)
1063 choices.append(c_value)
1065 negated_choices = [smt.Boolean_Negation(c)
1066 for c in choices]
1068 # pylint: disable=consider-using-enumerate
1070 if len(choices) == 1:
1071 result = choices[0]
1072 elif len(choices) == 2:
1073 result = smt.Exclusive_Disjunction(choices[0], choices[1])
1074 else:
1075 assert len(choices) >= 3
1076 values = []
1077 for choice_id in range(len(choices)):
1078 sequence = []
1079 for other_id in range(len(choices)):
1080 if other_id == choice_id:
1081 sequence.append(choices[other_id])
1082 else:
1083 sequence.append(negated_choices[other_id])
1084 values.append(smt.Conjunction(*sequence))
1085 result = smt.Disjunction(*values)
1087 return self.create_return(n_expr, result)
1089 def tr_conditional_expression_functional(self, n_expr):
1090 assert isinstance(n_expr, Conditional_Expression)
1092 s_result, _ = self.tr_expression(n_expr.else_expr)
1093 for n_action in reversed(n_expr.actions):
1094 s_condition, _ = self.tr_expression(n_action.n_cond)
1095 s_true, _ = self.tr_expression(n_action.n_expr)
1096 s_result = smt.Conditional(s_condition, s_true, s_result)
1098 return self.create_return(n_expr, s_result)
1100 def tr_conditional_expression(self, n_expr):
1101 assert isinstance(n_expr, Conditional_Expression)
1102 assert not self.functional
1104 gn_end = graph.Node(self.graph)
1105 sym_result = smt.Constant(self.tr_type(n_expr.typ),
1106 self.new_temp_name())
1108 for n_action in n_expr.actions:
1109 test_value, test_valid = self.tr_expression(n_action.n_cond)
1110 self.attach_validity_check(test_valid, n_action.n_cond)
1111 current_start = self.start
1113 # Create path where action is true
1114 self.attach_assumption(test_value)
1115 res_value, res_valid = self.tr_expression(n_action.n_expr)
1116 self.attach_validity_check(res_valid, n_action.n_expr)
1117 self.attach_temp_declaration(n_action,
1118 sym_result,
1119 res_value)
1120 self.start.add_edge_to(gn_end)
1122 # Reset to test and proceed with the other actions
1123 self.start = current_start
1124 self.attach_assumption(smt.Boolean_Negation(test_value))
1126 # Finally execute the else part
1127 res_value, res_valid = self.tr_expression(n_expr.else_expr)
1128 self.attach_validity_check(res_valid, n_expr.else_expr)
1129 self.attach_temp_declaration(n_expr,
1130 sym_result,
1131 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,
1146 smt.Implication(lhs_value, rhs_value))
1148 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1149 # Emit VC for validity
1150 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1152 # Split into two paths.
1153 current_start = self.start
1154 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1155 self.new_temp_name())
1156 gn_end = graph.Node(self.graph)
1158 ### 1: Implication is not valid
1159 self.start = current_start
1160 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1161 self.attach_temp_declaration(n_expr,
1162 sym_result,
1163 smt.Boolean_Literal(True))
1164 self.start.add_edge_to(gn_end)
1166 ### 2: Implication is valid.
1167 self.start = current_start
1168 self.attach_assumption(lhs_value)
1169 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1170 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1171 self.attach_temp_declaration(n_expr,
1172 sym_result,
1173 rhs_value)
1174 self.start.add_edge_to(gn_end)
1176 # Join paths
1177 self.start = gn_end
1179 return sym_result, smt.Boolean_Literal(True)
1181 def tr_op_and(self, n_expr):
1182 assert isinstance(n_expr, Binary_Expression)
1183 assert n_expr.operator == Binary_Operator.LOGICAL_AND
1185 if self.functional:
1186 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1187 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1188 return self.create_return(n_expr,
1189 smt.Conjunction(lhs_value, rhs_value))
1191 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1192 # Emit VC for validity
1193 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1195 # Split into two paths.
1196 current_start = self.start
1197 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1198 self.new_temp_name())
1199 gn_end = graph.Node(self.graph)
1201 ### 1: LHS is not true
1202 self.start = current_start
1203 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1204 self.attach_temp_declaration(n_expr,
1205 sym_result,
1206 smt.Boolean_Literal(False))
1207 self.start.add_edge_to(gn_end)
1209 ### 2: LHS is true
1210 self.start = current_start
1211 self.attach_assumption(lhs_value)
1212 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1213 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1214 self.attach_temp_declaration(n_expr,
1215 sym_result,
1216 rhs_value)
1217 self.start.add_edge_to(gn_end)
1219 # Join paths
1220 self.start = gn_end
1222 return sym_result, smt.Boolean_Literal(True)
1224 def tr_op_or(self, n_expr):
1225 assert isinstance(n_expr, Binary_Expression)
1226 assert n_expr.operator == Binary_Operator.LOGICAL_OR
1228 if self.functional: 1228 ↛ 1229line 1228 didn't jump to line 1229 because the condition on line 1228 was never true
1229 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1230 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1231 return self.create_return(n_expr,
1232 smt.Disjunction(lhs_value, rhs_value))
1234 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1235 # Emit VC for validity
1236 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1238 # Split into two paths.
1239 current_start = self.start
1240 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1241 self.new_temp_name())
1242 gn_end = graph.Node(self.graph)
1244 ### 1: LHS is true
1245 self.start = current_start
1246 self.attach_assumption(lhs_value)
1247 self.attach_temp_declaration(n_expr,
1248 sym_result,
1249 smt.Boolean_Literal(True))
1250 self.start.add_edge_to(gn_end)
1252 ### 2: LHS is not true
1253 self.start = current_start
1254 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1255 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1256 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1257 self.attach_temp_declaration(n_expr,
1258 sym_result,
1259 rhs_value)
1260 self.start.add_edge_to(gn_end)
1262 # Join paths
1263 self.start = gn_end
1265 return sym_result, smt.Boolean_Literal(True)
1267 def tr_core_equality_tuple_component(self, n_component, lhs, rhs):
1268 assert isinstance(n_component, Composite_Component)
1269 assert isinstance(lhs, smt.Expression)
1270 assert isinstance(rhs, smt.Expression)
1272 value_lhs = smt.Record_Access(lhs,
1273 n_component.name + ".value")
1274 value_rhs = smt.Record_Access(rhs,
1275 n_component.name + ".value")
1276 valid_equal = self.tr_core_equality(n_component.n_typ,
1277 value_lhs,
1278 value_rhs)
1280 if not n_component.optional:
1281 return valid_equal
1283 valid_lhs = smt.Record_Access(lhs,
1284 n_component.name + ".valid")
1285 valid_rhs = smt.Record_Access(rhs,
1286 n_component.name + ".valid")
1288 return smt.Conjunction(
1289 smt.Comparison("=", valid_lhs, valid_rhs),
1290 smt.Implication(valid_lhs, valid_equal))
1292 def tr_core_equality(self, n_typ, lhs, rhs):
1293 assert isinstance(n_typ, Type)
1294 assert isinstance(lhs, smt.Expression)
1295 assert isinstance(rhs, smt.Expression)
1297 if isinstance(n_typ, Tuple_Type):
1298 parts = []
1299 for n_component in n_typ.all_components():
1300 parts.append(
1301 self.tr_core_equality_tuple_component(n_component,
1302 lhs,
1303 rhs))
1305 if len(parts) == 0: 1305 ↛ 1306line 1305 didn't jump to line 1306 because the condition on line 1305 was never true
1306 return smt.Boolean_Literal(True)
1307 elif len(parts) == 1: 1307 ↛ 1308line 1307 didn't jump to line 1308 because the condition on line 1307 was never true
1308 return parts[0]
1309 else:
1310 result = smt.Conjunction(parts[0], parts[1])
1311 for part in parts[2:]:
1312 result = smt.Conjunction(result, part)
1313 return result
1315 else:
1316 return smt.Comparison("=", lhs, rhs)
1318 def tr_op_equality(self, n_expr):
1319 assert isinstance(n_expr, Binary_Expression)
1320 assert n_expr.operator in (Binary_Operator.COMP_EQ,
1321 Binary_Operator.COMP_NEQ)
1323 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1324 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1326 if lhs_value is None:
1327 comp_typ = n_expr.n_rhs.typ
1328 else:
1329 comp_typ = n_expr.n_lhs.typ
1331 if lhs_valid.is_static_true() and rhs_valid.is_static_true():
1332 # Simplified form, this is just x == y
1333 result = self.tr_core_equality(comp_typ,
1334 lhs_value,
1335 rhs_value)
1337 elif lhs_valid.is_static_false() and rhs_valid.is_static_false():
1338 # This is null == null, so true
1339 result = smt.Boolean_Literal(True)
1341 elif lhs_value is None: 1341 ↛ 1343line 1341 didn't jump to line 1343 because the condition on line 1341 was never true
1342 # This is null == <expr>, true iff rhs is null
1343 result = smt.Boolean_Negation(rhs_valid)
1345 elif rhs_value is None:
1346 # This is <expr> == null, true iff lhs is null
1347 result = smt.Boolean_Negation(lhs_valid)
1349 else:
1350 # This is <expr> == <expr> without shortcuts
1351 result = smt.Conjunction(
1352 smt.Comparison("=", lhs_valid, rhs_valid),
1353 smt.Implication(lhs_valid,
1354 self.tr_core_equality(comp_typ,
1355 lhs_value,
1356 rhs_value)))
1358 if n_expr.operator == Binary_Operator.COMP_NEQ:
1359 result = smt.Boolean_Negation(result)
1361 return self.create_return(n_expr, result)
1363 def tr_quantified_expression(self, n_expr):
1364 assert isinstance(n_expr, Quantified_Expression)
1366 # Nested quantifiers are not supported yet
1367 if self.functional: # pragma: no cover
1368 self.flag_unsupported(n_expr,
1369 "functional evaluation of quantifier")
1371 # TRLC quantifier
1372 # (forall x in arr_name => body)
1373 #
1374 # SMT quantifier
1375 # (forall ((i Int))
1376 # (=> (and (>= i 0) (< i (seq.len arr_name)))
1377 # (... (seq.nth arr_name i) ... )))
1378 #
1379 # There is an alternative which is:
1380 # (forall ((element ElementSort))
1381 # (=> (seq.contains arr_name (seq.unit element))
1382 # (... element ...)
1383 #
1384 # However it looks like for CVC5 at least this generates more
1385 # unknown and less unsat if a check depends on the explicit
1386 # value of some sequence member.
1388 # Evaluate subject first and creat a null check
1389 s_subject_value, s_subject_valid = \
1390 self.tr_name_reference(n_expr.n_source)
1391 self.attach_validity_check(s_subject_valid, n_expr.n_source)
1393 # Create validity checks for the body. We do this by creating
1394 # a new branch and eliminating the quantifier; pretending it's
1395 # a forall (since we want to show that for all evaluations
1396 # it's valid).
1397 current_start = self.start
1398 self.attach_empty_assumption()
1399 src_typ = n_expr.n_source.typ
1400 assert isinstance(src_typ, Array_Type)
1401 s_qe_index = smt.Constant(smt.BUILTIN_INTEGER,
1402 self.new_temp_name())
1403 self.start.add_statement(
1404 smt.Constant_Declaration(
1405 symbol = s_qe_index,
1406 comment = ("quantifier elimination (index) for %s at %s" %
1407 (n_expr.to_string(),
1408 n_expr.location.to_string()))))
1409 self.start.add_statement(
1410 smt.Assertion(smt.Comparison(">=",
1411 s_qe_index,
1412 smt.Integer_Literal(0))))
1413 self.start.add_statement(
1414 smt.Assertion(
1415 smt.Comparison("<",
1416 s_qe_index,
1417 smt.Sequence_Length(s_subject_value))))
1418 s_qe_sym = smt.Constant(self.tr_type(src_typ.element_type),
1419 self.new_temp_name())
1420 self.start.add_statement(
1421 smt.Constant_Declaration(
1422 symbol = s_qe_sym,
1423 value = smt.Sequence_Index(s_subject_value, s_qe_index),
1424 comment = ("quantifier elimination (symbol) for %s at %s" %
1425 (n_expr.to_string(),
1426 n_expr.location.to_string()))))
1427 self.qe_vars[n_expr.n_var] = s_qe_sym
1429 _, b_valid = self.tr_expression(n_expr.n_expr)
1430 self.attach_validity_check(b_valid, n_expr.n_expr)
1432 self.start = current_start
1433 del self.qe_vars[n_expr.n_var]
1435 # We have now shown that any path in the quantifier cannot
1436 # raise exception. Asserting the actual value of the
1437 # quantifier is more awkward.
1439 s_q_idx = smt.Bound_Variable(smt.BUILTIN_INTEGER,
1440 self.new_temp_name())
1441 s_q_sym = smt.Sequence_Index(s_subject_value, s_q_idx)
1442 self.bound_vars[n_expr.n_var] = s_q_sym
1444 temp, self.functional = self.functional, True
1445 b_value, _ = self.tr_expression(n_expr.n_expr)
1446 self.functional = temp
1448 bounds_expr = smt.Conjunction(
1449 smt.Comparison(">=",
1450 s_q_idx,
1451 smt.Integer_Literal(0)),
1452 smt.Comparison("<",
1453 s_q_idx,
1454 smt.Sequence_Length(s_subject_value)))
1455 if n_expr.universal:
1456 value = smt.Quantifier(
1457 "forall",
1458 [s_q_idx],
1459 smt.Implication(bounds_expr, b_value))
1460 else:
1461 value = smt.Quantifier(
1462 "exists",
1463 [s_q_idx],
1464 smt.Conjunction(bounds_expr, b_value))
1466 return value, smt.Boolean_Literal(True)
1468 def tr_field_access_expression(self, n_expr):
1469 assert isinstance(n_expr, Field_Access_Expression)
1471 if self.functional: # pragma: no cover
1472 self.flag_unsupported(n_expr,
1473 "functional evaluation of field access")
1475 prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix)
1476 prefix_typ = n_expr.n_prefix.typ
1477 self.attach_validity_check(prefix_valid, n_expr.n_prefix)
1479 if isinstance(prefix_typ, Tuple_Type):
1480 field_value = smt.Record_Access(prefix_value,
1481 n_expr.n_field.name + ".value")
1482 if n_expr.n_field.optional:
1483 field_valid = smt.Record_Access(prefix_value,
1484 n_expr.n_field.name + ".valid")
1485 else:
1486 field_valid = smt.Boolean_Literal(True)
1488 elif isinstance(prefix_typ, Record_Type):
1489 # We need a sort for the record instance + a UF to convert
1490 # the int values into instances of this sort.
1491 if prefix_typ in self.records:
1492 record_sort = self.records[prefix_typ]
1493 to_record_uf = self.uf_records[prefix_typ]
1494 else:
1495 record_sort = smt.Record(prefix_typ.n_package.name +
1496 "." + prefix_typ.name)
1497 for n_component in prefix_typ.all_components():
1498 record_sort.add_component(n_component.name + ".value",
1499 self.tr_type(n_component.n_typ))
1500 if n_component.optional:
1501 record_sort.add_component(n_component.name + ".valid",
1502 smt.BUILTIN_BOOLEAN)
1503 self.records[prefix_typ] = record_sort
1504 self.preamble.add_statement(
1505 smt.Record_Declaration(
1506 record_sort,
1507 "record %s from %s" % (
1508 prefix_typ.name,
1509 prefix_typ.location.to_string())))
1511 to_record_uf = smt.Function(
1512 "access.%s.%s" %
1513 (prefix_typ.n_package.name, prefix_typ.name),
1514 record_sort,
1515 smt.Bound_Variable(smt.BUILTIN_INTEGER, "ref"))
1516 self.preamble.add_statement(
1517 smt.Function_Declaration(to_record_uf))
1519 self.uf_records[prefix_typ] = to_record_uf
1521 # We can now apply the magic int to the UF to get a record
1522 # value
1523 dereference = smt.Function_Application(to_record_uf, prefix_value)
1525 # We can now perform the access on the record value
1526 field_value = smt.Record_Access(dereference,
1527 n_expr.n_field.name + ".value")
1528 if n_expr.n_field.optional:
1529 field_valid = smt.Record_Access(dereference,
1530 n_expr.n_field.name + ".valid")
1531 else:
1532 field_valid = smt.Boolean_Literal(True)
1534 else:
1535 self.mh.ice_loc(n_expr.n_prefix.location,
1536 "unexpected type %s as prefix of field access" %
1537 n_expr.n_prefix.typ.__class__.__name__)
1539 # pylint: disable=possibly-used-before-assignment
1540 return field_value, field_valid