Coverage for trlc/vcg.py: 97%
750 statements
« prev ^ index » next coverage.py v7.7.1, created at 2025-03-27 00:52 +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 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.arrays = {}
107 self.bound_vars = {}
108 self.qe_vars = {}
109 self.tuple_base = {}
111 self.uf_matches = None
112 # Pointer to the UF we use for matches. We only generate it
113 # when we must, as it may affect the logics selected due to
114 # string theory being used.
116 self.functional = False
117 # If set to true, then we ignore validity checks and do not
118 # create intermediates. We just build the value and validity
119 # expresions and return them.
121 self.emit_checks = True
122 # If set to false, we skip creating checks.
124 @staticmethod
125 def flag_unsupported(node, text=None): # pragma: no cover
126 assert isinstance(node, Node)
127 raise Unsupported(node, text)
129 def new_temp_name(self):
130 self.tmp_id += 1
131 return "tmp.%u" % self.tmp_id
133 def get_uf_matches(self):
134 if self.uf_matches is None:
135 self.uf_matches = \
136 smt.Function("trlc.matches",
137 smt.BUILTIN_BOOLEAN,
138 smt.Bound_Variable(smt.BUILTIN_STRING,
139 "subject"),
140 smt.Bound_Variable(smt.BUILTIN_STRING,
141 "regex"))
143 # Create UF for the matches function (for now, later we
144 # will deal with regex properly).
145 self.preamble.add_statement(
146 smt.Function_Declaration(self.uf_matches))
148 return self.uf_matches
150 def create_return(self, node, s_value, s_valid=None):
151 assert isinstance(node, Expression)
152 assert isinstance(s_value, smt.Expression)
153 assert isinstance(s_valid, smt.Expression) or s_valid is None
155 if s_valid is None: 155 ↛ 158line 155 didn't jump to line 158 because the condition on line 155 was always true
156 s_valid = smt.Boolean_Literal(True)
158 if self.functional:
159 return s_value, s_valid
161 else:
162 sym_result = smt.Constant(s_value.sort,
163 self.new_temp_name())
164 self.attach_temp_declaration(node, sym_result, s_value)
166 return sym_result, s_valid
168 def attach_validity_check(self, bool_expr, origin):
169 assert isinstance(bool_expr, smt.Expression)
170 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
171 assert isinstance(origin, Expression)
172 assert not self.functional
174 if not self.emit_checks:
175 return
177 # Attach new graph node advance start
178 if not bool_expr.is_static_true():
179 gn_check = graph.Check(self.graph)
180 gn_check.add_goal(bool_expr,
181 Feedback(origin,
182 "expression could be null",
183 "evaluation-of-null"),
184 "validity check for %s" % origin.to_string())
185 self.start.add_edge_to(gn_check)
186 self.start = gn_check
188 def attach_int_division_check(self, int_expr, origin):
189 assert isinstance(int_expr, smt.Expression)
190 assert int_expr.sort is smt.BUILTIN_INTEGER
191 assert isinstance(origin, Expression)
192 assert not self.functional
194 if not self.emit_checks: 194 ↛ 195line 194 didn't jump to line 195 because the condition on line 194 was never true
195 return
197 # Attach new graph node advance start
198 gn_check = graph.Check(self.graph)
199 gn_check.add_goal(
200 smt.Boolean_Negation(
201 smt.Comparison("=", int_expr, smt.Integer_Literal(0))),
202 Feedback(origin,
203 "divisor could be 0",
204 "div-by-zero"),
205 "division by zero check for %s" % origin.to_string())
206 self.start.add_edge_to(gn_check)
207 self.start = gn_check
209 def attach_real_division_check(self, real_expr, origin):
210 assert isinstance(real_expr, smt.Expression)
211 assert real_expr.sort is smt.BUILTIN_REAL
212 assert isinstance(origin, Expression)
213 assert not self.functional
215 if not self.emit_checks: 215 ↛ 216line 215 didn't jump to line 216 because the condition on line 215 was never true
216 return
218 # Attach new graph node advance start
219 gn_check = graph.Check(self.graph)
220 gn_check.add_goal(
221 smt.Boolean_Negation(
222 smt.Comparison("=", real_expr, smt.Real_Literal(0))),
223 Feedback(origin,
224 "divisor could be 0.0",
225 "div-by-zero"),
226 "division by zero check for %s" % origin.to_string())
227 self.start.add_edge_to(gn_check)
228 self.start = gn_check
230 def attach_index_check(self, seq_expr, index_expr, origin):
231 assert isinstance(seq_expr, smt.Expression)
232 assert isinstance(seq_expr.sort, smt.Sequence_Sort)
233 assert isinstance(index_expr, smt.Expression)
234 assert index_expr.sort is smt.BUILTIN_INTEGER
235 assert isinstance(origin, Binary_Expression)
236 assert origin.operator == Binary_Operator.INDEX
237 assert not self.functional
239 if not self.emit_checks: 239 ↛ 240line 239 didn't jump to line 240 because the condition on line 239 was never true
240 return
242 # Attach new graph node advance start
243 gn_check = graph.Check(self.graph)
244 gn_check.add_goal(
245 smt.Comparison(">=", index_expr, smt.Integer_Literal(0)),
246 Feedback(origin,
247 "array index could be less than 0",
248 "array-index"),
249 "index lower bound check for %s" % origin.to_string())
250 gn_check.add_goal(
251 smt.Comparison("<",
252 index_expr,
253 smt.Sequence_Length(seq_expr)),
254 Feedback(origin,
255 "array index could be larger than len(%s)" %
256 origin.n_lhs.to_string(),
257 "array-index"),
258 "index lower bound check for %s" % origin.to_string())
260 self.start.add_edge_to(gn_check)
261 self.start = gn_check
263 def attach_feasability_check(self, bool_expr, origin):
264 assert isinstance(bool_expr, smt.Expression)
265 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
266 assert isinstance(origin, Expression)
267 assert not self.functional
269 if not self.emit_checks:
270 return
272 # Attach new graph node advance start
273 gn_check = graph.Check(self.graph)
274 gn_check.add_goal(bool_expr,
275 Feedback(origin,
276 "expression is always true",
277 "always-true",
278 expect_unsat = False),
279 "feasability check for %s" % origin.to_string())
280 self.start.add_edge_to(gn_check)
282 def attach_assumption(self, bool_expr):
283 assert isinstance(bool_expr, smt.Expression)
284 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
285 assert not self.functional
287 # Attach new graph node advance start
288 gn_ass = graph.Assumption(self.graph)
289 gn_ass.add_statement(smt.Assertion(bool_expr))
290 self.start.add_edge_to(gn_ass)
291 self.start = gn_ass
293 def attach_temp_declaration(self, node, sym, value=None):
294 assert isinstance(node, (Expression, Action))
295 assert isinstance(sym, smt.Constant)
296 assert isinstance(value, smt.Expression) or value is None
297 assert not self.functional
299 # Attach new graph node advance start
300 gn_decl = graph.Assumption(self.graph)
301 gn_decl.add_statement(
302 smt.Constant_Declaration(
303 symbol = sym,
304 value = value,
305 comment = "result of %s at %s" % (node.to_string(),
306 node.location.to_string()),
307 relevant = False))
308 self.start.add_edge_to(gn_decl)
309 self.start = gn_decl
311 def attach_empty_assumption(self):
312 assert not self.functional
314 # Attach new graph node advance start
315 gn_decl = graph.Assumption(self.graph)
316 self.start.add_edge_to(gn_decl)
317 self.start = gn_decl
319 def analyze(self):
320 try:
321 self.checks_on_composite_type(self.n_ctyp)
322 except Unsupported as exc: # pragma: no cover
323 self.mh.warning(exc.location,
324 exc.message)
326 def checks_on_composite_type(self, n_ctyp):
327 assert isinstance(n_ctyp, Composite_Type)
329 # Create node for global declarations
330 gn_locals = graph.Assumption(self.graph)
331 self.start.add_edge_to(gn_locals)
332 self.start = gn_locals
333 self.preamble = gn_locals
335 # Create local variables
336 for n_component in n_ctyp.all_components():
337 self.tr_component_decl(n_component, self.start)
339 # Create paths for checks
340 for n_check in n_ctyp.iter_checks():
341 current_start = self.start
342 self.tr_check(n_check)
344 # Only fatal checks contribute to the total knowledge
345 if n_check.severity != "fatal":
346 self.start = current_start
348 # Emit debug graph
349 if self.debug: # pragma: no cover
350 subprocess.run(["dot", "-Tpdf", "-o%s.pdf" % self.vc_name],
351 input = self.graph.debug_render_dot(),
352 check = True,
353 encoding = "UTF-8")
355 # Generate VCs
356 self.vcg.generate()
358 # Solve VCs and provide feedback
359 nok_feasibility_checks = []
360 ok_feasibility_checks = set()
361 nok_validity_checks = set()
363 for vc_id, vc in enumerate(self.vcg.vcs):
364 if self.debug: # pramga: no cover 364 ↛ 365line 364 didn't jump to line 365 because the condition on line 364 was never true
365 with open(self.vc_name + "_%04u.smt2" % vc_id, "w",
366 encoding="UTF-8") as fd:
367 fd.write(vc["script"].generate_vc(SMTLIB_Generator()))
369 # Checks that have already failed don't need to be checked
370 # again on a different path
371 if vc["feedback"].expect_unsat and \
372 vc["feedback"] in nok_validity_checks:
373 continue
375 if self.use_api:
376 solver = CVC5_Solver()
377 else:
378 solver = CVC5_File_Solver(self.cvc5_bin)
379 for name, value in CVC5_OPTIONS.items():
380 solver.set_solver_option(name, value)
382 status, values = vc["script"].solve_vc(solver)
384 message = vc["feedback"].message
385 if self.debug: # pragma: no cover
386 message += " [vc_id = %u]" % vc_id
388 if vc["feedback"].expect_unsat:
389 if status != "unsat":
390 self.mh.check(vc["feedback"].node.location,
391 message,
392 vc["feedback"].kind,
393 self.create_counterexample(status,
394 values))
395 nok_validity_checks.add(vc["feedback"])
396 else:
397 if status == "unsat":
398 nok_feasibility_checks.append(vc["feedback"])
399 else:
400 ok_feasibility_checks.add(vc["feedback"])
402 # This is a bit wonky, but this way we make sure the ording is
403 # consistent
404 for feedback in nok_feasibility_checks:
405 if feedback not in ok_feasibility_checks:
406 self.mh.check(feedback.node.location,
407 feedback.message,
408 feedback.kind)
409 ok_feasibility_checks.add(feedback)
411 def create_counterexample(self, status, values):
412 rv = [
413 "example %s triggering error:" %
414 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 (id_value not in values or 421 ↛ 423line 421 didn't jump to line 423 because the condition on line 421 was never true
422 id_valid not in values):
423 rv.append(" %s = ???" % n_component.name)
424 elif values.get(id_valid):
425 rv.append(" %s = %s" %
426 (n_component.name,
427 self.value_to_trlc(n_component.n_typ,
428 values[id_value])))
429 else:
430 rv.append(" /* %s is null */" % n_component.name)
432 rv.append(" }")
433 if status == "unknown":
434 rv.append("/* note: counter-example is unreliable in this case */")
435 return "\n".join(rv)
437 def fraction_to_decimal_string(self, num, den):
438 assert isinstance(num, int)
439 assert isinstance(den, int) and den >= 1
441 tmp = den
442 if tmp > 2:
443 while tmp > 1:
444 if tmp % 2 == 0:
445 tmp = tmp // 2
446 elif tmp % 5 == 0:
447 tmp = tmp // 5
448 else:
449 return "%i / %u" % (num, den)
451 rv = str(abs(num) // den)
453 i = abs(num) % den
454 j = den
456 if i > 0:
457 rv += "."
458 while i > 0:
459 i *= 10
460 rv += str(i // j)
461 i = i % j
462 else:
463 rv += ".0"
465 if num < 0:
466 return "-" + rv
467 else:
468 return rv
470 def value_to_trlc(self, n_typ, value):
471 assert isinstance(n_typ, Type)
473 if isinstance(n_typ, Builtin_Integer):
474 return str(value)
476 elif isinstance(n_typ, Builtin_Decimal):
477 if isinstance(value, Fraction):
478 num, den = value.as_integer_ratio()
479 if den >= 1: 479 ↛ 482line 479 didn't jump to line 482 because the condition on line 479 was always true
480 return self.fraction_to_decimal_string(num, den)
481 else:
482 return self.fraction_to_decimal_string(-num, -den)
483 else:
484 return "/* unable to generate precise value */"
486 elif isinstance(n_typ, Builtin_Boolean):
487 return "true" if value else "false"
489 elif isinstance(n_typ, Enumeration_Type):
490 return n_typ.name + "." + value
492 elif isinstance(n_typ, Builtin_String):
493 if "\n" in value:
494 return "'''%s'''" % value
495 else:
496 return '"%s"' % value
498 elif isinstance(n_typ, Record_Type):
499 if value < 0:
500 instance_id = value * -2 - 1
501 else:
502 instance_id = value * 2
503 if n_typ.n_package is self.n_ctyp.n_package:
504 return "%s_instance_%i" % (n_typ.name, instance_id)
505 else:
506 return "%s.%s_instance_%i" % (n_typ.n_package.name,
507 n_typ.name,
508 instance_id)
510 elif isinstance(n_typ, Tuple_Type):
511 parts = []
512 for n_item in n_typ.iter_sequence():
513 if isinstance(n_item, Composite_Component):
514 if n_item.optional and not value[n_item.name + ".valid"]:
515 parts.pop()
516 break
517 parts.append(
518 self.value_to_trlc(n_item.n_typ,
519 value[n_item.name + ".value"]))
521 else:
522 assert isinstance(n_item, Separator)
523 sep_text = {
524 "AT" : "@",
525 "COLON" : ":",
526 "SEMICOLON" : ";"
527 }.get(n_item.token.kind, n_item.token.value)
528 parts.append(sep_text)
530 if n_typ.has_separators(): 530 ↛ 533line 530 didn't jump to line 533 because the condition on line 530 was always true
531 return "".join(parts)
532 else:
533 return "(%s)" % ", ".join(parts)
535 elif isinstance(n_typ, Array_Type):
536 return "[%s]" % ", ".join(self.value_to_trlc(n_typ.element_type,
537 item)
538 for item in value)
540 else: # pragma: no cover
541 self.flag_unsupported(n_typ,
542 "back-conversion from %s" % n_typ.name)
544 def tr_component_value_name(self, n_component):
545 return n_component.member_of.fully_qualified_name() + \
546 "." + n_component.name + ".value"
548 def tr_component_valid_name(self, n_component):
549 return n_component.member_of.fully_qualified_name() + \
550 "." + n_component.name + ".valid"
552 def emit_tuple_constraints(self, n_tuple, s_sym):
553 assert isinstance(n_tuple, Tuple_Type)
554 assert isinstance(s_sym, smt.Constant)
556 old_functional, self.functional = self.functional, True
557 self.tuple_base[n_tuple] = s_sym
559 constraints = []
561 # The first tuple constraint is that all checks must have
562 # passed, otherwise the tool would just error. An error in a
563 # tuple is pretty much the same as a fatal in the enclosing
564 # record.
566 for n_check in n_tuple.iter_checks():
567 if n_check.severity == "warning":
568 continue
569 # We do consider both fatal and errors to be sources of
570 # truth here.
571 c_value, _ = self.tr_expression(n_check.n_expr)
572 constraints.append(c_value)
574 # The secopnd tuple constraint is that once you get a null
575 # field, all following fields must also be null.
577 components = n_tuple.all_components()
578 for i, component in enumerate(components):
579 if component.optional:
580 condition = smt.Boolean_Negation(
581 smt.Record_Access(s_sym,
582 component.name + ".valid"))
583 consequences = [
584 smt.Boolean_Negation(
585 smt.Record_Access(s_sym,
586 c.name + ".valid"))
587 for c in components[i + 1:]
588 ]
589 if len(consequences) == 0:
590 break
591 elif len(consequences) == 1: 591 ↛ 594line 591 didn't jump to line 594 because the condition on line 591 was always true
592 consequence = consequences[0]
593 else:
594 consequence = smt.Conjunction(*consequences)
595 constraints.append(smt.Implication(condition, consequence))
597 del self.tuple_base[n_tuple]
598 self.functional = old_functional
600 for cons in constraints:
601 self.start.add_statement(smt.Assertion(cons))
603 def tr_component_decl(self, n_component, gn_locals):
604 assert isinstance(n_component, Composite_Component)
605 assert isinstance(gn_locals, graph.Assumption)
607 if isinstance(self.n_ctyp, Record_Type):
608 frozen = self.n_ctyp.is_frozen(n_component)
609 else:
610 frozen = False
612 id_value = self.tr_component_value_name(n_component)
613 s_sort = self.tr_type(n_component.n_typ)
614 s_sym = smt.Constant(s_sort, id_value)
615 if frozen:
616 old_functional, self.functional = self.functional, True
617 s_val, _ = self.tr_expression(
618 self.n_ctyp.get_freezing_expression(n_component))
619 self.functional = old_functional
620 else:
621 s_val = None
622 s_decl = smt.Constant_Declaration(
623 symbol = s_sym,
624 value = s_val,
625 comment = "value for %s declared on %s" % (
626 n_component.name,
627 n_component.location.to_string()),
628 relevant = True)
629 gn_locals.add_statement(s_decl)
630 self.constants[id_value] = s_sym
632 if isinstance(n_component.n_typ, Tuple_Type):
633 self.emit_tuple_constraints(n_component.n_typ, s_sym)
635 # For arrays we need to add additional constraints for the
636 # length
637 if isinstance(n_component.n_typ, Array_Type):
638 if n_component.n_typ.lower_bound > 0:
639 s_lower = smt.Integer_Literal(n_component.n_typ.lower_bound)
640 gn_locals.add_statement(
641 smt.Assertion(
642 smt.Comparison(">=",
643 smt.Sequence_Length(s_sym),
644 s_lower)))
646 if n_component.n_typ.upper_bound is not None:
647 s_upper = smt.Integer_Literal(n_component.n_typ.upper_bound)
648 gn_locals.add_statement(
649 smt.Assertion(
650 smt.Comparison("<=",
651 smt.Sequence_Length(s_sym),
652 s_upper)))
654 id_valid = self.tr_component_valid_name(n_component)
655 s_sym = smt.Constant(smt.BUILTIN_BOOLEAN, id_valid)
656 s_val = (None
657 if n_component.optional and not frozen
658 else smt.Boolean_Literal(True))
659 s_decl = smt.Constant_Declaration(
660 symbol = s_sym,
661 value = s_val,
662 relevant = True)
663 gn_locals.add_statement(s_decl)
664 self.constants[id_valid] = s_sym
666 def tr_type(self, n_type):
667 assert isinstance(n_type, Type)
669 if isinstance(n_type, Builtin_Boolean):
670 return smt.BUILTIN_BOOLEAN
672 elif isinstance(n_type, Builtin_Integer):
673 return smt.BUILTIN_INTEGER
675 elif isinstance(n_type, Builtin_Decimal):
676 return smt.BUILTIN_REAL
678 elif isinstance(n_type, Builtin_String):
679 return smt.BUILTIN_STRING
681 elif isinstance(n_type, Enumeration_Type):
682 if n_type not in self.enumerations:
683 s_sort = smt.Enumeration(n_type.n_package.name +
684 "." + n_type.name)
685 for n_lit in n_type.literals.values():
686 s_sort.add_literal(n_lit.name)
687 self.enumerations[n_type] = s_sort
688 self.start.add_statement(
689 smt.Enumeration_Declaration(
690 s_sort,
691 "enumeration %s from %s" % (
692 n_type.name,
693 n_type.location.to_string())))
694 return self.enumerations[n_type]
696 elif isinstance(n_type, Tuple_Type):
697 if n_type not in self.tuples:
698 s_sort = smt.Record(n_type.n_package.name +
699 "." + n_type.name)
700 for n_component in n_type.all_components():
701 s_sort.add_component(n_component.name + ".value",
702 self.tr_type(n_component.n_typ))
703 if n_component.optional:
704 s_sort.add_component(n_component.name + ".valid",
705 smt.BUILTIN_BOOLEAN)
706 self.tuples[n_type] = s_sort
707 self.start.add_statement(
708 smt.Record_Declaration(
709 s_sort,
710 "tuple %s from %s" % (
711 n_type.name,
712 n_type.location.to_string())))
714 return self.tuples[n_type]
716 elif isinstance(n_type, Array_Type):
717 if n_type not in self.arrays: 717 ↛ 722line 717 didn't jump to line 722 because the condition on line 717 was always true
718 s_element_sort = self.tr_type(n_type.element_type)
719 s_sequence = smt.Sequence_Sort(s_element_sort)
720 self.arrays[n_type] = s_sequence
722 return self.arrays[n_type]
724 elif isinstance(n_type, Record_Type):
725 # Record references are modelled as a free integer, since
726 # we can't really _do_ anything with them. We just need a
727 # variable with infinite range so we can generate
728 # arbitrary fictional record names
729 return smt.BUILTIN_INTEGER
731 else: # pragma: no cover
732 self.flag_unsupported(n_type)
734 def tr_check(self, n_check):
735 assert isinstance(n_check, Check)
737 # If the check belongs to a different type then we are looking
738 # at a type extension. In this case we do not create checks
739 # again, because if a check would failt it would already have
740 # failed.
741 if n_check.n_type is not self.n_ctyp:
742 old_emit, self.emit_checks = self.emit_checks, False
744 value, valid = self.tr_expression(n_check.n_expr)
745 self.attach_validity_check(valid, n_check.n_expr)
746 self.attach_feasability_check(value, n_check.n_expr)
747 self.attach_assumption(value)
749 if n_check.n_type is not self.n_ctyp:
750 self.emit_checks = old_emit
752 def tr_expression(self, n_expr):
753 value = None
755 if isinstance(n_expr, Name_Reference):
756 return self.tr_name_reference(n_expr)
758 elif isinstance(n_expr, Unary_Expression):
759 return self.tr_unary_expression(n_expr)
761 elif isinstance(n_expr, Binary_Expression):
762 return self.tr_binary_expression(n_expr)
764 elif isinstance(n_expr, Range_Test):
765 return self.tr_range_test(n_expr)
767 elif isinstance(n_expr, OneOf_Expression):
768 return self.tr_oneof_test(n_expr)
770 elif isinstance(n_expr, Conditional_Expression):
771 if self.functional:
772 return self.tr_conditional_expression_functional(n_expr)
773 else:
774 return self.tr_conditional_expression(n_expr)
776 elif isinstance(n_expr, Null_Literal):
777 return None, smt.Boolean_Literal(False)
779 elif isinstance(n_expr, Boolean_Literal):
780 value = smt.Boolean_Literal(n_expr.value)
782 elif isinstance(n_expr, Integer_Literal):
783 value = smt.Integer_Literal(n_expr.value)
785 elif isinstance(n_expr, Decimal_Literal):
786 value = smt.Real_Literal(n_expr.value)
788 elif isinstance(n_expr, Enumeration_Literal):
789 value = smt.Enumeration_Literal(self.tr_type(n_expr.typ),
790 n_expr.value.name)
792 elif isinstance(n_expr, String_Literal):
793 value = smt.String_Literal(n_expr.value)
795 elif isinstance(n_expr, Quantified_Expression):
796 return self.tr_quantified_expression(n_expr)
798 elif isinstance(n_expr, Field_Access_Expression):
799 return self.tr_field_access_expression(n_expr)
801 else: # pragma: no cover
802 self.flag_unsupported(n_expr)
804 return value, smt.Boolean_Literal(True)
806 def tr_name_reference(self, n_ref):
807 assert isinstance(n_ref, Name_Reference)
809 if isinstance(n_ref.entity, Composite_Component):
810 if n_ref.entity.member_of in self.tuple_base:
811 sym = self.tuple_base[n_ref.entity.member_of]
812 if n_ref.entity.optional:
813 s_valid = smt.Record_Access(sym,
814 n_ref.entity.name + ".valid")
815 else:
816 s_valid = smt.Boolean_Literal(True)
817 s_value = smt.Record_Access(sym,
818 n_ref.entity.name + ".value")
819 return s_value, s_valid
821 else:
822 id_value = self.tr_component_value_name(n_ref.entity)
823 id_valid = self.tr_component_valid_name(n_ref.entity)
824 return self.constants[id_value], self.constants[id_valid]
826 else:
827 assert isinstance(n_ref.entity, Quantified_Variable)
828 if n_ref.entity in self.qe_vars:
829 return self.qe_vars[n_ref.entity], smt.Boolean_Literal(True)
830 else:
831 return self.bound_vars[n_ref.entity], smt.Boolean_Literal(True)
833 def tr_unary_expression(self, n_expr):
834 assert isinstance(n_expr, Unary_Expression)
836 operand_value, operand_valid = self.tr_expression(n_expr.n_operand)
837 if not self.functional:
838 self.attach_validity_check(operand_valid, n_expr.n_operand)
840 sym_value = None
842 if n_expr.operator == Unary_Operator.MINUS:
843 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
844 sym_value = smt.Unary_Int_Arithmetic_Op("-",
845 operand_value)
846 else:
847 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
848 sym_value = smt.Unary_Real_Arithmetic_Op("-",
849 operand_value)
851 elif n_expr.operator == Unary_Operator.PLUS:
852 sym_value = operand_value
854 elif n_expr.operator == Unary_Operator.LOGICAL_NOT:
855 sym_value = smt.Boolean_Negation(operand_value)
857 elif n_expr.operator == Unary_Operator.ABSOLUTE_VALUE:
858 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
859 sym_value = smt.Unary_Int_Arithmetic_Op("abs",
860 operand_value)
862 else:
863 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
864 sym_value = smt.Unary_Real_Arithmetic_Op("abs",
865 operand_value)
867 elif n_expr.operator == Unary_Operator.STRING_LENGTH:
868 sym_value = smt.String_Length(operand_value)
870 elif n_expr.operator == Unary_Operator.ARRAY_LENGTH:
871 sym_value = smt.Sequence_Length(operand_value)
873 elif n_expr.operator == Unary_Operator.CONVERSION_TO_DECIMAL:
874 sym_value = smt.Conversion_To_Real(operand_value)
876 elif n_expr.operator == Unary_Operator.CONVERSION_TO_INT:
877 sym_value = smt.Conversion_To_Integer("rna", operand_value)
879 else:
880 self.mh.ice_loc(n_expr,
881 "unexpected unary operator %s" %
882 n_expr.operator.name)
884 return self.create_return(n_expr, sym_value)
886 def tr_binary_expression(self, n_expr):
887 assert isinstance(n_expr, Binary_Expression)
889 # Some operators deal with validity in a different way. We
890 # deal with them first and then exit.
891 if n_expr.operator in (Binary_Operator.COMP_EQ,
892 Binary_Operator.COMP_NEQ):
893 return self.tr_op_equality(n_expr)
895 elif n_expr.operator == Binary_Operator.LOGICAL_IMPLIES:
896 return self.tr_op_implication(n_expr)
898 elif n_expr.operator == Binary_Operator.LOGICAL_AND:
899 return self.tr_op_and(n_expr)
901 elif n_expr.operator == Binary_Operator.LOGICAL_OR:
902 return self.tr_op_or(n_expr)
904 # The remaining operators always check for validity, so we can
905 # obtain the values of both sides now.
906 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
907 if not self.functional:
908 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
909 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
910 if not self.functional:
911 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
912 sym_value = None
914 if n_expr.operator == Binary_Operator.LOGICAL_XOR:
915 sym_value = smt.Exclusive_Disjunction(lhs_value, rhs_value)
917 elif n_expr.operator in (Binary_Operator.PLUS,
918 Binary_Operator.MINUS,
919 Binary_Operator.TIMES,
920 Binary_Operator.DIVIDE,
921 Binary_Operator.REMAINDER):
923 if isinstance(n_expr.n_lhs.typ, Builtin_String):
924 assert n_expr.operator == Binary_Operator.PLUS
925 sym_value = smt.String_Concatenation(lhs_value, rhs_value)
927 elif isinstance(n_expr.n_lhs.typ, Builtin_Integer):
928 if n_expr.operator in (Binary_Operator.DIVIDE,
929 Binary_Operator.REMAINDER):
930 self.attach_int_division_check(rhs_value, n_expr)
932 smt_op = {
933 Binary_Operator.PLUS : "+",
934 Binary_Operator.MINUS : "-",
935 Binary_Operator.TIMES : "*",
936 Binary_Operator.DIVIDE : "floor_div",
937 Binary_Operator.REMAINDER : "ada_remainder",
938 }[n_expr.operator]
940 sym_value = smt.Binary_Int_Arithmetic_Op(smt_op,
941 lhs_value,
942 rhs_value)
944 else:
945 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
946 if n_expr.operator == Binary_Operator.DIVIDE:
947 self.attach_real_division_check(rhs_value, n_expr)
949 smt_op = {
950 Binary_Operator.PLUS : "+",
951 Binary_Operator.MINUS : "-",
952 Binary_Operator.TIMES : "*",
953 Binary_Operator.DIVIDE : "/",
954 }[n_expr.operator]
956 sym_value = smt.Binary_Real_Arithmetic_Op(smt_op,
957 lhs_value,
958 rhs_value)
960 elif n_expr.operator in (Binary_Operator.COMP_LT,
961 Binary_Operator.COMP_LEQ,
962 Binary_Operator.COMP_GT,
963 Binary_Operator.COMP_GEQ):
964 smt_op = {
965 Binary_Operator.COMP_LT : "<",
966 Binary_Operator.COMP_LEQ : "<=",
967 Binary_Operator.COMP_GT : ">",
968 Binary_Operator.COMP_GEQ : ">=",
969 }[n_expr.operator]
971 sym_value = smt.Comparison(smt_op, lhs_value, rhs_value)
973 elif n_expr.operator in (Binary_Operator.STRING_CONTAINS,
974 Binary_Operator.STRING_STARTSWITH,
975 Binary_Operator.STRING_ENDSWITH):
977 smt_op = {
978 Binary_Operator.STRING_CONTAINS : "contains",
979 Binary_Operator.STRING_STARTSWITH : "prefixof",
980 Binary_Operator.STRING_ENDSWITH : "suffixof"
981 }
983 # LHS / RHS ordering is not a mistake, in SMTLIB it's the
984 # other way around than in TRLC.
985 sym_value = smt.String_Predicate(smt_op[n_expr.operator],
986 rhs_value,
987 lhs_value)
989 elif n_expr.operator == Binary_Operator.STRING_REGEX:
990 rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None).value
991 assert isinstance(rhs_evaluation, str)
993 sym_value = smt.Function_Application(
994 self.get_uf_matches(),
995 lhs_value,
996 smt.String_Literal(rhs_evaluation))
998 elif n_expr.operator == Binary_Operator.INDEX:
999 self.attach_index_check(lhs_value, rhs_value, n_expr)
1000 sym_value = smt.Sequence_Index(lhs_value, rhs_value)
1002 elif n_expr.operator == Binary_Operator.ARRAY_CONTAINS:
1003 sym_value = smt.Sequence_Contains(rhs_value, lhs_value)
1005 elif n_expr.operator == Binary_Operator.POWER:
1006 # LRM says that the exponent is always static and an
1007 # integer
1008 static_value = n_expr.n_rhs.evaluate(self.mh, None).value
1009 assert isinstance(static_value, int) and static_value >= 0
1011 if static_value == 0: 1011 ↛ 1012line 1011 didn't jump to line 1012 because the condition on line 1011 was never true
1012 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1013 sym_value = smt.Integer_Literal(1)
1014 else:
1015 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1016 sym_value = smt.Real_Literal(1)
1018 else:
1019 sym_value = lhs_value
1020 for _ in range(1, static_value):
1021 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1022 sym_value = smt.Binary_Int_Arithmetic_Op("*",
1023 sym_value,
1024 lhs_value)
1025 else:
1026 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1027 sym_value = smt.Binary_Real_Arithmetic_Op("*",
1028 sym_value,
1029 lhs_value)
1031 else: # pragma: no cover
1032 self.flag_unsupported(n_expr, n_expr.operator.name)
1034 return self.create_return(n_expr, sym_value)
1036 def tr_range_test(self, n_expr):
1037 assert isinstance(n_expr, Range_Test)
1039 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1040 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1041 lower_value, lower_valid = self.tr_expression(n_expr.n_lower)
1042 self.attach_validity_check(lower_valid, n_expr.n_lower)
1043 upper_value, upper_valid = self.tr_expression(n_expr.n_upper)
1044 self.attach_validity_check(upper_valid, n_expr.n_upper)
1046 sym_value = smt.Conjunction(
1047 smt.Comparison(">=", lhs_value, lower_value),
1048 smt.Comparison("<=", lhs_value, upper_value))
1050 return self.create_return(n_expr, sym_value)
1052 def tr_oneof_test(self, n_expr):
1053 assert isinstance(n_expr, OneOf_Expression)
1055 choices = []
1056 for n_choice in n_expr.choices:
1057 c_value, c_valid = self.tr_expression(n_choice)
1058 self.attach_validity_check(c_valid, n_choice)
1059 choices.append(c_value)
1061 negated_choices = [smt.Boolean_Negation(c)
1062 for c in choices]
1064 # pylint: disable=consider-using-enumerate
1066 if len(choices) == 1:
1067 result = choices[0]
1068 elif len(choices) == 2:
1069 result = smt.Exclusive_Disjunction(choices[0], choices[1])
1070 else:
1071 assert len(choices) >= 3
1072 values = []
1073 for choice_id in range(len(choices)):
1074 sequence = []
1075 for other_id in range(len(choices)):
1076 if other_id == choice_id:
1077 sequence.append(choices[other_id])
1078 else:
1079 sequence.append(negated_choices[other_id])
1080 values.append(smt.Conjunction(*sequence))
1081 result = smt.Disjunction(*values)
1083 return self.create_return(n_expr, result)
1085 def tr_conditional_expression_functional(self, n_expr):
1086 assert isinstance(n_expr, Conditional_Expression)
1088 s_result, _ = self.tr_expression(n_expr.else_expr)
1089 for n_action in reversed(n_expr.actions):
1090 s_condition, _ = self.tr_expression(n_action.n_cond)
1091 s_true, _ = self.tr_expression(n_action.n_expr)
1092 s_result = smt.Conditional(s_condition, s_true, s_result)
1094 return self.create_return(n_expr, s_result)
1096 def tr_conditional_expression(self, n_expr):
1097 assert isinstance(n_expr, Conditional_Expression)
1098 assert not self.functional
1100 gn_end = graph.Node(self.graph)
1101 sym_result = smt.Constant(self.tr_type(n_expr.typ),
1102 self.new_temp_name())
1104 for n_action in n_expr.actions:
1105 test_value, test_valid = self.tr_expression(n_action.n_cond)
1106 self.attach_validity_check(test_valid, n_action.n_cond)
1107 current_start = self.start
1109 # Create path where action is true
1110 self.attach_assumption(test_value)
1111 res_value, res_valid = self.tr_expression(n_action.n_expr)
1112 self.attach_validity_check(res_valid, n_action.n_expr)
1113 self.attach_temp_declaration(n_action,
1114 sym_result,
1115 res_value)
1116 self.start.add_edge_to(gn_end)
1118 # Reset to test and proceed with the other actions
1119 self.start = current_start
1120 self.attach_assumption(smt.Boolean_Negation(test_value))
1122 # Finally execute the else part
1123 res_value, res_valid = self.tr_expression(n_expr.else_expr)
1124 self.attach_validity_check(res_valid, n_expr.else_expr)
1125 self.attach_temp_declaration(n_expr,
1126 sym_result,
1127 res_value)
1128 self.start.add_edge_to(gn_end)
1130 # And join
1131 self.start = gn_end
1132 return sym_result, smt.Boolean_Literal(True)
1134 def tr_op_implication(self, n_expr):
1135 assert isinstance(n_expr, Binary_Expression)
1136 assert n_expr.operator == Binary_Operator.LOGICAL_IMPLIES
1138 if self.functional:
1139 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1140 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1141 return self.create_return(n_expr,
1142 smt.Implication(lhs_value, rhs_value))
1144 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1145 # Emit VC for validity
1146 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1148 # Split into two paths.
1149 current_start = self.start
1150 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1151 self.new_temp_name())
1152 gn_end = graph.Node(self.graph)
1154 ### 1: Implication is not valid
1155 self.start = current_start
1156 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1157 self.attach_temp_declaration(n_expr,
1158 sym_result,
1159 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,
1168 sym_result,
1169 rhs_value)
1170 self.start.add_edge_to(gn_end)
1172 # Join paths
1173 self.start = gn_end
1175 return sym_result, smt.Boolean_Literal(True)
1177 def tr_op_and(self, n_expr):
1178 assert isinstance(n_expr, Binary_Expression)
1179 assert n_expr.operator == Binary_Operator.LOGICAL_AND
1181 if self.functional:
1182 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1183 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1184 return self.create_return(n_expr,
1185 smt.Conjunction(lhs_value, rhs_value))
1187 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1188 # Emit VC for validity
1189 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1191 # Split into two paths.
1192 current_start = self.start
1193 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1194 self.new_temp_name())
1195 gn_end = graph.Node(self.graph)
1197 ### 1: LHS is not true
1198 self.start = current_start
1199 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1200 self.attach_temp_declaration(n_expr,
1201 sym_result,
1202 smt.Boolean_Literal(False))
1203 self.start.add_edge_to(gn_end)
1205 ### 2: LHS is true
1206 self.start = current_start
1207 self.attach_assumption(lhs_value)
1208 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1209 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1210 self.attach_temp_declaration(n_expr,
1211 sym_result,
1212 rhs_value)
1213 self.start.add_edge_to(gn_end)
1215 # Join paths
1216 self.start = gn_end
1218 return sym_result, smt.Boolean_Literal(True)
1220 def tr_op_or(self, n_expr):
1221 assert isinstance(n_expr, Binary_Expression)
1222 assert n_expr.operator == Binary_Operator.LOGICAL_OR
1224 if self.functional: 1224 ↛ 1225line 1224 didn't jump to line 1225 because the condition on line 1224 was never true
1225 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1226 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1227 return self.create_return(n_expr,
1228 smt.Disjunction(lhs_value, rhs_value))
1230 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1231 # Emit VC for validity
1232 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1234 # Split into two paths.
1235 current_start = self.start
1236 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1237 self.new_temp_name())
1238 gn_end = graph.Node(self.graph)
1240 ### 1: LHS is true
1241 self.start = current_start
1242 self.attach_assumption(lhs_value)
1243 self.attach_temp_declaration(n_expr,
1244 sym_result,
1245 smt.Boolean_Literal(True))
1246 self.start.add_edge_to(gn_end)
1248 ### 2: LHS is not true
1249 self.start = current_start
1250 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1251 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1252 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1253 self.attach_temp_declaration(n_expr,
1254 sym_result,
1255 rhs_value)
1256 self.start.add_edge_to(gn_end)
1258 # Join paths
1259 self.start = gn_end
1261 return sym_result, smt.Boolean_Literal(True)
1263 def tr_core_equality_tuple_component(self, n_component, lhs, rhs):
1264 assert isinstance(n_component, Composite_Component)
1265 assert isinstance(lhs, smt.Expression)
1266 assert isinstance(rhs, smt.Expression)
1268 value_lhs = smt.Record_Access(lhs,
1269 n_component.name + ".value")
1270 value_rhs = smt.Record_Access(rhs,
1271 n_component.name + ".value")
1272 valid_equal = self.tr_core_equality(n_component.n_typ,
1273 value_lhs,
1274 value_rhs)
1276 if not n_component.optional:
1277 return valid_equal
1279 valid_lhs = smt.Record_Access(lhs,
1280 n_component.name + ".valid")
1281 valid_rhs = smt.Record_Access(rhs,
1282 n_component.name + ".valid")
1284 return smt.Conjunction(
1285 smt.Comparison("=", valid_lhs, valid_rhs),
1286 smt.Implication(valid_lhs, valid_equal))
1288 def tr_core_equality(self, n_typ, lhs, rhs):
1289 assert isinstance(n_typ, Type)
1290 assert isinstance(lhs, smt.Expression)
1291 assert isinstance(rhs, smt.Expression)
1293 if isinstance(n_typ, Tuple_Type):
1294 parts = []
1295 for n_component in n_typ.all_components():
1296 parts.append(
1297 self.tr_core_equality_tuple_component(n_component,
1298 lhs,
1299 rhs))
1301 if len(parts) == 0: 1301 ↛ 1302line 1301 didn't jump to line 1302 because the condition on line 1301 was never true
1302 return smt.Boolean_Literal(True)
1303 elif len(parts) == 1: 1303 ↛ 1304line 1303 didn't jump to line 1304 because the condition on line 1303 was never true
1304 return parts[0]
1305 else:
1306 result = smt.Conjunction(parts[0], parts[1])
1307 for part in parts[2:]:
1308 result = smt.Conjunction(result, part)
1309 return result
1311 else:
1312 return smt.Comparison("=", lhs, rhs)
1314 def tr_op_equality(self, n_expr):
1315 assert isinstance(n_expr, Binary_Expression)
1316 assert n_expr.operator in (Binary_Operator.COMP_EQ,
1317 Binary_Operator.COMP_NEQ)
1319 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1320 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1322 if lhs_value is None:
1323 comp_typ = n_expr.n_rhs.typ
1324 else:
1325 comp_typ = n_expr.n_lhs.typ
1327 if lhs_valid.is_static_true() and rhs_valid.is_static_true():
1328 # Simplified form, this is just x == y
1329 result = self.tr_core_equality(comp_typ,
1330 lhs_value,
1331 rhs_value)
1333 elif lhs_valid.is_static_false() and rhs_valid.is_static_false():
1334 # This is null == null, so true
1335 result = smt.Boolean_Literal(True)
1337 elif lhs_value is None: 1337 ↛ 1339line 1337 didn't jump to line 1339 because the condition on line 1337 was never true
1338 # This is null == <expr>, true iff rhs is null
1339 result = smt.Boolean_Negation(rhs_valid)
1341 elif rhs_value is None:
1342 # This is <expr> == null, true iff lhs is null
1343 result = smt.Boolean_Negation(lhs_valid)
1345 else:
1346 # This is <expr> == <expr> without shortcuts
1347 result = smt.Conjunction(
1348 smt.Comparison("=", lhs_valid, rhs_valid),
1349 smt.Implication(lhs_valid,
1350 self.tr_core_equality(comp_typ,
1351 lhs_value,
1352 rhs_value)))
1354 if n_expr.operator == Binary_Operator.COMP_NEQ:
1355 result = smt.Boolean_Negation(result)
1357 return self.create_return(n_expr, result)
1359 def tr_quantified_expression(self, n_expr):
1360 assert isinstance(n_expr, Quantified_Expression)
1362 # Nested quantifiers are not supported yet
1363 if self.functional: # pragma: no cover
1364 self.flag_unsupported(n_expr,
1365 "functional evaluation of quantifier")
1367 # TRLC quantifier
1368 # (forall x in arr_name => body)
1369 #
1370 # SMT quantifier
1371 # (forall ((i Int))
1372 # (=> (and (>= i 0) (< i (seq.len arr_name)))
1373 # (... (seq.nth arr_name i) ... )))
1374 #
1375 # There is an alternative which is:
1376 # (forall ((element ElementSort))
1377 # (=> (seq.contains arr_name (seq.unit element))
1378 # (... element ...)
1379 #
1380 # However it looks like for CVC5 at least this generates more
1381 # unknown and less unsat if a check depends on the explicit
1382 # value of some sequence member.
1384 # Evaluate subject first and creat a null check
1385 s_subject_value, s_subject_valid = \
1386 self.tr_name_reference(n_expr.n_source)
1387 self.attach_validity_check(s_subject_valid, n_expr.n_source)
1389 # Create validity checks for the body. We do this by creating
1390 # a new branch and eliminating the quantifier; pretending it's
1391 # a forall (since we want to show that for all evaluations
1392 # it's valid).
1393 current_start = self.start
1394 self.attach_empty_assumption()
1395 src_typ = n_expr.n_source.typ
1396 assert isinstance(src_typ, Array_Type)
1397 s_qe_index = smt.Constant(smt.BUILTIN_INTEGER,
1398 self.new_temp_name())
1399 self.start.add_statement(
1400 smt.Constant_Declaration(
1401 symbol = s_qe_index,
1402 comment = ("quantifier elimination (index) for %s at %s" %
1403 (n_expr.to_string(),
1404 n_expr.location.to_string()))))
1405 self.start.add_statement(
1406 smt.Assertion(smt.Comparison(">=",
1407 s_qe_index,
1408 smt.Integer_Literal(0))))
1409 self.start.add_statement(
1410 smt.Assertion(
1411 smt.Comparison("<",
1412 s_qe_index,
1413 smt.Sequence_Length(s_subject_value))))
1414 s_qe_sym = smt.Constant(self.tr_type(src_typ.element_type),
1415 self.new_temp_name())
1416 self.start.add_statement(
1417 smt.Constant_Declaration(
1418 symbol = s_qe_sym,
1419 value = smt.Sequence_Index(s_subject_value, s_qe_index),
1420 comment = ("quantifier elimination (symbol) for %s at %s" %
1421 (n_expr.to_string(),
1422 n_expr.location.to_string()))))
1423 self.qe_vars[n_expr.n_var] = s_qe_sym
1425 _, b_valid = self.tr_expression(n_expr.n_expr)
1426 self.attach_validity_check(b_valid, n_expr.n_expr)
1428 self.start = current_start
1429 del self.qe_vars[n_expr.n_var]
1431 # We have now shown that any path in the quantifier cannot
1432 # raise exception. Asserting the actual value of the
1433 # quantifier is more awkward.
1435 s_q_idx = smt.Bound_Variable(smt.BUILTIN_INTEGER,
1436 self.new_temp_name())
1437 s_q_sym = smt.Sequence_Index(s_subject_value, s_q_idx)
1438 self.bound_vars[n_expr.n_var] = s_q_sym
1440 temp, self.functional = self.functional, True
1441 b_value, _ = self.tr_expression(n_expr.n_expr)
1442 self.functional = temp
1444 bounds_expr = smt.Conjunction(
1445 smt.Comparison(">=",
1446 s_q_idx,
1447 smt.Integer_Literal(0)),
1448 smt.Comparison("<",
1449 s_q_idx,
1450 smt.Sequence_Length(s_subject_value)))
1451 if n_expr.universal:
1452 value = smt.Quantifier(
1453 "forall",
1454 [s_q_idx],
1455 smt.Implication(bounds_expr, b_value))
1456 else:
1457 value = smt.Quantifier(
1458 "exists",
1459 [s_q_idx],
1460 smt.Conjunction(bounds_expr, b_value))
1462 return value, smt.Boolean_Literal(True)
1464 def tr_field_access_expression(self, n_expr):
1465 assert isinstance(n_expr, Field_Access_Expression)
1467 prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix)
1468 self.attach_validity_check(prefix_valid, n_expr.n_prefix)
1470 field_value = smt.Record_Access(prefix_value,
1471 n_expr.n_field.name + ".value")
1472 if n_expr.n_field.optional:
1473 field_valid = smt.Record_Access(prefix_value,
1474 n_expr.n_field.name + ".valid")
1475 else:
1476 field_valid = smt.Boolean_Literal(True)
1478 return field_value, field_valid