Coverage for trlc/vcg.py: 97%
787 statements
« prev ^ index » next coverage.py v7.10.7, created at 2026-07-07 15:09 +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 VCG_AVAILABLE = True
33except ImportError: # pragma: no cover
34 VCG_AVAILABLE = False
36try:
37 from pyvcg.driver.cvc5_api import CVC5_Solver
38 CVC5_API_AVAILABLE = True
39except ImportError: # pragma: no cover
40 CVC5_API_AVAILABLE = False
42CVC5_OPTIONS = {
43 "tlimit-per" : 2500,
44 "seed" : 42,
45 "sat-random-seed" : 42,
46}
49class Unsupported(Exception): # pragma: no cover
50 # lobster-exclude: Not safety relevant
51 def __init__(self, node, text):
52 assert isinstance(node, Node)
53 assert isinstance(text, str) or text is None
54 super().__init__()
55 self.message = "%s not yet supported in VCG" % \
56 (text if text else node.__class__.__name__)
57 self.location = node.location
60class Feedback:
61 # lobster-exclude: Not safety relevant
62 def __init__(self, node, message, kind, expect_unsat=True):
63 assert isinstance(node, Expression)
64 assert isinstance(message, str)
65 assert isinstance(kind, str)
66 assert isinstance(expect_unsat, bool)
67 self.node = node
68 self.message = message
69 self.kind = "vcg-" + kind
70 self.expect_unsat = expect_unsat
73class VCG:
74 # lobster-exclude: Not safety relevant
75 def __init__(self, mh, n_ctyp, debug):
76 assert VCG_AVAILABLE
77 assert isinstance(mh, Message_Handler)
78 assert isinstance(n_ctyp, Composite_Type)
79 assert isinstance(debug, bool)
81 self.mh = mh
82 self.n_ctyp = n_ctyp
83 self.debug = debug
85 self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name,
86 n_ctyp.name)
88 self.tmp_id = 0
90 self.vcg = vcg.VCG()
91 self.graph = self.vcg.graph
92 self.start = self.vcg.start
93 # Current start node, we will update this as we go along.
94 self.preamble = None
95 # We do remember the first node where we put all our
96 # declarations, in case we need to add some more later.
98 self.constants = {}
99 self.enumerations = {}
100 self.tuples = {}
101 self.records = {}
102 self.arrays = {}
103 self.bound_vars = {}
104 self.qe_vars = {}
105 self.tuple_base = {}
106 self.uf_records = {}
108 self.uf_matches = None
109 # Pointer to the UF we use for matches. We only generate it
110 # when we must, as it may affect the logics selected due to
111 # string theory being used.
113 self.functional = False
114 # If set to true, then we ignore validity checks and do not
115 # create intermediates. We just build the value and validity
116 # expresions and return them.
118 self.emit_checks = True
119 # If set to false, we skip creating checks.
121 @staticmethod
122 def flag_unsupported(node, text=None): # pragma: no cover
123 assert isinstance(node, Node)
124 raise Unsupported(node, text)
126 def new_temp_name(self):
127 self.tmp_id += 1
128 return "tmp.%u" % self.tmp_id
130 def get_uf_matches(self):
131 if self.uf_matches is None:
132 self.uf_matches = \
133 smt.Function("trlc.matches",
134 smt.BUILTIN_BOOLEAN,
135 smt.Bound_Variable(smt.BUILTIN_STRING,
136 "subject"),
137 smt.Bound_Variable(smt.BUILTIN_STRING,
138 "regex"))
140 # Create UF for the matches function (for now, later we
141 # will deal with regex properly).
142 self.preamble.add_statement(
143 smt.Function_Declaration(self.uf_matches))
145 return self.uf_matches
147 def create_return(self, node, s_value, s_valid=None):
148 assert isinstance(node, Expression)
149 assert isinstance(s_value, smt.Expression)
150 assert isinstance(s_valid, smt.Expression) or s_valid is None
152 if s_valid is None: 152 ↛ 155line 152 didn't jump to line 155 because the condition on line 152 was always true
153 s_valid = smt.Boolean_Literal(True)
155 if self.functional:
156 return s_value, s_valid
158 else:
159 sym_result = smt.Constant(s_value.sort,
160 self.new_temp_name())
161 self.attach_temp_declaration(node, sym_result, s_value)
163 return sym_result, s_valid
165 def attach_validity_check(self, bool_expr, origin):
166 assert isinstance(bool_expr, smt.Expression)
167 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
168 assert isinstance(origin, Expression)
169 assert not self.functional
171 if not self.emit_checks:
172 return
174 # Attach new graph node advance start
175 if not bool_expr.is_static_true():
176 gn_check = graph.Check(self.graph)
177 gn_check.add_goal(bool_expr,
178 Feedback(origin,
179 "expression could be null",
180 "evaluation-of-null"),
181 "validity check for %s" % origin.to_string())
182 self.start.add_edge_to(gn_check)
183 self.start = gn_check
185 def attach_int_division_check(self, int_expr, origin):
186 assert isinstance(int_expr, smt.Expression)
187 assert int_expr.sort is smt.BUILTIN_INTEGER
188 assert isinstance(origin, Expression)
189 assert not self.functional
191 if not self.emit_checks: 191 ↛ 192line 191 didn't jump to line 192 because the condition on line 191 was never true
192 return
194 # Attach new graph node advance start
195 gn_check = graph.Check(self.graph)
196 gn_check.add_goal(
197 smt.Boolean_Negation(
198 smt.Comparison("=", int_expr, smt.Integer_Literal(0))),
199 Feedback(origin,
200 "divisor could be 0",
201 "div-by-zero"),
202 "division by zero check for %s" % origin.to_string())
203 self.start.add_edge_to(gn_check)
204 self.start = gn_check
206 def attach_real_division_check(self, real_expr, origin):
207 assert isinstance(real_expr, smt.Expression)
208 assert real_expr.sort is smt.BUILTIN_REAL
209 assert isinstance(origin, Expression)
210 assert not self.functional
212 if not self.emit_checks: 212 ↛ 213line 212 didn't jump to line 213 because the condition on line 212 was never true
213 return
215 # Attach new graph node advance start
216 gn_check = graph.Check(self.graph)
217 gn_check.add_goal(
218 smt.Boolean_Negation(
219 smt.Comparison("=", real_expr, smt.Real_Literal(0))),
220 Feedback(origin,
221 "divisor could be 0.0",
222 "div-by-zero"),
223 "division by zero check for %s" % origin.to_string())
224 self.start.add_edge_to(gn_check)
225 self.start = gn_check
227 def attach_index_check(self, seq_expr, index_expr, origin):
228 assert isinstance(seq_expr, smt.Expression)
229 assert isinstance(seq_expr.sort, smt.Sequence_Sort)
230 assert isinstance(index_expr, smt.Expression)
231 assert index_expr.sort is smt.BUILTIN_INTEGER
232 assert isinstance(origin, Binary_Expression)
233 assert origin.operator == Binary_Operator.INDEX
234 assert not self.functional
236 if not self.emit_checks: 236 ↛ 237line 236 didn't jump to line 237 because the condition on line 236 was never true
237 return
239 # Attach new graph node advance start
240 gn_check = graph.Check(self.graph)
241 gn_check.add_goal(
242 smt.Comparison(">=", index_expr, smt.Integer_Literal(0)),
243 Feedback(origin,
244 "array index could be less than 0",
245 "array-index"),
246 "index lower bound check for %s" % origin.to_string())
247 gn_check.add_goal(
248 smt.Comparison("<",
249 index_expr,
250 smt.Sequence_Length(seq_expr)),
251 Feedback(origin,
252 "array index could be larger than len(%s)" %
253 origin.n_lhs.to_string(),
254 "array-index"),
255 "index lower bound check for %s" % origin.to_string())
257 self.start.add_edge_to(gn_check)
258 self.start = gn_check
260 def attach_feasability_check(self, bool_expr, origin):
261 assert isinstance(bool_expr, smt.Expression)
262 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
263 assert isinstance(origin, Expression)
264 assert not self.functional
266 if not self.emit_checks:
267 return
269 # Attach new graph node advance start
270 gn_check = graph.Check(self.graph)
271 gn_check.add_goal(bool_expr,
272 Feedback(origin,
273 "expression is always true",
274 "always-true",
275 expect_unsat = False),
276 "feasability check for %s" % origin.to_string())
277 self.start.add_edge_to(gn_check)
279 def attach_assumption(self, bool_expr):
280 assert isinstance(bool_expr, smt.Expression)
281 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
282 assert not self.functional
284 # Attach new graph node advance start
285 gn_ass = graph.Assumption(self.graph)
286 gn_ass.add_statement(smt.Assertion(bool_expr))
287 self.start.add_edge_to(gn_ass)
288 self.start = gn_ass
290 def attach_temp_declaration(self, node, sym, value=None):
291 assert isinstance(node, (Expression, Action))
292 assert isinstance(sym, smt.Constant)
293 assert isinstance(value, smt.Expression) or value is None
294 assert not self.functional
296 # Attach new graph node advance start
297 gn_decl = graph.Assumption(self.graph)
298 gn_decl.add_statement(
299 smt.Constant_Declaration(
300 symbol = sym,
301 value = value,
302 comment = "result of %s at %s" % (node.to_string(),
303 node.location.to_string()),
304 relevant = False))
305 self.start.add_edge_to(gn_decl)
306 self.start = gn_decl
308 def attach_empty_assumption(self):
309 assert not self.functional
311 # Attach new graph node advance start
312 gn_decl = graph.Assumption(self.graph)
313 self.start.add_edge_to(gn_decl)
314 self.start = gn_decl
316 def analyze(self):
317 try:
318 self.checks_on_composite_type(self.n_ctyp)
319 except Unsupported as exc: # pragma: no cover
320 self.mh.warning(exc.location,
321 exc.message)
323 def checks_on_composite_type(self, n_ctyp):
324 assert isinstance(n_ctyp, Composite_Type)
326 # Create node for global declarations
327 gn_locals = graph.Assumption(self.graph)
328 self.start.add_edge_to(gn_locals)
329 self.start = gn_locals
330 self.preamble = gn_locals
332 # Create local variables
333 for n_component in n_ctyp.all_components():
334 self.tr_component_decl(n_component, self.start)
336 # Create paths for checks in two phases:
337 # Phase A ("at declaration"): checks that do not follow any
338 # record or union reference via field access. These are fully
339 # self-contained and are analyzed first.
340 # Phase B ("after references"): checks that dereference at
341 # least one record or union reference. They run after Phase A
342 # so that knowledge accumulated from Phase A fatal checks is
343 # available.
344 for phase in (False, True):
345 for n_check in n_ctyp.iter_checks():
346 if n_check.uses_field_access != phase:
347 continue
348 current_start = self.start
349 self.tr_check(n_check)
351 # Only fatal checks contribute to the total knowledge
352 if n_check.severity != "fatal":
353 self.start = current_start
355 # Emit debug graph
356 if self.debug: # pragma: no cover
357 subprocess.run(["dot", "-Tpdf", "-o%s.pdf" % self.vc_name],
358 input = self.graph.debug_render_dot(),
359 check = True,
360 encoding = "UTF-8")
362 # Generate VCs
363 self.vcg.generate()
365 # Solve VCs and provide feedback
366 nok_feasibility_checks = []
367 ok_feasibility_checks = set()
368 nok_validity_checks = set()
370 for vc_id, vc in enumerate(self.vcg.vcs):
371 if self.debug: # pramga: no cover 371 ↛ 372line 371 didn't jump to line 372 because the condition on line 371 was never true
372 with open(self.vc_name + "_%04u.smt2" % vc_id, "w",
373 encoding="UTF-8") as fd:
374 fd.write(vc["script"].generate_vc(SMTLIB_Generator()))
376 # Checks that have already failed don't need to be checked
377 # again on a different path
378 if vc["feedback"].expect_unsat and \
379 vc["feedback"] in nok_validity_checks:
380 continue
382 solver = CVC5_Solver()
383 for name, value in CVC5_OPTIONS.items():
384 solver.set_solver_option(name, value)
386 status, values = vc["script"].solve_vc(solver)
388 message = vc["feedback"].message
389 if self.debug: # pragma: no cover
390 message += " [vc_id = %u]" % vc_id
392 if vc["feedback"].expect_unsat:
393 if status != "unsat":
394 self.mh.check(vc["feedback"].node.location,
395 message,
396 vc["feedback"].kind,
397 self.create_counterexample(status,
398 values))
399 nok_validity_checks.add(vc["feedback"])
400 else:
401 if status == "unsat":
402 nok_feasibility_checks.append(vc["feedback"])
403 else:
404 ok_feasibility_checks.add(vc["feedback"])
406 # This is a bit wonky, but this way we make sure the ording is
407 # consistent
408 for feedback in nok_feasibility_checks:
409 if feedback not in ok_feasibility_checks:
410 self.mh.check(feedback.node.location,
411 feedback.message,
412 feedback.kind)
413 ok_feasibility_checks.add(feedback)
415 def create_counterexample(self, status, values):
416 rv = [
417 "example %s triggering error:" %
418 self.n_ctyp.__class__.__name__.lower(),
419 " %s bad_potato {" % self.n_ctyp.name
420 ]
422 for n_component in self.n_ctyp.all_components():
423 id_value = self.tr_component_value_name(n_component)
424 id_valid = self.tr_component_valid_name(n_component)
425 if status == "unknown" and (id_value not in values or 425 ↛ 427line 425 didn't jump to line 427 because the condition on line 425 was never true
426 id_valid not in values):
427 rv.append(" %s = ???" % n_component.name)
428 elif values.get(id_valid):
429 rv.append(" %s = %s" %
430 (n_component.name,
431 self.value_to_trlc(n_component.n_typ,
432 values[id_value])))
433 else:
434 rv.append(" /* %s is null */" % n_component.name)
436 rv.append(" }")
437 if status == "unknown":
438 rv.append("/* note: counter-example is unreliable in this case */")
439 return "\n".join(rv)
441 def fraction_to_decimal_string(self, num, den):
442 assert isinstance(num, int)
443 assert isinstance(den, int) and den >= 1
445 tmp = den
446 if tmp > 2:
447 while tmp > 1:
448 if tmp % 2 == 0:
449 tmp = tmp // 2
450 elif tmp % 5 == 0:
451 tmp = tmp // 5
452 else:
453 return "%i / %u" % (num, den)
455 rv = str(abs(num) // den)
457 i = abs(num) % den
458 j = den
460 if i > 0:
461 rv += "."
462 while i > 0:
463 i *= 10
464 rv += str(i // j)
465 i = i % j
466 else:
467 rv += ".0"
469 if num < 0:
470 return "-" + rv
471 else:
472 return rv
474 def value_to_trlc(self, n_typ, value):
475 assert isinstance(n_typ, Type)
477 if isinstance(n_typ, Builtin_Integer):
478 return str(value)
480 elif isinstance(n_typ, Builtin_Decimal):
481 if isinstance(value, Fraction):
482 num, den = value.as_integer_ratio()
483 if den >= 1: 483 ↛ 486line 483 didn't jump to line 486 because the condition on line 483 was always true
484 return self.fraction_to_decimal_string(num, den)
485 else:
486 return self.fraction_to_decimal_string(-num, -den)
487 else:
488 return "/* unable to generate precise value */"
490 elif isinstance(n_typ, Builtin_Boolean):
491 return "true" if value else "false"
493 elif isinstance(n_typ, Enumeration_Type):
494 return n_typ.name + "." + value
496 elif isinstance(n_typ, Builtin_String):
497 if "\n" in value:
498 return "'''%s'''" % value
499 else:
500 return '"%s"' % value
502 elif isinstance(n_typ, (Record_Type, Union_Type)):
503 # lobster-trace: LRM.Union_Type_Equality
504 if value < 0:
505 instance_id = value * -2 - 1
506 else:
507 instance_id = value * 2
508 if isinstance(n_typ, Record_Type): 508 ↛ 516line 508 didn't jump to line 516 because the condition on line 508 was always true
509 if n_typ.n_package is self.n_ctyp.n_package:
510 return "%s_instance_%i" % (n_typ.name, instance_id)
511 else:
512 return "%s.%s_instance_%i" % (n_typ.n_package.name,
513 n_typ.name,
514 instance_id)
515 else:
516 return "instance_%i" % instance_id
518 elif isinstance(n_typ, Tuple_Type):
519 parts = []
520 for n_item in n_typ.iter_sequence():
521 if isinstance(n_item, Composite_Component):
522 if n_item.optional and not value[n_item.name + ".valid"]:
523 parts.pop()
524 break
525 parts.append(
526 self.value_to_trlc(n_item.n_typ,
527 value[n_item.name + ".value"]))
529 else:
530 assert isinstance(n_item, Separator)
531 sep_text = {
532 "AT" : "@",
533 "COLON" : ":",
534 "SEMICOLON" : ";"
535 }.get(n_item.token.kind, n_item.token.value)
536 parts.append(sep_text)
538 if n_typ.has_separators():
539 return "".join(parts)
540 else:
541 return "(%s)" % ", ".join(parts)
543 elif isinstance(n_typ, Array_Type):
544 return "[%s]" % ", ".join(self.value_to_trlc(n_typ.element_type,
545 item)
546 for item in value)
548 else: # pragma: no cover
549 self.flag_unsupported(n_typ,
550 "back-conversion from %s" % n_typ.name)
552 def tr_component_value_name(self, n_component):
553 return n_component.member_of.fully_qualified_name() + \
554 "." + n_component.name + ".value"
556 def tr_component_valid_name(self, n_component):
557 return n_component.member_of.fully_qualified_name() + \
558 "." + n_component.name + ".valid"
560 def emit_tuple_constraints(self, n_tuple, s_sym):
561 assert isinstance(n_tuple, Tuple_Type)
562 assert isinstance(s_sym, smt.Constant)
564 old_functional, self.functional = self.functional, True
565 self.tuple_base[n_tuple] = s_sym
567 constraints = []
569 # The first tuple constraint is that all checks must have
570 # passed, otherwise the tool would just error. An error in a
571 # tuple is pretty much the same as a fatal in the enclosing
572 # record.
574 for n_check in n_tuple.iter_checks():
575 if n_check.severity == "warning":
576 continue
577 # We do consider both fatal and errors to be sources of
578 # truth here.
579 c_value, _ = self.tr_expression(n_check.n_expr)
580 constraints.append(c_value)
582 # The secopnd tuple constraint is that once you get a null
583 # field, all following fields must also be null.
585 components = n_tuple.all_components()
586 for i, component in enumerate(components):
587 if component.optional:
588 condition = smt.Boolean_Negation(
589 smt.Record_Access(s_sym,
590 component.name + ".valid"))
591 consequences = [
592 smt.Boolean_Negation(
593 smt.Record_Access(s_sym,
594 c.name + ".valid"))
595 for c in components[i + 1:]
596 ]
597 if len(consequences) == 0:
598 break
599 elif len(consequences) == 1: 599 ↛ 602line 599 didn't jump to line 602 because the condition on line 599 was always true
600 consequence = consequences[0]
601 else:
602 consequence = smt.Conjunction(*consequences)
603 constraints.append(smt.Implication(condition, consequence))
605 del self.tuple_base[n_tuple]
606 self.functional = old_functional
608 for cons in constraints:
609 self.start.add_statement(smt.Assertion(cons))
611 def tr_component_decl(self, n_component, gn_locals):
612 assert isinstance(n_component, Composite_Component)
613 assert isinstance(gn_locals, graph.Assumption)
615 if isinstance(self.n_ctyp, Record_Type):
616 frozen = self.n_ctyp.is_frozen(n_component)
617 else:
618 frozen = False
620 id_value = self.tr_component_value_name(n_component)
621 s_sort = self.tr_type(n_component.n_typ)
622 s_sym = smt.Constant(s_sort, id_value)
623 if frozen:
624 old_functional, self.functional = self.functional, True
625 s_val, _ = self.tr_expression(
626 self.n_ctyp.get_freezing_expression(n_component))
627 self.functional = old_functional
628 else:
629 s_val = None
630 s_decl = smt.Constant_Declaration(
631 symbol = s_sym,
632 value = s_val,
633 comment = "value for %s declared on %s" % (
634 n_component.name,
635 n_component.location.to_string()),
636 relevant = True)
637 gn_locals.add_statement(s_decl)
638 self.constants[id_value] = s_sym
640 if isinstance(n_component.n_typ, Tuple_Type):
641 self.emit_tuple_constraints(n_component.n_typ, s_sym)
643 # For arrays we need to add additional constraints for the
644 # length
645 if isinstance(n_component.n_typ, Array_Type):
646 if n_component.n_typ.lower_bound > 0:
647 s_lower = smt.Integer_Literal(n_component.n_typ.lower_bound)
648 gn_locals.add_statement(
649 smt.Assertion(
650 smt.Comparison(">=",
651 smt.Sequence_Length(s_sym),
652 s_lower)))
654 if n_component.n_typ.upper_bound is not None:
655 s_upper = smt.Integer_Literal(n_component.n_typ.upper_bound)
656 gn_locals.add_statement(
657 smt.Assertion(
658 smt.Comparison("<=",
659 smt.Sequence_Length(s_sym),
660 s_upper)))
662 id_valid = self.tr_component_valid_name(n_component)
663 s_sym = smt.Constant(smt.BUILTIN_BOOLEAN, id_valid)
664 s_val = (None
665 if n_component.optional and not frozen
666 else smt.Boolean_Literal(True))
667 s_decl = smt.Constant_Declaration(
668 symbol = s_sym,
669 value = s_val,
670 relevant = True)
671 gn_locals.add_statement(s_decl)
672 self.constants[id_valid] = s_sym
674 def tr_type(self, n_type):
675 assert isinstance(n_type, Type)
677 if isinstance(n_type, Builtin_Boolean):
678 return smt.BUILTIN_BOOLEAN
680 elif isinstance(n_type, Builtin_Integer):
681 return smt.BUILTIN_INTEGER
683 elif isinstance(n_type, Builtin_Decimal):
684 return smt.BUILTIN_REAL
686 elif isinstance(n_type, Builtin_String):
687 return smt.BUILTIN_STRING
689 elif isinstance(n_type, Enumeration_Type):
690 if n_type not in self.enumerations:
691 s_sort = smt.Enumeration(n_type.n_package.name +
692 "." + n_type.name)
693 for n_lit in n_type.literals.values():
694 s_sort.add_literal(n_lit.name)
695 self.enumerations[n_type] = s_sort
696 self.start.add_statement(
697 smt.Enumeration_Declaration(
698 s_sort,
699 "enumeration %s from %s" % (
700 n_type.name,
701 n_type.location.to_string())))
702 return self.enumerations[n_type]
704 elif isinstance(n_type, Tuple_Type):
705 if n_type not in self.tuples:
706 s_sort = smt.Record(n_type.n_package.name +
707 "." + n_type.name)
708 for n_component in n_type.all_components():
709 s_sort.add_component(n_component.name + ".value",
710 self.tr_type(n_component.n_typ))
711 if n_component.optional:
712 s_sort.add_component(n_component.name + ".valid",
713 smt.BUILTIN_BOOLEAN)
714 self.tuples[n_type] = s_sort
715 self.start.add_statement(
716 smt.Record_Declaration(
717 s_sort,
718 "tuple %s from %s" % (
719 n_type.name,
720 n_type.location.to_string())))
722 return self.tuples[n_type]
724 elif isinstance(n_type, Array_Type):
725 if n_type not in self.arrays:
726 s_element_sort = self.tr_type(n_type.element_type)
727 s_sequence = smt.Sequence_Sort(s_element_sort)
728 self.arrays[n_type] = s_sequence
730 return self.arrays[n_type]
732 elif isinstance(n_type, (Record_Type, Union_Type)):
733 # lobster-trace: LRM.union_type
734 # Record and union references are modelled as a free
735 # integer. If we access their field then we use an
736 # uninterpreted function. Some of these have special
737 # meaning:
738 # 0 - the null reference
739 # 1 - the self reference
740 # anything else - uninterpreted
741 return smt.BUILTIN_INTEGER
743 else: # pragma: no cover
744 self.flag_unsupported(n_type)
746 def tr_check(self, n_check):
747 assert isinstance(n_check, Check)
749 # If the check belongs to a different type then we are looking
750 # at a type extension. In this case we do not create checks
751 # again, because if a check would fail it would already have
752 # failed.
753 if n_check.n_type is not self.n_ctyp:
754 old_emit, self.emit_checks = self.emit_checks, False
756 value, valid = self.tr_expression(n_check.n_expr)
757 self.attach_validity_check(valid, n_check.n_expr)
758 self.attach_feasability_check(value, n_check.n_expr)
759 self.attach_assumption(value)
761 if n_check.n_type is not self.n_ctyp:
762 self.emit_checks = old_emit
764 def tr_expression(self, n_expr):
765 value = None
767 if isinstance(n_expr, Name_Reference):
768 return self.tr_name_reference(n_expr)
770 elif isinstance(n_expr, Unary_Expression):
771 return self.tr_unary_expression(n_expr)
773 elif isinstance(n_expr, Binary_Expression):
774 return self.tr_binary_expression(n_expr)
776 elif isinstance(n_expr, Range_Test):
777 return self.tr_range_test(n_expr)
779 elif isinstance(n_expr, OneOf_Expression):
780 return self.tr_oneof_test(n_expr)
782 elif isinstance(n_expr, Conditional_Expression):
783 if self.functional:
784 return self.tr_conditional_expression_functional(n_expr)
785 else:
786 return self.tr_conditional_expression(n_expr)
788 elif isinstance(n_expr, Null_Literal):
789 return None, smt.Boolean_Literal(False)
791 elif isinstance(n_expr, Boolean_Literal):
792 value = smt.Boolean_Literal(n_expr.value)
794 elif isinstance(n_expr, Integer_Literal):
795 value = smt.Integer_Literal(n_expr.value)
797 elif isinstance(n_expr, Decimal_Literal):
798 value = smt.Real_Literal(n_expr.value)
800 elif isinstance(n_expr, Enumeration_Literal):
801 value = smt.Enumeration_Literal(self.tr_type(n_expr.typ),
802 n_expr.value.name)
804 elif isinstance(n_expr, String_Literal):
805 value = smt.String_Literal(n_expr.value)
807 elif isinstance(n_expr, Quantified_Expression):
808 return self.tr_quantified_expression(n_expr)
810 elif isinstance(n_expr, Field_Access_Expression):
811 return self.tr_field_access_expression(n_expr)
813 else: # pragma: no cover
814 self.flag_unsupported(n_expr)
816 return value, smt.Boolean_Literal(True)
818 def tr_name_reference(self, n_ref):
819 assert isinstance(n_ref, Name_Reference)
821 if isinstance(n_ref.entity, Composite_Component):
822 if n_ref.entity.member_of in self.tuple_base:
823 sym = self.tuple_base[n_ref.entity.member_of]
824 if n_ref.entity.optional:
825 s_valid = smt.Record_Access(sym,
826 n_ref.entity.name + ".valid")
827 else:
828 s_valid = smt.Boolean_Literal(True)
829 s_value = smt.Record_Access(sym,
830 n_ref.entity.name + ".value")
831 return s_value, s_valid
833 else:
834 id_value = self.tr_component_value_name(n_ref.entity)
835 id_valid = self.tr_component_valid_name(n_ref.entity)
836 return self.constants[id_value], self.constants[id_valid]
838 else:
839 assert isinstance(n_ref.entity, Quantified_Variable)
840 if n_ref.entity in self.qe_vars:
841 return self.qe_vars[n_ref.entity], smt.Boolean_Literal(True)
842 else:
843 return self.bound_vars[n_ref.entity], smt.Boolean_Literal(True)
845 def tr_unary_expression(self, n_expr):
846 assert isinstance(n_expr, Unary_Expression)
848 operand_value, operand_valid = self.tr_expression(n_expr.n_operand)
849 if not self.functional:
850 self.attach_validity_check(operand_valid, n_expr.n_operand)
852 sym_value = None
854 if n_expr.operator == Unary_Operator.MINUS:
855 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
856 sym_value = smt.Unary_Int_Arithmetic_Op("-",
857 operand_value)
858 else:
859 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
860 sym_value = smt.Unary_Real_Arithmetic_Op("-",
861 operand_value)
863 elif n_expr.operator == Unary_Operator.PLUS:
864 sym_value = operand_value
866 elif n_expr.operator == Unary_Operator.LOGICAL_NOT:
867 sym_value = smt.Boolean_Negation(operand_value)
869 elif n_expr.operator == Unary_Operator.ABSOLUTE_VALUE:
870 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
871 sym_value = smt.Unary_Int_Arithmetic_Op("abs",
872 operand_value)
874 else:
875 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
876 sym_value = smt.Unary_Real_Arithmetic_Op("abs",
877 operand_value)
879 elif n_expr.operator == Unary_Operator.STRING_LENGTH:
880 sym_value = smt.String_Length(operand_value)
882 elif n_expr.operator == Unary_Operator.ARRAY_LENGTH:
883 sym_value = smt.Sequence_Length(operand_value)
885 elif n_expr.operator == Unary_Operator.CONVERSION_TO_DECIMAL:
886 sym_value = smt.Conversion_To_Real(operand_value)
888 elif n_expr.operator == Unary_Operator.CONVERSION_TO_INT:
889 sym_value = smt.Conversion_To_Integer("rna", operand_value)
891 else:
892 self.mh.ice_loc(n_expr,
893 "unexpected unary operator %s" %
894 n_expr.operator.name)
896 return self.create_return(n_expr, sym_value)
898 def tr_binary_expression(self, n_expr):
899 assert isinstance(n_expr, Binary_Expression)
901 # Some operators deal with validity in a different way. We
902 # deal with them first and then exit.
903 if n_expr.operator in (Binary_Operator.COMP_EQ,
904 Binary_Operator.COMP_NEQ):
905 return self.tr_op_equality(n_expr)
907 elif n_expr.operator == Binary_Operator.LOGICAL_IMPLIES:
908 return self.tr_op_implication(n_expr)
910 elif n_expr.operator == Binary_Operator.LOGICAL_AND:
911 return self.tr_op_and(n_expr)
913 elif n_expr.operator == Binary_Operator.LOGICAL_OR:
914 return self.tr_op_or(n_expr)
916 # The remaining operators always check for validity, so we can
917 # obtain the values of both sides now.
918 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
919 if not self.functional:
920 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
921 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
922 if not self.functional:
923 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
924 sym_value = None
926 if n_expr.operator == Binary_Operator.LOGICAL_XOR:
927 sym_value = smt.Exclusive_Disjunction(lhs_value, rhs_value)
929 elif n_expr.operator in (Binary_Operator.PLUS,
930 Binary_Operator.MINUS,
931 Binary_Operator.TIMES,
932 Binary_Operator.DIVIDE,
933 Binary_Operator.REMAINDER):
935 if isinstance(n_expr.n_lhs.typ, Builtin_String):
936 assert n_expr.operator == Binary_Operator.PLUS
937 sym_value = smt.String_Concatenation(lhs_value, rhs_value)
939 elif isinstance(n_expr.n_lhs.typ, Builtin_Integer):
940 if n_expr.operator in (Binary_Operator.DIVIDE,
941 Binary_Operator.REMAINDER):
942 self.attach_int_division_check(rhs_value, n_expr)
944 smt_op = {
945 Binary_Operator.PLUS : "+",
946 Binary_Operator.MINUS : "-",
947 Binary_Operator.TIMES : "*",
948 Binary_Operator.DIVIDE : "floor_div",
949 Binary_Operator.REMAINDER : "ada_remainder",
950 }[n_expr.operator]
952 sym_value = smt.Binary_Int_Arithmetic_Op(smt_op,
953 lhs_value,
954 rhs_value)
956 else:
957 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
958 if n_expr.operator == Binary_Operator.DIVIDE:
959 self.attach_real_division_check(rhs_value, n_expr)
961 smt_op = {
962 Binary_Operator.PLUS : "+",
963 Binary_Operator.MINUS : "-",
964 Binary_Operator.TIMES : "*",
965 Binary_Operator.DIVIDE : "/",
966 }[n_expr.operator]
968 sym_value = smt.Binary_Real_Arithmetic_Op(smt_op,
969 lhs_value,
970 rhs_value)
972 elif n_expr.operator in (Binary_Operator.COMP_LT,
973 Binary_Operator.COMP_LEQ,
974 Binary_Operator.COMP_GT,
975 Binary_Operator.COMP_GEQ):
976 smt_op = {
977 Binary_Operator.COMP_LT : "<",
978 Binary_Operator.COMP_LEQ : "<=",
979 Binary_Operator.COMP_GT : ">",
980 Binary_Operator.COMP_GEQ : ">=",
981 }[n_expr.operator]
983 sym_value = smt.Comparison(smt_op, lhs_value, rhs_value)
985 elif n_expr.operator in (Binary_Operator.STRING_CONTAINS,
986 Binary_Operator.STRING_STARTSWITH,
987 Binary_Operator.STRING_ENDSWITH):
989 smt_op = {
990 Binary_Operator.STRING_CONTAINS : "contains",
991 Binary_Operator.STRING_STARTSWITH : "prefixof",
992 Binary_Operator.STRING_ENDSWITH : "suffixof"
993 }
995 # LHS / RHS ordering is not a mistake, in SMTLIB it's the
996 # other way around than in TRLC.
997 sym_value = smt.String_Predicate(smt_op[n_expr.operator],
998 rhs_value,
999 lhs_value)
1001 elif n_expr.operator == Binary_Operator.STRING_REGEX:
1002 rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None, None).value
1003 assert isinstance(rhs_evaluation, str)
1005 sym_value = smt.Function_Application(
1006 self.get_uf_matches(),
1007 lhs_value,
1008 smt.String_Literal(rhs_evaluation))
1010 elif n_expr.operator == Binary_Operator.INDEX:
1011 self.attach_index_check(lhs_value, rhs_value, n_expr)
1012 sym_value = smt.Sequence_Index(lhs_value, rhs_value)
1014 elif n_expr.operator == Binary_Operator.ARRAY_CONTAINS:
1015 sym_value = smt.Sequence_Contains(rhs_value, lhs_value)
1017 elif n_expr.operator == Binary_Operator.POWER:
1018 # LRM says that the exponent is always static and an
1019 # integer
1020 static_value = n_expr.n_rhs.evaluate(self.mh, None, None).value
1021 assert isinstance(static_value, int) and static_value >= 0
1023 if static_value == 0: 1023 ↛ 1024line 1023 didn't jump to line 1024 because the condition on line 1023 was never true
1024 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1025 sym_value = smt.Integer_Literal(1)
1026 else:
1027 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1028 sym_value = smt.Real_Literal(1)
1030 else:
1031 sym_value = lhs_value
1032 for _ in range(1, static_value):
1033 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1034 sym_value = smt.Binary_Int_Arithmetic_Op("*",
1035 sym_value,
1036 lhs_value)
1037 else:
1038 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1039 sym_value = smt.Binary_Real_Arithmetic_Op("*",
1040 sym_value,
1041 lhs_value)
1043 else: # pragma: no cover
1044 self.flag_unsupported(n_expr, n_expr.operator.name)
1046 return self.create_return(n_expr, sym_value)
1048 def tr_range_test(self, n_expr):
1049 assert isinstance(n_expr, Range_Test)
1051 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1052 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1053 lower_value, lower_valid = self.tr_expression(n_expr.n_lower)
1054 self.attach_validity_check(lower_valid, n_expr.n_lower)
1055 upper_value, upper_valid = self.tr_expression(n_expr.n_upper)
1056 self.attach_validity_check(upper_valid, n_expr.n_upper)
1058 sym_value = smt.Conjunction(
1059 smt.Comparison(">=", lhs_value, lower_value),
1060 smt.Comparison("<=", lhs_value, upper_value))
1062 return self.create_return(n_expr, sym_value)
1064 def tr_oneof_test(self, n_expr):
1065 assert isinstance(n_expr, OneOf_Expression)
1067 choices = []
1068 for n_choice in n_expr.choices:
1069 c_value, c_valid = self.tr_expression(n_choice)
1070 self.attach_validity_check(c_valid, n_choice)
1071 choices.append(c_value)
1073 negated_choices = [smt.Boolean_Negation(c)
1074 for c in choices]
1076 # pylint: disable=consider-using-enumerate
1078 if len(choices) == 1:
1079 result = choices[0]
1080 elif len(choices) == 2:
1081 result = smt.Exclusive_Disjunction(choices[0], choices[1])
1082 else:
1083 assert len(choices) >= 3
1084 values = []
1085 for choice_id in range(len(choices)):
1086 sequence = []
1087 for other_id in range(len(choices)):
1088 if other_id == choice_id:
1089 sequence.append(choices[other_id])
1090 else:
1091 sequence.append(negated_choices[other_id])
1092 values.append(smt.Conjunction(*sequence))
1093 result = smt.Disjunction(*values)
1095 return self.create_return(n_expr, result)
1097 def tr_conditional_expression_functional(self, n_expr):
1098 assert isinstance(n_expr, Conditional_Expression)
1100 s_result, _ = self.tr_expression(n_expr.else_expr)
1101 for n_action in reversed(n_expr.actions):
1102 s_condition, _ = self.tr_expression(n_action.n_cond)
1103 s_true, _ = self.tr_expression(n_action.n_expr)
1104 s_result = smt.Conditional(s_condition, s_true, s_result)
1106 return self.create_return(n_expr, s_result)
1108 def tr_conditional_expression(self, n_expr):
1109 assert isinstance(n_expr, Conditional_Expression)
1110 assert not self.functional
1112 gn_end = graph.Node(self.graph)
1113 sym_result = smt.Constant(self.tr_type(n_expr.typ),
1114 self.new_temp_name())
1116 for n_action in n_expr.actions:
1117 test_value, test_valid = self.tr_expression(n_action.n_cond)
1118 self.attach_validity_check(test_valid, n_action.n_cond)
1119 current_start = self.start
1121 # Create path where action is true
1122 self.attach_assumption(test_value)
1123 res_value, res_valid = self.tr_expression(n_action.n_expr)
1124 self.attach_validity_check(res_valid, n_action.n_expr)
1125 self.attach_temp_declaration(n_action,
1126 sym_result,
1127 res_value)
1128 self.start.add_edge_to(gn_end)
1130 # Reset to test and proceed with the other actions
1131 self.start = current_start
1132 self.attach_assumption(smt.Boolean_Negation(test_value))
1134 # Finally execute the else part
1135 res_value, res_valid = self.tr_expression(n_expr.else_expr)
1136 self.attach_validity_check(res_valid, n_expr.else_expr)
1137 self.attach_temp_declaration(n_expr,
1138 sym_result,
1139 res_value)
1140 self.start.add_edge_to(gn_end)
1142 # And join
1143 self.start = gn_end
1144 return sym_result, smt.Boolean_Literal(True)
1146 def tr_op_implication(self, n_expr):
1147 assert isinstance(n_expr, Binary_Expression)
1148 assert n_expr.operator == Binary_Operator.LOGICAL_IMPLIES
1150 if self.functional:
1151 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1152 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1153 return self.create_return(n_expr,
1154 smt.Implication(lhs_value, rhs_value))
1156 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1157 # Emit VC for validity
1158 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1160 # Split into two paths.
1161 current_start = self.start
1162 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1163 self.new_temp_name())
1164 gn_end = graph.Node(self.graph)
1166 ### 1: Implication is not valid
1167 self.start = current_start
1168 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1169 self.attach_temp_declaration(n_expr,
1170 sym_result,
1171 smt.Boolean_Literal(True))
1172 self.start.add_edge_to(gn_end)
1174 ### 2: Implication is valid.
1175 self.start = current_start
1176 self.attach_assumption(lhs_value)
1177 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1178 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1179 self.attach_temp_declaration(n_expr,
1180 sym_result,
1181 rhs_value)
1182 self.start.add_edge_to(gn_end)
1184 # Join paths
1185 self.start = gn_end
1187 return sym_result, smt.Boolean_Literal(True)
1189 def tr_op_and(self, n_expr):
1190 assert isinstance(n_expr, Binary_Expression)
1191 assert n_expr.operator == Binary_Operator.LOGICAL_AND
1193 if self.functional:
1194 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1195 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1196 return self.create_return(n_expr,
1197 smt.Conjunction(lhs_value, rhs_value))
1199 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1200 # Emit VC for validity
1201 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1203 # Split into two paths.
1204 current_start = self.start
1205 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1206 self.new_temp_name())
1207 gn_end = graph.Node(self.graph)
1209 ### 1: LHS is not true
1210 self.start = current_start
1211 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1212 self.attach_temp_declaration(n_expr,
1213 sym_result,
1214 smt.Boolean_Literal(False))
1215 self.start.add_edge_to(gn_end)
1217 ### 2: LHS is true
1218 self.start = current_start
1219 self.attach_assumption(lhs_value)
1220 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1221 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1222 self.attach_temp_declaration(n_expr,
1223 sym_result,
1224 rhs_value)
1225 self.start.add_edge_to(gn_end)
1227 # Join paths
1228 self.start = gn_end
1230 return sym_result, smt.Boolean_Literal(True)
1232 def tr_op_or(self, n_expr):
1233 assert isinstance(n_expr, Binary_Expression)
1234 assert n_expr.operator == Binary_Operator.LOGICAL_OR
1236 if self.functional: 1236 ↛ 1237line 1236 didn't jump to line 1237 because the condition on line 1236 was never true
1237 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1238 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1239 return self.create_return(n_expr,
1240 smt.Disjunction(lhs_value, rhs_value))
1242 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1243 # Emit VC for validity
1244 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1246 # Split into two paths.
1247 current_start = self.start
1248 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1249 self.new_temp_name())
1250 gn_end = graph.Node(self.graph)
1252 ### 1: LHS is true
1253 self.start = current_start
1254 self.attach_assumption(lhs_value)
1255 self.attach_temp_declaration(n_expr,
1256 sym_result,
1257 smt.Boolean_Literal(True))
1258 self.start.add_edge_to(gn_end)
1260 ### 2: LHS is not true
1261 self.start = current_start
1262 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1263 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1264 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1265 self.attach_temp_declaration(n_expr,
1266 sym_result,
1267 rhs_value)
1268 self.start.add_edge_to(gn_end)
1270 # Join paths
1271 self.start = gn_end
1273 return sym_result, smt.Boolean_Literal(True)
1275 def tr_core_equality_tuple_component(self, n_component, lhs, rhs):
1276 assert isinstance(n_component, Composite_Component)
1277 assert isinstance(lhs, smt.Expression)
1278 assert isinstance(rhs, smt.Expression)
1280 value_lhs = smt.Record_Access(lhs,
1281 n_component.name + ".value")
1282 value_rhs = smt.Record_Access(rhs,
1283 n_component.name + ".value")
1284 valid_equal = self.tr_core_equality(n_component.n_typ,
1285 value_lhs,
1286 value_rhs)
1288 if not n_component.optional:
1289 return valid_equal
1291 valid_lhs = smt.Record_Access(lhs,
1292 n_component.name + ".valid")
1293 valid_rhs = smt.Record_Access(rhs,
1294 n_component.name + ".valid")
1296 return smt.Conjunction(
1297 smt.Comparison("=", valid_lhs, valid_rhs),
1298 smt.Implication(valid_lhs, valid_equal))
1300 def tr_core_equality(self, n_typ, lhs, rhs):
1301 assert isinstance(n_typ, Type)
1302 assert isinstance(lhs, smt.Expression)
1303 assert isinstance(rhs, smt.Expression)
1305 if isinstance(n_typ, Tuple_Type):
1306 parts = []
1307 for n_component in n_typ.all_components():
1308 parts.append(
1309 self.tr_core_equality_tuple_component(n_component,
1310 lhs,
1311 rhs))
1313 if len(parts) == 0: 1313 ↛ 1314line 1313 didn't jump to line 1314 because the condition on line 1313 was never true
1314 return smt.Boolean_Literal(True)
1315 elif len(parts) == 1: 1315 ↛ 1316line 1315 didn't jump to line 1316 because the condition on line 1315 was never true
1316 return parts[0]
1317 else:
1318 result = smt.Conjunction(parts[0], parts[1])
1319 for part in parts[2:]:
1320 result = smt.Conjunction(result, part)
1321 return result
1323 else:
1324 return smt.Comparison("=", lhs, rhs)
1326 def tr_op_equality(self, n_expr):
1327 assert isinstance(n_expr, Binary_Expression)
1328 assert n_expr.operator in (Binary_Operator.COMP_EQ,
1329 Binary_Operator.COMP_NEQ)
1331 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1332 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1334 if lhs_value is None:
1335 comp_typ = n_expr.n_rhs.typ
1336 else:
1337 comp_typ = n_expr.n_lhs.typ
1339 if lhs_valid.is_static_true() and rhs_valid.is_static_true():
1340 # Simplified form, this is just x == y
1341 result = self.tr_core_equality(comp_typ,
1342 lhs_value,
1343 rhs_value)
1345 elif lhs_valid.is_static_false() and rhs_valid.is_static_false():
1346 # This is null == null, so true
1347 result = smt.Boolean_Literal(True)
1349 elif lhs_value is None: 1349 ↛ 1351line 1349 didn't jump to line 1351 because the condition on line 1349 was never true
1350 # This is null == <expr>, true iff rhs is null
1351 result = smt.Boolean_Negation(rhs_valid)
1353 elif rhs_value is None:
1354 # This is <expr> == null, true iff lhs is null
1355 result = smt.Boolean_Negation(lhs_valid)
1357 else:
1358 # This is <expr> == <expr> without shortcuts
1359 result = smt.Conjunction(
1360 smt.Comparison("=", lhs_valid, rhs_valid),
1361 smt.Implication(lhs_valid,
1362 self.tr_core_equality(comp_typ,
1363 lhs_value,
1364 rhs_value)))
1366 if n_expr.operator == Binary_Operator.COMP_NEQ:
1367 result = smt.Boolean_Negation(result)
1369 return self.create_return(n_expr, result)
1371 def tr_quantified_expression(self, n_expr):
1372 assert isinstance(n_expr, Quantified_Expression)
1374 # Nested quantifiers are not supported yet
1375 if self.functional: # pragma: no cover
1376 self.flag_unsupported(n_expr,
1377 "functional evaluation of quantifier")
1379 # TRLC quantifier
1380 # (forall x in arr_name => body)
1381 #
1382 # SMT quantifier
1383 # (forall ((i Int))
1384 # (=> (and (>= i 0) (< i (seq.len arr_name)))
1385 # (... (seq.nth arr_name i) ... )))
1386 #
1387 # There is an alternative which is:
1388 # (forall ((element ElementSort))
1389 # (=> (seq.contains arr_name (seq.unit element))
1390 # (... element ...)
1391 #
1392 # However it looks like for CVC5 at least this generates more
1393 # unknown and less unsat if a check depends on the explicit
1394 # value of some sequence member.
1396 # Evaluate subject first and creat a null check
1397 s_subject_value, s_subject_valid = \
1398 self.tr_name_reference(n_expr.n_source)
1399 self.attach_validity_check(s_subject_valid, n_expr.n_source)
1401 # Create validity checks for the body. We do this by creating
1402 # a new branch and eliminating the quantifier; pretending it's
1403 # a forall (since we want to show that for all evaluations
1404 # it's valid).
1405 current_start = self.start
1406 self.attach_empty_assumption()
1407 src_typ = n_expr.n_source.typ
1408 assert isinstance(src_typ, Array_Type)
1409 s_qe_index = smt.Constant(smt.BUILTIN_INTEGER,
1410 self.new_temp_name())
1411 self.start.add_statement(
1412 smt.Constant_Declaration(
1413 symbol = s_qe_index,
1414 comment = ("quantifier elimination (index) for %s at %s" %
1415 (n_expr.to_string(),
1416 n_expr.location.to_string()))))
1417 self.start.add_statement(
1418 smt.Assertion(smt.Comparison(">=",
1419 s_qe_index,
1420 smt.Integer_Literal(0))))
1421 self.start.add_statement(
1422 smt.Assertion(
1423 smt.Comparison("<",
1424 s_qe_index,
1425 smt.Sequence_Length(s_subject_value))))
1426 s_qe_sym = smt.Constant(self.tr_type(src_typ.element_type),
1427 self.new_temp_name())
1428 self.start.add_statement(
1429 smt.Constant_Declaration(
1430 symbol = s_qe_sym,
1431 value = smt.Sequence_Index(s_subject_value, s_qe_index),
1432 comment = ("quantifier elimination (symbol) for %s at %s" %
1433 (n_expr.to_string(),
1434 n_expr.location.to_string()))))
1435 self.qe_vars[n_expr.n_var] = s_qe_sym
1437 _, b_valid = self.tr_expression(n_expr.n_expr)
1438 self.attach_validity_check(b_valid, n_expr.n_expr)
1440 self.start = current_start
1441 del self.qe_vars[n_expr.n_var]
1443 # We have now shown that any path in the quantifier cannot
1444 # raise exception. Asserting the actual value of the
1445 # quantifier is more awkward.
1447 s_q_idx = smt.Bound_Variable(smt.BUILTIN_INTEGER,
1448 self.new_temp_name())
1449 s_q_sym = smt.Sequence_Index(s_subject_value, s_q_idx)
1450 self.bound_vars[n_expr.n_var] = s_q_sym
1452 temp, self.functional = self.functional, True
1453 b_value, _ = self.tr_expression(n_expr.n_expr)
1454 self.functional = temp
1456 bounds_expr = smt.Conjunction(
1457 smt.Comparison(">=",
1458 s_q_idx,
1459 smt.Integer_Literal(0)),
1460 smt.Comparison("<",
1461 s_q_idx,
1462 smt.Sequence_Length(s_subject_value)))
1463 if n_expr.universal:
1464 value = smt.Quantifier(
1465 "forall",
1466 [s_q_idx],
1467 smt.Implication(bounds_expr, b_value))
1468 else:
1469 value = smt.Quantifier(
1470 "exists",
1471 [s_q_idx],
1472 smt.Conjunction(bounds_expr, b_value))
1474 return value, smt.Boolean_Literal(True)
1476 def _ensure_record_deref(self, type_key, sort_name, uf_name,
1477 components):
1478 """Lazily create an SMT record sort and uninterpreted function
1479 for dereferencing integer-encoded references.
1481 :param type_key: cache key; always the canonical sort_name string
1482 :param sort_name: name for the SMT Record sort
1483 :param uf_name: name for the UF mapping integer to sort
1484 :param components: iterable of (field_name, smt_sort, needs_valid)
1485 :returns: (record_sort, to_record_uf)
1486 """
1487 if type_key in self.records:
1488 return self.records[type_key], self.uf_records[type_key]
1490 record_sort = smt.Record(sort_name)
1491 for field_name, field_sort, needs_valid in components:
1492 record_sort.add_component(field_name + ".value", field_sort)
1493 if needs_valid:
1494 record_sort.add_component(field_name + ".valid",
1495 smt.BUILTIN_BOOLEAN)
1496 self.records[type_key] = record_sort
1497 self.preamble.add_statement(
1498 smt.Record_Declaration(
1499 record_sort,
1500 sort_name))
1502 to_record_uf = smt.Function(
1503 uf_name, record_sort,
1504 smt.Bound_Variable(smt.BUILTIN_INTEGER, "ref"))
1505 self.preamble.add_statement(
1506 smt.Function_Declaration(to_record_uf))
1507 self.uf_records[type_key] = to_record_uf
1509 return record_sort, to_record_uf
1511 def tr_field_access_expression(self, n_expr):
1512 assert isinstance(n_expr, Field_Access_Expression)
1514 prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix)
1515 prefix_typ = n_expr.n_prefix.typ
1516 if not self.functional:
1517 self.attach_validity_check(prefix_valid, n_expr.n_prefix)
1519 if isinstance(prefix_typ, Tuple_Type):
1520 field_value = smt.Record_Access(prefix_value,
1521 n_expr.n_field.name + ".value")
1522 if n_expr.n_field.optional:
1523 field_valid = smt.Record_Access(prefix_value,
1524 n_expr.n_field.name + ".valid")
1525 else:
1526 field_valid = smt.Boolean_Literal(True)
1528 elif isinstance(prefix_typ, (Record_Type, Union_Type)):
1529 # lobster-trace: LRM.Union_Type_Field_Access
1530 # lobster-trace: LRM.Union_Type_Partial_Field_Access
1531 # lobster-trace: LRM.Union_Type_Partial_Field_Null
1532 # Both Record_Type and Union_Type are represented as
1533 # integers. We create a record sort with accessible
1534 # fields and a UF to dereference the integer.
1535 if isinstance(prefix_typ, Record_Type):
1536 components = [
1537 (c.name, self.tr_type(c.n_typ), c.optional)
1538 for c in prefix_typ.all_components()
1539 ]
1540 sort_name = "%s.%s" % (prefix_typ.n_package.name,
1541 prefix_typ.name)
1542 uf_name = "access.%s.%s" % (prefix_typ.n_package.name,
1543 prefix_typ.name)
1544 else:
1545 field_map = prefix_typ.get_field_map()
1546 union_id = "_".join(t.fully_qualified_name()
1547 for t in prefix_typ.types)
1548 components = [
1549 (name,
1550 self.tr_type(info["n_typ"]),
1551 info["count"] != info["total"] or
1552 info["optional_in_any"])
1553 for name, info in field_map.items()
1554 if info["n_typ"] is not None
1555 ]
1556 sort_name = "union." + union_id
1557 uf_name = "access.union." + union_id
1559 _, to_record_uf = self._ensure_record_deref(
1560 sort_name, sort_name, uf_name, components)
1561 dereference = smt.Function_Application(to_record_uf,
1562 prefix_value)
1564 # Perform the field access on the dereferenced record
1565 field_value = smt.Record_Access(dereference,
1566 n_expr.n_field.name + ".value")
1567 if isinstance(prefix_typ, Union_Type):
1568 info = prefix_typ.get_field_map()[n_expr.n_field.name]
1569 has_valid = (info["count"] != info["total"] or
1570 info["optional_in_any"])
1571 else:
1572 has_valid = n_expr.n_field.optional
1574 if has_valid:
1575 field_valid = smt.Record_Access(
1576 dereference,
1577 n_expr.n_field.name + ".valid")
1578 else:
1579 field_valid = smt.Boolean_Literal(True)
1581 else:
1582 self.mh.ice_loc(n_expr.n_prefix.location,
1583 "unexpected type %s as prefix of field access" %
1584 n_expr.n_prefix.typ.__class__.__name__)
1586 # pylint: disable=possibly-used-before-assignment
1587 return field_value, field_valid