Coverage for trlc/vcg.py: 97%
794 statements
« prev ^ index » next coverage.py v7.10.7, created at 2026-05-21 07:21 +0000
1#!/usr/bin/env python3
2#
3# TRLC - Treat Requirements Like Code
4# Copyright (C) 2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG)
5# Copyright (C) 2023-2025 Florian Schanda
6#
7# This file is part of the TRLC Python Reference Implementation.
8#
9# TRLC is free software: you can redistribute it and/or modify it
10# under the terms of the GNU General Public License as published by
11# the Free Software Foundation, either version 3 of the License, or
12# (at your option) any later version.
13#
14# TRLC is distributed in the hope that it will be useful, but WITHOUT
15# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
16# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
17# License for more details.
18#
19# You should have received a copy of the GNU General Public License
20# along with TRLC. If not, see <https://www.gnu.org/licenses/>.
22import subprocess
24from trlc.ast import *
25from trlc.errors import Location, Message_Handler
27try:
28 from pyvcg import smt
29 from pyvcg import graph
30 from pyvcg import vcg
31 from pyvcg.driver.file_smtlib import SMTLIB_Generator
32 from pyvcg.driver.cvc5_smtlib import CVC5_File_Solver
33 VCG_AVAILABLE = True
34except ImportError: # pragma: no cover
35 VCG_AVAILABLE = False
37try:
38 from pyvcg.driver.cvc5_api import CVC5_Solver
39 CVC5_API_AVAILABLE = True
40except ImportError: # pragma: no cover
41 CVC5_API_AVAILABLE = False
43CVC5_OPTIONS = {
44 "tlimit-per" : 2500,
45 "seed" : 42,
46 "sat-random-seed" : 42,
47}
50class Unsupported(Exception): # pragma: no cover
51 # lobster-exclude: Not safety relevant
52 def __init__(self, node, text):
53 assert isinstance(node, Node)
54 assert isinstance(text, str) or text is None
55 super().__init__()
56 self.message = "%s not yet supported in VCG" % \
57 (text if text else node.__class__.__name__)
58 self.location = node.location
61class Feedback:
62 # lobster-exclude: Not safety relevant
63 def __init__(self, node, message, kind, expect_unsat=True):
64 assert isinstance(node, Expression)
65 assert isinstance(message, str)
66 assert isinstance(kind, str)
67 assert isinstance(expect_unsat, bool)
68 self.node = node
69 self.message = message
70 self.kind = "vcg-" + kind
71 self.expect_unsat = expect_unsat
74class VCG:
75 # lobster-exclude: Not safety relevant
76 def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None):
77 assert VCG_AVAILABLE
78 assert isinstance(mh, Message_Handler)
79 assert isinstance(n_ctyp, Composite_Type)
80 assert isinstance(debug, bool)
81 assert isinstance(use_api, bool)
82 assert use_api or isinstance(cvc5_binary, str)
84 self.mh = mh
85 self.n_ctyp = n_ctyp
86 self.debug = debug
87 self.use_api = use_api
88 self.cvc5_bin = cvc5_binary
90 self.vc_name = "trlc-%s-%s" % (n_ctyp.n_package.name,
91 n_ctyp.name)
93 self.tmp_id = 0
95 self.vcg = vcg.VCG()
96 self.graph = self.vcg.graph
97 self.start = self.vcg.start
98 # Current start node, we will update this as we go along.
99 self.preamble = None
100 # We do remember the first node where we put all our
101 # declarations, in case we need to add some more later.
103 self.constants = {}
104 self.enumerations = {}
105 self.tuples = {}
106 self.records = {}
107 self.arrays = {}
108 self.bound_vars = {}
109 self.qe_vars = {}
110 self.tuple_base = {}
111 self.uf_records = {}
113 self.uf_matches = None
114 # Pointer to the UF we use for matches. We only generate it
115 # when we must, as it may affect the logics selected due to
116 # string theory being used.
118 self.functional = False
119 # If set to true, then we ignore validity checks and do not
120 # create intermediates. We just build the value and validity
121 # expresions and return them.
123 self.emit_checks = True
124 # If set to false, we skip creating checks.
126 @staticmethod
127 def flag_unsupported(node, text=None): # pragma: no cover
128 assert isinstance(node, Node)
129 raise Unsupported(node, text)
131 def new_temp_name(self):
132 self.tmp_id += 1
133 return "tmp.%u" % self.tmp_id
135 def get_uf_matches(self):
136 if self.uf_matches is None:
137 self.uf_matches = \
138 smt.Function("trlc.matches",
139 smt.BUILTIN_BOOLEAN,
140 smt.Bound_Variable(smt.BUILTIN_STRING,
141 "subject"),
142 smt.Bound_Variable(smt.BUILTIN_STRING,
143 "regex"))
145 # Create UF for the matches function (for now, later we
146 # will deal with regex properly).
147 self.preamble.add_statement(
148 smt.Function_Declaration(self.uf_matches))
150 return self.uf_matches
152 def create_return(self, node, s_value, s_valid=None):
153 assert isinstance(node, Expression)
154 assert isinstance(s_value, smt.Expression)
155 assert isinstance(s_valid, smt.Expression) or s_valid is None
157 if s_valid is None: 157 ↛ 160line 157 didn't jump to line 160 because the condition on line 157 was always true
158 s_valid = smt.Boolean_Literal(True)
160 if self.functional:
161 return s_value, s_valid
163 else:
164 sym_result = smt.Constant(s_value.sort,
165 self.new_temp_name())
166 self.attach_temp_declaration(node, sym_result, s_value)
168 return sym_result, s_valid
170 def attach_validity_check(self, bool_expr, origin):
171 assert isinstance(bool_expr, smt.Expression)
172 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
173 assert isinstance(origin, Expression)
174 assert not self.functional
176 if not self.emit_checks:
177 return
179 # Attach new graph node advance start
180 if not bool_expr.is_static_true():
181 gn_check = graph.Check(self.graph)
182 gn_check.add_goal(bool_expr,
183 Feedback(origin,
184 "expression could be null",
185 "evaluation-of-null"),
186 "validity check for %s" % origin.to_string())
187 self.start.add_edge_to(gn_check)
188 self.start = gn_check
190 def attach_int_division_check(self, int_expr, origin):
191 assert isinstance(int_expr, smt.Expression)
192 assert int_expr.sort is smt.BUILTIN_INTEGER
193 assert isinstance(origin, Expression)
194 assert not self.functional
196 if not self.emit_checks: 196 ↛ 197line 196 didn't jump to line 197 because the condition on line 196 was never true
197 return
199 # Attach new graph node advance start
200 gn_check = graph.Check(self.graph)
201 gn_check.add_goal(
202 smt.Boolean_Negation(
203 smt.Comparison("=", int_expr, smt.Integer_Literal(0))),
204 Feedback(origin,
205 "divisor could be 0",
206 "div-by-zero"),
207 "division by zero check for %s" % origin.to_string())
208 self.start.add_edge_to(gn_check)
209 self.start = gn_check
211 def attach_real_division_check(self, real_expr, origin):
212 assert isinstance(real_expr, smt.Expression)
213 assert real_expr.sort is smt.BUILTIN_REAL
214 assert isinstance(origin, Expression)
215 assert not self.functional
217 if not self.emit_checks: 217 ↛ 218line 217 didn't jump to line 218 because the condition on line 217 was never true
218 return
220 # Attach new graph node advance start
221 gn_check = graph.Check(self.graph)
222 gn_check.add_goal(
223 smt.Boolean_Negation(
224 smt.Comparison("=", real_expr, smt.Real_Literal(0))),
225 Feedback(origin,
226 "divisor could be 0.0",
227 "div-by-zero"),
228 "division by zero check for %s" % origin.to_string())
229 self.start.add_edge_to(gn_check)
230 self.start = gn_check
232 def attach_index_check(self, seq_expr, index_expr, origin):
233 assert isinstance(seq_expr, smt.Expression)
234 assert isinstance(seq_expr.sort, smt.Sequence_Sort)
235 assert isinstance(index_expr, smt.Expression)
236 assert index_expr.sort is smt.BUILTIN_INTEGER
237 assert isinstance(origin, Binary_Expression)
238 assert origin.operator == Binary_Operator.INDEX
239 assert not self.functional
241 if not self.emit_checks: 241 ↛ 242line 241 didn't jump to line 242 because the condition on line 241 was never true
242 return
244 # Attach new graph node advance start
245 gn_check = graph.Check(self.graph)
246 gn_check.add_goal(
247 smt.Comparison(">=", index_expr, smt.Integer_Literal(0)),
248 Feedback(origin,
249 "array index could be less than 0",
250 "array-index"),
251 "index lower bound check for %s" % origin.to_string())
252 gn_check.add_goal(
253 smt.Comparison("<",
254 index_expr,
255 smt.Sequence_Length(seq_expr)),
256 Feedback(origin,
257 "array index could be larger than len(%s)" %
258 origin.n_lhs.to_string(),
259 "array-index"),
260 "index lower bound check for %s" % origin.to_string())
262 self.start.add_edge_to(gn_check)
263 self.start = gn_check
265 def attach_feasability_check(self, bool_expr, origin):
266 assert isinstance(bool_expr, smt.Expression)
267 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
268 assert isinstance(origin, Expression)
269 assert not self.functional
271 if not self.emit_checks:
272 return
274 # Attach new graph node advance start
275 gn_check = graph.Check(self.graph)
276 gn_check.add_goal(bool_expr,
277 Feedback(origin,
278 "expression is always true",
279 "always-true",
280 expect_unsat = False),
281 "feasability check for %s" % origin.to_string())
282 self.start.add_edge_to(gn_check)
284 def attach_assumption(self, bool_expr):
285 assert isinstance(bool_expr, smt.Expression)
286 assert bool_expr.sort is smt.BUILTIN_BOOLEAN
287 assert not self.functional
289 # Attach new graph node advance start
290 gn_ass = graph.Assumption(self.graph)
291 gn_ass.add_statement(smt.Assertion(bool_expr))
292 self.start.add_edge_to(gn_ass)
293 self.start = gn_ass
295 def attach_temp_declaration(self, node, sym, value=None):
296 assert isinstance(node, (Expression, Action))
297 assert isinstance(sym, smt.Constant)
298 assert isinstance(value, smt.Expression) or value is None
299 assert not self.functional
301 # Attach new graph node advance start
302 gn_decl = graph.Assumption(self.graph)
303 gn_decl.add_statement(
304 smt.Constant_Declaration(
305 symbol = sym,
306 value = value,
307 comment = "result of %s at %s" % (node.to_string(),
308 node.location.to_string()),
309 relevant = False))
310 self.start.add_edge_to(gn_decl)
311 self.start = gn_decl
313 def attach_empty_assumption(self):
314 assert not self.functional
316 # Attach new graph node advance start
317 gn_decl = graph.Assumption(self.graph)
318 self.start.add_edge_to(gn_decl)
319 self.start = gn_decl
321 def analyze(self):
322 try:
323 self.checks_on_composite_type(self.n_ctyp)
324 except Unsupported as exc: # pragma: no cover
325 self.mh.warning(exc.location,
326 exc.message)
328 def checks_on_composite_type(self, n_ctyp):
329 assert isinstance(n_ctyp, Composite_Type)
331 # Create node for global declarations
332 gn_locals = graph.Assumption(self.graph)
333 self.start.add_edge_to(gn_locals)
334 self.start = gn_locals
335 self.preamble = gn_locals
337 # Create local variables
338 for n_component in n_ctyp.all_components():
339 self.tr_component_decl(n_component, self.start)
341 # Create paths for checks in two phases:
342 # Phase A ("at declaration"): checks that do not follow any
343 # record or union reference via field access. These are fully
344 # self-contained and are analyzed first.
345 # Phase B ("after references"): checks that dereference at
346 # least one record or union reference. They run after Phase A
347 # so that knowledge accumulated from Phase A fatal checks is
348 # available.
349 for phase in (False, True):
350 for n_check in n_ctyp.iter_checks():
351 if n_check.uses_field_access != phase:
352 continue
353 current_start = self.start
354 self.tr_check(n_check)
356 # Only fatal checks contribute to the total knowledge
357 if n_check.severity != "fatal":
358 self.start = current_start
360 # Emit debug graph
361 if self.debug: # pragma: no cover
362 subprocess.run(["dot", "-Tpdf", "-o%s.pdf" % self.vc_name],
363 input = self.graph.debug_render_dot(),
364 check = True,
365 encoding = "UTF-8")
367 # Generate VCs
368 self.vcg.generate()
370 # Solve VCs and provide feedback
371 nok_feasibility_checks = []
372 ok_feasibility_checks = set()
373 nok_validity_checks = set()
375 for vc_id, vc in enumerate(self.vcg.vcs):
376 if self.debug: # pramga: no cover 376 ↛ 377line 376 didn't jump to line 377 because the condition on line 376 was never true
377 with open(self.vc_name + "_%04u.smt2" % vc_id, "w",
378 encoding="UTF-8") as fd:
379 fd.write(vc["script"].generate_vc(SMTLIB_Generator()))
381 # Checks that have already failed don't need to be checked
382 # again on a different path
383 if vc["feedback"].expect_unsat and \
384 vc["feedback"] in nok_validity_checks:
385 continue
387 if self.use_api:
388 solver = CVC5_Solver()
389 else:
390 solver = CVC5_File_Solver(self.cvc5_bin)
391 for name, value in CVC5_OPTIONS.items():
392 solver.set_solver_option(name, value)
394 status, values = vc["script"].solve_vc(solver)
396 message = vc["feedback"].message
397 if self.debug: # pragma: no cover
398 message += " [vc_id = %u]" % vc_id
400 if vc["feedback"].expect_unsat:
401 if status != "unsat":
402 self.mh.check(vc["feedback"].node.location,
403 message,
404 vc["feedback"].kind,
405 self.create_counterexample(status,
406 values))
407 nok_validity_checks.add(vc["feedback"])
408 else:
409 if status == "unsat":
410 nok_feasibility_checks.append(vc["feedback"])
411 else:
412 ok_feasibility_checks.add(vc["feedback"])
414 # This is a bit wonky, but this way we make sure the ording is
415 # consistent
416 for feedback in nok_feasibility_checks:
417 if feedback not in ok_feasibility_checks:
418 self.mh.check(feedback.node.location,
419 feedback.message,
420 feedback.kind)
421 ok_feasibility_checks.add(feedback)
423 def create_counterexample(self, status, values):
424 rv = [
425 "example %s triggering error:" %
426 self.n_ctyp.__class__.__name__.lower(),
427 " %s bad_potato {" % self.n_ctyp.name
428 ]
430 for n_component in self.n_ctyp.all_components():
431 id_value = self.tr_component_value_name(n_component)
432 id_valid = self.tr_component_valid_name(n_component)
433 if status == "unknown" and (id_value not in values or 433 ↛ 435line 433 didn't jump to line 435 because the condition on line 433 was never true
434 id_valid not in values):
435 rv.append(" %s = ???" % n_component.name)
436 elif values.get(id_valid):
437 rv.append(" %s = %s" %
438 (n_component.name,
439 self.value_to_trlc(n_component.n_typ,
440 values[id_value])))
441 else:
442 rv.append(" /* %s is null */" % n_component.name)
444 rv.append(" }")
445 if status == "unknown":
446 rv.append("/* note: counter-example is unreliable in this case */")
447 return "\n".join(rv)
449 def fraction_to_decimal_string(self, num, den):
450 assert isinstance(num, int)
451 assert isinstance(den, int) and den >= 1
453 tmp = den
454 if tmp > 2:
455 while tmp > 1:
456 if tmp % 2 == 0:
457 tmp = tmp // 2
458 elif tmp % 5 == 0:
459 tmp = tmp // 5
460 else:
461 return "%i / %u" % (num, den)
463 rv = str(abs(num) // den)
465 i = abs(num) % den
466 j = den
468 if i > 0:
469 rv += "."
470 while i > 0:
471 i *= 10
472 rv += str(i // j)
473 i = i % j
474 else:
475 rv += ".0"
477 if num < 0:
478 return "-" + rv
479 else:
480 return rv
482 def value_to_trlc(self, n_typ, value):
483 assert isinstance(n_typ, Type)
485 if isinstance(n_typ, Builtin_Integer):
486 return str(value)
488 elif isinstance(n_typ, Builtin_Decimal):
489 if isinstance(value, Fraction):
490 num, den = value.as_integer_ratio()
491 if den >= 1: 491 ↛ 494line 491 didn't jump to line 494 because the condition on line 491 was always true
492 return self.fraction_to_decimal_string(num, den)
493 else:
494 return self.fraction_to_decimal_string(-num, -den)
495 else:
496 return "/* unable to generate precise value */"
498 elif isinstance(n_typ, Builtin_Boolean):
499 return "true" if value else "false"
501 elif isinstance(n_typ, Enumeration_Type):
502 return n_typ.name + "." + value
504 elif isinstance(n_typ, Builtin_String):
505 if "\n" in value:
506 return "'''%s'''" % value
507 else:
508 return '"%s"' % value
510 elif isinstance(n_typ, (Record_Type, Union_Type)):
511 # lobster-trace: LRM.Union_Type_Equality
512 if value < 0:
513 instance_id = value * -2 - 1
514 else:
515 instance_id = value * 2
516 if isinstance(n_typ, Record_Type): 516 ↛ 524line 516 didn't jump to line 524 because the condition on line 516 was always true
517 if n_typ.n_package is self.n_ctyp.n_package:
518 return "%s_instance_%i" % (n_typ.name, instance_id)
519 else:
520 return "%s.%s_instance_%i" % (n_typ.n_package.name,
521 n_typ.name,
522 instance_id)
523 else:
524 return "instance_%i" % instance_id
526 elif isinstance(n_typ, Tuple_Type):
527 parts = []
528 for n_item in n_typ.iter_sequence():
529 if isinstance(n_item, Composite_Component):
530 if n_item.optional and not value[n_item.name + ".valid"]:
531 parts.pop()
532 break
533 parts.append(
534 self.value_to_trlc(n_item.n_typ,
535 value[n_item.name + ".value"]))
537 else:
538 assert isinstance(n_item, Separator)
539 sep_text = {
540 "AT" : "@",
541 "COLON" : ":",
542 "SEMICOLON" : ";"
543 }.get(n_item.token.kind, n_item.token.value)
544 parts.append(sep_text)
546 if n_typ.has_separators():
547 return "".join(parts)
548 else:
549 return "(%s)" % ", ".join(parts)
551 elif isinstance(n_typ, Array_Type):
552 return "[%s]" % ", ".join(self.value_to_trlc(n_typ.element_type,
553 item)
554 for item in value)
556 else: # pragma: no cover
557 self.flag_unsupported(n_typ,
558 "back-conversion from %s" % n_typ.name)
560 def tr_component_value_name(self, n_component):
561 return n_component.member_of.fully_qualified_name() + \
562 "." + n_component.name + ".value"
564 def tr_component_valid_name(self, n_component):
565 return n_component.member_of.fully_qualified_name() + \
566 "." + n_component.name + ".valid"
568 def emit_tuple_constraints(self, n_tuple, s_sym):
569 assert isinstance(n_tuple, Tuple_Type)
570 assert isinstance(s_sym, smt.Constant)
572 old_functional, self.functional = self.functional, True
573 self.tuple_base[n_tuple] = s_sym
575 constraints = []
577 # The first tuple constraint is that all checks must have
578 # passed, otherwise the tool would just error. An error in a
579 # tuple is pretty much the same as a fatal in the enclosing
580 # record.
582 for n_check in n_tuple.iter_checks():
583 if n_check.severity == "warning":
584 continue
585 # We do consider both fatal and errors to be sources of
586 # truth here.
587 c_value, _ = self.tr_expression(n_check.n_expr)
588 constraints.append(c_value)
590 # The secopnd tuple constraint is that once you get a null
591 # field, all following fields must also be null.
593 components = n_tuple.all_components()
594 for i, component in enumerate(components):
595 if component.optional:
596 condition = smt.Boolean_Negation(
597 smt.Record_Access(s_sym,
598 component.name + ".valid"))
599 consequences = [
600 smt.Boolean_Negation(
601 smt.Record_Access(s_sym,
602 c.name + ".valid"))
603 for c in components[i + 1:]
604 ]
605 if len(consequences) == 0:
606 break
607 elif len(consequences) == 1: 607 ↛ 610line 607 didn't jump to line 610 because the condition on line 607 was always true
608 consequence = consequences[0]
609 else:
610 consequence = smt.Conjunction(*consequences)
611 constraints.append(smt.Implication(condition, consequence))
613 del self.tuple_base[n_tuple]
614 self.functional = old_functional
616 for cons in constraints:
617 self.start.add_statement(smt.Assertion(cons))
619 def tr_component_decl(self, n_component, gn_locals):
620 assert isinstance(n_component, Composite_Component)
621 assert isinstance(gn_locals, graph.Assumption)
623 if isinstance(self.n_ctyp, Record_Type):
624 frozen = self.n_ctyp.is_frozen(n_component)
625 else:
626 frozen = False
628 id_value = self.tr_component_value_name(n_component)
629 s_sort = self.tr_type(n_component.n_typ)
630 s_sym = smt.Constant(s_sort, id_value)
631 if frozen:
632 old_functional, self.functional = self.functional, True
633 s_val, _ = self.tr_expression(
634 self.n_ctyp.get_freezing_expression(n_component))
635 self.functional = old_functional
636 else:
637 s_val = None
638 s_decl = smt.Constant_Declaration(
639 symbol = s_sym,
640 value = s_val,
641 comment = "value for %s declared on %s" % (
642 n_component.name,
643 n_component.location.to_string()),
644 relevant = True)
645 gn_locals.add_statement(s_decl)
646 self.constants[id_value] = s_sym
648 if isinstance(n_component.n_typ, Tuple_Type):
649 self.emit_tuple_constraints(n_component.n_typ, s_sym)
651 # For arrays we need to add additional constraints for the
652 # length
653 if isinstance(n_component.n_typ, Array_Type):
654 if n_component.n_typ.lower_bound > 0:
655 s_lower = smt.Integer_Literal(n_component.n_typ.lower_bound)
656 gn_locals.add_statement(
657 smt.Assertion(
658 smt.Comparison(">=",
659 smt.Sequence_Length(s_sym),
660 s_lower)))
662 if n_component.n_typ.upper_bound is not None:
663 s_upper = smt.Integer_Literal(n_component.n_typ.upper_bound)
664 gn_locals.add_statement(
665 smt.Assertion(
666 smt.Comparison("<=",
667 smt.Sequence_Length(s_sym),
668 s_upper)))
670 id_valid = self.tr_component_valid_name(n_component)
671 s_sym = smt.Constant(smt.BUILTIN_BOOLEAN, id_valid)
672 s_val = (None
673 if n_component.optional and not frozen
674 else smt.Boolean_Literal(True))
675 s_decl = smt.Constant_Declaration(
676 symbol = s_sym,
677 value = s_val,
678 relevant = True)
679 gn_locals.add_statement(s_decl)
680 self.constants[id_valid] = s_sym
682 def tr_type(self, n_type):
683 assert isinstance(n_type, Type)
685 if isinstance(n_type, Builtin_Boolean):
686 return smt.BUILTIN_BOOLEAN
688 elif isinstance(n_type, Builtin_Integer):
689 return smt.BUILTIN_INTEGER
691 elif isinstance(n_type, Builtin_Decimal):
692 return smt.BUILTIN_REAL
694 elif isinstance(n_type, Builtin_String):
695 return smt.BUILTIN_STRING
697 elif isinstance(n_type, Enumeration_Type):
698 if n_type not in self.enumerations:
699 s_sort = smt.Enumeration(n_type.n_package.name +
700 "." + n_type.name)
701 for n_lit in n_type.literals.values():
702 s_sort.add_literal(n_lit.name)
703 self.enumerations[n_type] = s_sort
704 self.start.add_statement(
705 smt.Enumeration_Declaration(
706 s_sort,
707 "enumeration %s from %s" % (
708 n_type.name,
709 n_type.location.to_string())))
710 return self.enumerations[n_type]
712 elif isinstance(n_type, Tuple_Type):
713 if n_type not in self.tuples:
714 s_sort = smt.Record(n_type.n_package.name +
715 "." + n_type.name)
716 for n_component in n_type.all_components():
717 s_sort.add_component(n_component.name + ".value",
718 self.tr_type(n_component.n_typ))
719 if n_component.optional:
720 s_sort.add_component(n_component.name + ".valid",
721 smt.BUILTIN_BOOLEAN)
722 self.tuples[n_type] = s_sort
723 self.start.add_statement(
724 smt.Record_Declaration(
725 s_sort,
726 "tuple %s from %s" % (
727 n_type.name,
728 n_type.location.to_string())))
730 return self.tuples[n_type]
732 elif isinstance(n_type, Array_Type):
733 if n_type not in self.arrays:
734 s_element_sort = self.tr_type(n_type.element_type)
735 s_sequence = smt.Sequence_Sort(s_element_sort)
736 self.arrays[n_type] = s_sequence
738 return self.arrays[n_type]
740 elif isinstance(n_type, (Record_Type, Union_Type)):
741 # lobster-trace: LRM.union_type
742 # Record and union references are modelled as a free
743 # integer. If we access their field then we use an
744 # uninterpreted function. Some of these have special
745 # meaning:
746 # 0 - the null reference
747 # 1 - the self reference
748 # anything else - uninterpreted
749 return smt.BUILTIN_INTEGER
751 else: # pragma: no cover
752 self.flag_unsupported(n_type)
754 def tr_check(self, n_check):
755 assert isinstance(n_check, Check)
757 # If the check belongs to a different type then we are looking
758 # at a type extension. In this case we do not create checks
759 # again, because if a check would fail it would already have
760 # failed.
761 if n_check.n_type is not self.n_ctyp:
762 old_emit, self.emit_checks = self.emit_checks, False
764 value, valid = self.tr_expression(n_check.n_expr)
765 self.attach_validity_check(valid, n_check.n_expr)
766 self.attach_feasability_check(value, n_check.n_expr)
767 self.attach_assumption(value)
769 if n_check.n_type is not self.n_ctyp:
770 self.emit_checks = old_emit
772 def tr_expression(self, n_expr):
773 value = None
775 if isinstance(n_expr, Name_Reference):
776 return self.tr_name_reference(n_expr)
778 elif isinstance(n_expr, Unary_Expression):
779 return self.tr_unary_expression(n_expr)
781 elif isinstance(n_expr, Binary_Expression):
782 return self.tr_binary_expression(n_expr)
784 elif isinstance(n_expr, Range_Test):
785 return self.tr_range_test(n_expr)
787 elif isinstance(n_expr, OneOf_Expression):
788 return self.tr_oneof_test(n_expr)
790 elif isinstance(n_expr, Conditional_Expression):
791 if self.functional:
792 return self.tr_conditional_expression_functional(n_expr)
793 else:
794 return self.tr_conditional_expression(n_expr)
796 elif isinstance(n_expr, Null_Literal):
797 return None, smt.Boolean_Literal(False)
799 elif isinstance(n_expr, Boolean_Literal):
800 value = smt.Boolean_Literal(n_expr.value)
802 elif isinstance(n_expr, Integer_Literal):
803 value = smt.Integer_Literal(n_expr.value)
805 elif isinstance(n_expr, Decimal_Literal):
806 value = smt.Real_Literal(n_expr.value)
808 elif isinstance(n_expr, Enumeration_Literal):
809 value = smt.Enumeration_Literal(self.tr_type(n_expr.typ),
810 n_expr.value.name)
812 elif isinstance(n_expr, String_Literal):
813 value = smt.String_Literal(n_expr.value)
815 elif isinstance(n_expr, Quantified_Expression):
816 return self.tr_quantified_expression(n_expr)
818 elif isinstance(n_expr, Field_Access_Expression):
819 return self.tr_field_access_expression(n_expr)
821 else: # pragma: no cover
822 self.flag_unsupported(n_expr)
824 return value, smt.Boolean_Literal(True)
826 def tr_name_reference(self, n_ref):
827 assert isinstance(n_ref, Name_Reference)
829 if isinstance(n_ref.entity, Composite_Component):
830 if n_ref.entity.member_of in self.tuple_base:
831 sym = self.tuple_base[n_ref.entity.member_of]
832 if n_ref.entity.optional:
833 s_valid = smt.Record_Access(sym,
834 n_ref.entity.name + ".valid")
835 else:
836 s_valid = smt.Boolean_Literal(True)
837 s_value = smt.Record_Access(sym,
838 n_ref.entity.name + ".value")
839 return s_value, s_valid
841 else:
842 id_value = self.tr_component_value_name(n_ref.entity)
843 id_valid = self.tr_component_valid_name(n_ref.entity)
844 return self.constants[id_value], self.constants[id_valid]
846 else:
847 assert isinstance(n_ref.entity, Quantified_Variable)
848 if n_ref.entity in self.qe_vars:
849 return self.qe_vars[n_ref.entity], smt.Boolean_Literal(True)
850 else:
851 return self.bound_vars[n_ref.entity], smt.Boolean_Literal(True)
853 def tr_unary_expression(self, n_expr):
854 assert isinstance(n_expr, Unary_Expression)
856 operand_value, operand_valid = self.tr_expression(n_expr.n_operand)
857 if not self.functional:
858 self.attach_validity_check(operand_valid, n_expr.n_operand)
860 sym_value = None
862 if n_expr.operator == Unary_Operator.MINUS:
863 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
864 sym_value = smt.Unary_Int_Arithmetic_Op("-",
865 operand_value)
866 else:
867 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
868 sym_value = smt.Unary_Real_Arithmetic_Op("-",
869 operand_value)
871 elif n_expr.operator == Unary_Operator.PLUS:
872 sym_value = operand_value
874 elif n_expr.operator == Unary_Operator.LOGICAL_NOT:
875 sym_value = smt.Boolean_Negation(operand_value)
877 elif n_expr.operator == Unary_Operator.ABSOLUTE_VALUE:
878 if isinstance(n_expr.n_operand.typ, Builtin_Integer):
879 sym_value = smt.Unary_Int_Arithmetic_Op("abs",
880 operand_value)
882 else:
883 assert isinstance(n_expr.n_operand.typ, Builtin_Decimal)
884 sym_value = smt.Unary_Real_Arithmetic_Op("abs",
885 operand_value)
887 elif n_expr.operator == Unary_Operator.STRING_LENGTH:
888 sym_value = smt.String_Length(operand_value)
890 elif n_expr.operator == Unary_Operator.ARRAY_LENGTH:
891 sym_value = smt.Sequence_Length(operand_value)
893 elif n_expr.operator == Unary_Operator.CONVERSION_TO_DECIMAL:
894 sym_value = smt.Conversion_To_Real(operand_value)
896 elif n_expr.operator == Unary_Operator.CONVERSION_TO_INT:
897 sym_value = smt.Conversion_To_Integer("rna", operand_value)
899 else:
900 self.mh.ice_loc(n_expr,
901 "unexpected unary operator %s" %
902 n_expr.operator.name)
904 return self.create_return(n_expr, sym_value)
906 def tr_binary_expression(self, n_expr):
907 assert isinstance(n_expr, Binary_Expression)
909 # Some operators deal with validity in a different way. We
910 # deal with them first and then exit.
911 if n_expr.operator in (Binary_Operator.COMP_EQ,
912 Binary_Operator.COMP_NEQ):
913 return self.tr_op_equality(n_expr)
915 elif n_expr.operator == Binary_Operator.LOGICAL_IMPLIES:
916 return self.tr_op_implication(n_expr)
918 elif n_expr.operator == Binary_Operator.LOGICAL_AND:
919 return self.tr_op_and(n_expr)
921 elif n_expr.operator == Binary_Operator.LOGICAL_OR:
922 return self.tr_op_or(n_expr)
924 # The remaining operators always check for validity, so we can
925 # obtain the values of both sides now.
926 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
927 if not self.functional:
928 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
929 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
930 if not self.functional:
931 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
932 sym_value = None
934 if n_expr.operator == Binary_Operator.LOGICAL_XOR:
935 sym_value = smt.Exclusive_Disjunction(lhs_value, rhs_value)
937 elif n_expr.operator in (Binary_Operator.PLUS,
938 Binary_Operator.MINUS,
939 Binary_Operator.TIMES,
940 Binary_Operator.DIVIDE,
941 Binary_Operator.REMAINDER):
943 if isinstance(n_expr.n_lhs.typ, Builtin_String):
944 assert n_expr.operator == Binary_Operator.PLUS
945 sym_value = smt.String_Concatenation(lhs_value, rhs_value)
947 elif isinstance(n_expr.n_lhs.typ, Builtin_Integer):
948 if n_expr.operator in (Binary_Operator.DIVIDE,
949 Binary_Operator.REMAINDER):
950 self.attach_int_division_check(rhs_value, n_expr)
952 smt_op = {
953 Binary_Operator.PLUS : "+",
954 Binary_Operator.MINUS : "-",
955 Binary_Operator.TIMES : "*",
956 Binary_Operator.DIVIDE : "floor_div",
957 Binary_Operator.REMAINDER : "ada_remainder",
958 }[n_expr.operator]
960 sym_value = smt.Binary_Int_Arithmetic_Op(smt_op,
961 lhs_value,
962 rhs_value)
964 else:
965 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
966 if n_expr.operator == Binary_Operator.DIVIDE:
967 self.attach_real_division_check(rhs_value, n_expr)
969 smt_op = {
970 Binary_Operator.PLUS : "+",
971 Binary_Operator.MINUS : "-",
972 Binary_Operator.TIMES : "*",
973 Binary_Operator.DIVIDE : "/",
974 }[n_expr.operator]
976 sym_value = smt.Binary_Real_Arithmetic_Op(smt_op,
977 lhs_value,
978 rhs_value)
980 elif n_expr.operator in (Binary_Operator.COMP_LT,
981 Binary_Operator.COMP_LEQ,
982 Binary_Operator.COMP_GT,
983 Binary_Operator.COMP_GEQ):
984 smt_op = {
985 Binary_Operator.COMP_LT : "<",
986 Binary_Operator.COMP_LEQ : "<=",
987 Binary_Operator.COMP_GT : ">",
988 Binary_Operator.COMP_GEQ : ">=",
989 }[n_expr.operator]
991 sym_value = smt.Comparison(smt_op, lhs_value, rhs_value)
993 elif n_expr.operator in (Binary_Operator.STRING_CONTAINS,
994 Binary_Operator.STRING_STARTSWITH,
995 Binary_Operator.STRING_ENDSWITH):
997 smt_op = {
998 Binary_Operator.STRING_CONTAINS : "contains",
999 Binary_Operator.STRING_STARTSWITH : "prefixof",
1000 Binary_Operator.STRING_ENDSWITH : "suffixof"
1001 }
1003 # LHS / RHS ordering is not a mistake, in SMTLIB it's the
1004 # other way around than in TRLC.
1005 sym_value = smt.String_Predicate(smt_op[n_expr.operator],
1006 rhs_value,
1007 lhs_value)
1009 elif n_expr.operator == Binary_Operator.STRING_REGEX:
1010 rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None, None).value
1011 assert isinstance(rhs_evaluation, str)
1013 sym_value = smt.Function_Application(
1014 self.get_uf_matches(),
1015 lhs_value,
1016 smt.String_Literal(rhs_evaluation))
1018 elif n_expr.operator == Binary_Operator.INDEX:
1019 self.attach_index_check(lhs_value, rhs_value, n_expr)
1020 sym_value = smt.Sequence_Index(lhs_value, rhs_value)
1022 elif n_expr.operator == Binary_Operator.ARRAY_CONTAINS:
1023 sym_value = smt.Sequence_Contains(rhs_value, lhs_value)
1025 elif n_expr.operator == Binary_Operator.POWER:
1026 # LRM says that the exponent is always static and an
1027 # integer
1028 static_value = n_expr.n_rhs.evaluate(self.mh, None, None).value
1029 assert isinstance(static_value, int) and static_value >= 0
1031 if static_value == 0: 1031 ↛ 1032line 1031 didn't jump to line 1032 because the condition on line 1031 was never true
1032 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1033 sym_value = smt.Integer_Literal(1)
1034 else:
1035 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1036 sym_value = smt.Real_Literal(1)
1038 else:
1039 sym_value = lhs_value
1040 for _ in range(1, static_value):
1041 if isinstance(n_expr.n_lhs.typ, Builtin_Integer):
1042 sym_value = smt.Binary_Int_Arithmetic_Op("*",
1043 sym_value,
1044 lhs_value)
1045 else:
1046 assert isinstance(n_expr.n_lhs.typ, Builtin_Decimal)
1047 sym_value = smt.Binary_Real_Arithmetic_Op("*",
1048 sym_value,
1049 lhs_value)
1051 else: # pragma: no cover
1052 self.flag_unsupported(n_expr, n_expr.operator.name)
1054 return self.create_return(n_expr, sym_value)
1056 def tr_range_test(self, n_expr):
1057 assert isinstance(n_expr, Range_Test)
1059 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1060 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1061 lower_value, lower_valid = self.tr_expression(n_expr.n_lower)
1062 self.attach_validity_check(lower_valid, n_expr.n_lower)
1063 upper_value, upper_valid = self.tr_expression(n_expr.n_upper)
1064 self.attach_validity_check(upper_valid, n_expr.n_upper)
1066 sym_value = smt.Conjunction(
1067 smt.Comparison(">=", lhs_value, lower_value),
1068 smt.Comparison("<=", lhs_value, upper_value))
1070 return self.create_return(n_expr, sym_value)
1072 def tr_oneof_test(self, n_expr):
1073 assert isinstance(n_expr, OneOf_Expression)
1075 choices = []
1076 for n_choice in n_expr.choices:
1077 c_value, c_valid = self.tr_expression(n_choice)
1078 self.attach_validity_check(c_valid, n_choice)
1079 choices.append(c_value)
1081 negated_choices = [smt.Boolean_Negation(c)
1082 for c in choices]
1084 # pylint: disable=consider-using-enumerate
1086 if len(choices) == 1:
1087 result = choices[0]
1088 elif len(choices) == 2:
1089 result = smt.Exclusive_Disjunction(choices[0], choices[1])
1090 else:
1091 assert len(choices) >= 3
1092 values = []
1093 for choice_id in range(len(choices)):
1094 sequence = []
1095 for other_id in range(len(choices)):
1096 if other_id == choice_id:
1097 sequence.append(choices[other_id])
1098 else:
1099 sequence.append(negated_choices[other_id])
1100 values.append(smt.Conjunction(*sequence))
1101 result = smt.Disjunction(*values)
1103 return self.create_return(n_expr, result)
1105 def tr_conditional_expression_functional(self, n_expr):
1106 assert isinstance(n_expr, Conditional_Expression)
1108 s_result, _ = self.tr_expression(n_expr.else_expr)
1109 for n_action in reversed(n_expr.actions):
1110 s_condition, _ = self.tr_expression(n_action.n_cond)
1111 s_true, _ = self.tr_expression(n_action.n_expr)
1112 s_result = smt.Conditional(s_condition, s_true, s_result)
1114 return self.create_return(n_expr, s_result)
1116 def tr_conditional_expression(self, n_expr):
1117 assert isinstance(n_expr, Conditional_Expression)
1118 assert not self.functional
1120 gn_end = graph.Node(self.graph)
1121 sym_result = smt.Constant(self.tr_type(n_expr.typ),
1122 self.new_temp_name())
1124 for n_action in n_expr.actions:
1125 test_value, test_valid = self.tr_expression(n_action.n_cond)
1126 self.attach_validity_check(test_valid, n_action.n_cond)
1127 current_start = self.start
1129 # Create path where action is true
1130 self.attach_assumption(test_value)
1131 res_value, res_valid = self.tr_expression(n_action.n_expr)
1132 self.attach_validity_check(res_valid, n_action.n_expr)
1133 self.attach_temp_declaration(n_action,
1134 sym_result,
1135 res_value)
1136 self.start.add_edge_to(gn_end)
1138 # Reset to test and proceed with the other actions
1139 self.start = current_start
1140 self.attach_assumption(smt.Boolean_Negation(test_value))
1142 # Finally execute the else part
1143 res_value, res_valid = self.tr_expression(n_expr.else_expr)
1144 self.attach_validity_check(res_valid, n_expr.else_expr)
1145 self.attach_temp_declaration(n_expr,
1146 sym_result,
1147 res_value)
1148 self.start.add_edge_to(gn_end)
1150 # And join
1151 self.start = gn_end
1152 return sym_result, smt.Boolean_Literal(True)
1154 def tr_op_implication(self, n_expr):
1155 assert isinstance(n_expr, Binary_Expression)
1156 assert n_expr.operator == Binary_Operator.LOGICAL_IMPLIES
1158 if self.functional:
1159 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1160 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1161 return self.create_return(n_expr,
1162 smt.Implication(lhs_value, rhs_value))
1164 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1165 # Emit VC for validity
1166 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1168 # Split into two paths.
1169 current_start = self.start
1170 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1171 self.new_temp_name())
1172 gn_end = graph.Node(self.graph)
1174 ### 1: Implication is not valid
1175 self.start = current_start
1176 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1177 self.attach_temp_declaration(n_expr,
1178 sym_result,
1179 smt.Boolean_Literal(True))
1180 self.start.add_edge_to(gn_end)
1182 ### 2: Implication is valid.
1183 self.start = current_start
1184 self.attach_assumption(lhs_value)
1185 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1186 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1187 self.attach_temp_declaration(n_expr,
1188 sym_result,
1189 rhs_value)
1190 self.start.add_edge_to(gn_end)
1192 # Join paths
1193 self.start = gn_end
1195 return sym_result, smt.Boolean_Literal(True)
1197 def tr_op_and(self, n_expr):
1198 assert isinstance(n_expr, Binary_Expression)
1199 assert n_expr.operator == Binary_Operator.LOGICAL_AND
1201 if self.functional:
1202 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1203 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1204 return self.create_return(n_expr,
1205 smt.Conjunction(lhs_value, rhs_value))
1207 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1208 # Emit VC for validity
1209 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1211 # Split into two paths.
1212 current_start = self.start
1213 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1214 self.new_temp_name())
1215 gn_end = graph.Node(self.graph)
1217 ### 1: LHS is not true
1218 self.start = current_start
1219 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1220 self.attach_temp_declaration(n_expr,
1221 sym_result,
1222 smt.Boolean_Literal(False))
1223 self.start.add_edge_to(gn_end)
1225 ### 2: LHS is true
1226 self.start = current_start
1227 self.attach_assumption(lhs_value)
1228 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1229 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1230 self.attach_temp_declaration(n_expr,
1231 sym_result,
1232 rhs_value)
1233 self.start.add_edge_to(gn_end)
1235 # Join paths
1236 self.start = gn_end
1238 return sym_result, smt.Boolean_Literal(True)
1240 def tr_op_or(self, n_expr):
1241 assert isinstance(n_expr, Binary_Expression)
1242 assert n_expr.operator == Binary_Operator.LOGICAL_OR
1244 if self.functional: 1244 ↛ 1245line 1244 didn't jump to line 1245 because the condition on line 1244 was never true
1245 lhs_value, _ = self.tr_expression(n_expr.n_lhs)
1246 rhs_value, _ = self.tr_expression(n_expr.n_rhs)
1247 return self.create_return(n_expr,
1248 smt.Disjunction(lhs_value, rhs_value))
1250 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1251 # Emit VC for validity
1252 self.attach_validity_check(lhs_valid, n_expr.n_lhs)
1254 # Split into two paths.
1255 current_start = self.start
1256 sym_result = smt.Constant(smt.BUILTIN_BOOLEAN,
1257 self.new_temp_name())
1258 gn_end = graph.Node(self.graph)
1260 ### 1: LHS is true
1261 self.start = current_start
1262 self.attach_assumption(lhs_value)
1263 self.attach_temp_declaration(n_expr,
1264 sym_result,
1265 smt.Boolean_Literal(True))
1266 self.start.add_edge_to(gn_end)
1268 ### 2: LHS is not true
1269 self.start = current_start
1270 self.attach_assumption(smt.Boolean_Negation(lhs_value))
1271 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1272 self.attach_validity_check(rhs_valid, n_expr.n_rhs)
1273 self.attach_temp_declaration(n_expr,
1274 sym_result,
1275 rhs_value)
1276 self.start.add_edge_to(gn_end)
1278 # Join paths
1279 self.start = gn_end
1281 return sym_result, smt.Boolean_Literal(True)
1283 def tr_core_equality_tuple_component(self, n_component, lhs, rhs):
1284 assert isinstance(n_component, Composite_Component)
1285 assert isinstance(lhs, smt.Expression)
1286 assert isinstance(rhs, smt.Expression)
1288 value_lhs = smt.Record_Access(lhs,
1289 n_component.name + ".value")
1290 value_rhs = smt.Record_Access(rhs,
1291 n_component.name + ".value")
1292 valid_equal = self.tr_core_equality(n_component.n_typ,
1293 value_lhs,
1294 value_rhs)
1296 if not n_component.optional:
1297 return valid_equal
1299 valid_lhs = smt.Record_Access(lhs,
1300 n_component.name + ".valid")
1301 valid_rhs = smt.Record_Access(rhs,
1302 n_component.name + ".valid")
1304 return smt.Conjunction(
1305 smt.Comparison("=", valid_lhs, valid_rhs),
1306 smt.Implication(valid_lhs, valid_equal))
1308 def tr_core_equality(self, n_typ, lhs, rhs):
1309 assert isinstance(n_typ, Type)
1310 assert isinstance(lhs, smt.Expression)
1311 assert isinstance(rhs, smt.Expression)
1313 if isinstance(n_typ, Tuple_Type):
1314 parts = []
1315 for n_component in n_typ.all_components():
1316 parts.append(
1317 self.tr_core_equality_tuple_component(n_component,
1318 lhs,
1319 rhs))
1321 if len(parts) == 0: 1321 ↛ 1322line 1321 didn't jump to line 1322 because the condition on line 1321 was never true
1322 return smt.Boolean_Literal(True)
1323 elif len(parts) == 1: 1323 ↛ 1324line 1323 didn't jump to line 1324 because the condition on line 1323 was never true
1324 return parts[0]
1325 else:
1326 result = smt.Conjunction(parts[0], parts[1])
1327 for part in parts[2:]:
1328 result = smt.Conjunction(result, part)
1329 return result
1331 else:
1332 return smt.Comparison("=", lhs, rhs)
1334 def tr_op_equality(self, n_expr):
1335 assert isinstance(n_expr, Binary_Expression)
1336 assert n_expr.operator in (Binary_Operator.COMP_EQ,
1337 Binary_Operator.COMP_NEQ)
1339 lhs_value, lhs_valid = self.tr_expression(n_expr.n_lhs)
1340 rhs_value, rhs_valid = self.tr_expression(n_expr.n_rhs)
1342 if lhs_value is None:
1343 comp_typ = n_expr.n_rhs.typ
1344 else:
1345 comp_typ = n_expr.n_lhs.typ
1347 if lhs_valid.is_static_true() and rhs_valid.is_static_true():
1348 # Simplified form, this is just x == y
1349 result = self.tr_core_equality(comp_typ,
1350 lhs_value,
1351 rhs_value)
1353 elif lhs_valid.is_static_false() and rhs_valid.is_static_false():
1354 # This is null == null, so true
1355 result = smt.Boolean_Literal(True)
1357 elif lhs_value is None: 1357 ↛ 1359line 1357 didn't jump to line 1359 because the condition on line 1357 was never true
1358 # This is null == <expr>, true iff rhs is null
1359 result = smt.Boolean_Negation(rhs_valid)
1361 elif rhs_value is None:
1362 # This is <expr> == null, true iff lhs is null
1363 result = smt.Boolean_Negation(lhs_valid)
1365 else:
1366 # This is <expr> == <expr> without shortcuts
1367 result = smt.Conjunction(
1368 smt.Comparison("=", lhs_valid, rhs_valid),
1369 smt.Implication(lhs_valid,
1370 self.tr_core_equality(comp_typ,
1371 lhs_value,
1372 rhs_value)))
1374 if n_expr.operator == Binary_Operator.COMP_NEQ:
1375 result = smt.Boolean_Negation(result)
1377 return self.create_return(n_expr, result)
1379 def tr_quantified_expression(self, n_expr):
1380 assert isinstance(n_expr, Quantified_Expression)
1382 # Nested quantifiers are not supported yet
1383 if self.functional: # pragma: no cover
1384 self.flag_unsupported(n_expr,
1385 "functional evaluation of quantifier")
1387 # TRLC quantifier
1388 # (forall x in arr_name => body)
1389 #
1390 # SMT quantifier
1391 # (forall ((i Int))
1392 # (=> (and (>= i 0) (< i (seq.len arr_name)))
1393 # (... (seq.nth arr_name i) ... )))
1394 #
1395 # There is an alternative which is:
1396 # (forall ((element ElementSort))
1397 # (=> (seq.contains arr_name (seq.unit element))
1398 # (... element ...)
1399 #
1400 # However it looks like for CVC5 at least this generates more
1401 # unknown and less unsat if a check depends on the explicit
1402 # value of some sequence member.
1404 # Evaluate subject first and creat a null check
1405 s_subject_value, s_subject_valid = \
1406 self.tr_name_reference(n_expr.n_source)
1407 self.attach_validity_check(s_subject_valid, n_expr.n_source)
1409 # Create validity checks for the body. We do this by creating
1410 # a new branch and eliminating the quantifier; pretending it's
1411 # a forall (since we want to show that for all evaluations
1412 # it's valid).
1413 current_start = self.start
1414 self.attach_empty_assumption()
1415 src_typ = n_expr.n_source.typ
1416 assert isinstance(src_typ, Array_Type)
1417 s_qe_index = smt.Constant(smt.BUILTIN_INTEGER,
1418 self.new_temp_name())
1419 self.start.add_statement(
1420 smt.Constant_Declaration(
1421 symbol = s_qe_index,
1422 comment = ("quantifier elimination (index) for %s at %s" %
1423 (n_expr.to_string(),
1424 n_expr.location.to_string()))))
1425 self.start.add_statement(
1426 smt.Assertion(smt.Comparison(">=",
1427 s_qe_index,
1428 smt.Integer_Literal(0))))
1429 self.start.add_statement(
1430 smt.Assertion(
1431 smt.Comparison("<",
1432 s_qe_index,
1433 smt.Sequence_Length(s_subject_value))))
1434 s_qe_sym = smt.Constant(self.tr_type(src_typ.element_type),
1435 self.new_temp_name())
1436 self.start.add_statement(
1437 smt.Constant_Declaration(
1438 symbol = s_qe_sym,
1439 value = smt.Sequence_Index(s_subject_value, s_qe_index),
1440 comment = ("quantifier elimination (symbol) for %s at %s" %
1441 (n_expr.to_string(),
1442 n_expr.location.to_string()))))
1443 self.qe_vars[n_expr.n_var] = s_qe_sym
1445 _, b_valid = self.tr_expression(n_expr.n_expr)
1446 self.attach_validity_check(b_valid, n_expr.n_expr)
1448 self.start = current_start
1449 del self.qe_vars[n_expr.n_var]
1451 # We have now shown that any path in the quantifier cannot
1452 # raise exception. Asserting the actual value of the
1453 # quantifier is more awkward.
1455 s_q_idx = smt.Bound_Variable(smt.BUILTIN_INTEGER,
1456 self.new_temp_name())
1457 s_q_sym = smt.Sequence_Index(s_subject_value, s_q_idx)
1458 self.bound_vars[n_expr.n_var] = s_q_sym
1460 temp, self.functional = self.functional, True
1461 b_value, _ = self.tr_expression(n_expr.n_expr)
1462 self.functional = temp
1464 bounds_expr = smt.Conjunction(
1465 smt.Comparison(">=",
1466 s_q_idx,
1467 smt.Integer_Literal(0)),
1468 smt.Comparison("<",
1469 s_q_idx,
1470 smt.Sequence_Length(s_subject_value)))
1471 if n_expr.universal:
1472 value = smt.Quantifier(
1473 "forall",
1474 [s_q_idx],
1475 smt.Implication(bounds_expr, b_value))
1476 else:
1477 value = smt.Quantifier(
1478 "exists",
1479 [s_q_idx],
1480 smt.Conjunction(bounds_expr, b_value))
1482 return value, smt.Boolean_Literal(True)
1484 def _ensure_record_deref(self, type_key, sort_name, uf_name,
1485 components):
1486 """Lazily create an SMT record sort and uninterpreted function
1487 for dereferencing integer-encoded references.
1489 :param type_key: cache key; always the canonical sort_name string
1490 :param sort_name: name for the SMT Record sort
1491 :param uf_name: name for the UF mapping integer to sort
1492 :param components: iterable of (field_name, smt_sort, needs_valid)
1493 :returns: (record_sort, to_record_uf)
1494 """
1495 if type_key in self.records:
1496 return self.records[type_key], self.uf_records[type_key]
1498 record_sort = smt.Record(sort_name)
1499 for field_name, field_sort, needs_valid in components:
1500 record_sort.add_component(field_name + ".value", field_sort)
1501 if needs_valid:
1502 record_sort.add_component(field_name + ".valid",
1503 smt.BUILTIN_BOOLEAN)
1504 self.records[type_key] = record_sort
1505 self.preamble.add_statement(
1506 smt.Record_Declaration(
1507 record_sort,
1508 sort_name))
1510 to_record_uf = smt.Function(
1511 uf_name, record_sort,
1512 smt.Bound_Variable(smt.BUILTIN_INTEGER, "ref"))
1513 self.preamble.add_statement(
1514 smt.Function_Declaration(to_record_uf))
1515 self.uf_records[type_key] = to_record_uf
1517 return record_sort, to_record_uf
1519 def tr_field_access_expression(self, n_expr):
1520 assert isinstance(n_expr, Field_Access_Expression)
1522 prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix)
1523 prefix_typ = n_expr.n_prefix.typ
1524 if not self.functional:
1525 self.attach_validity_check(prefix_valid, n_expr.n_prefix)
1527 if isinstance(prefix_typ, Tuple_Type):
1528 field_value = smt.Record_Access(prefix_value,
1529 n_expr.n_field.name + ".value")
1530 if n_expr.n_field.optional:
1531 field_valid = smt.Record_Access(prefix_value,
1532 n_expr.n_field.name + ".valid")
1533 else:
1534 field_valid = smt.Boolean_Literal(True)
1536 elif isinstance(prefix_typ, (Record_Type, Union_Type)):
1537 # lobster-trace: LRM.Union_Type_Field_Access
1538 # lobster-trace: LRM.Union_Type_Partial_Field_Access
1539 # lobster-trace: LRM.Union_Type_Partial_Field_Null
1540 # Both Record_Type and Union_Type are represented as
1541 # integers. We create a record sort with accessible
1542 # fields and a UF to dereference the integer.
1543 if isinstance(prefix_typ, Record_Type):
1544 components = [
1545 (c.name, self.tr_type(c.n_typ), c.optional)
1546 for c in prefix_typ.all_components()
1547 ]
1548 sort_name = "%s.%s" % (prefix_typ.n_package.name,
1549 prefix_typ.name)
1550 uf_name = "access.%s.%s" % (prefix_typ.n_package.name,
1551 prefix_typ.name)
1552 else:
1553 field_map = prefix_typ.get_field_map()
1554 union_id = "_".join(t.fully_qualified_name()
1555 for t in prefix_typ.types)
1556 components = [
1557 (name,
1558 self.tr_type(info["n_typ"]),
1559 info["count"] != info["total"] or
1560 info["optional_in_any"])
1561 for name, info in field_map.items()
1562 if info["n_typ"] is not None
1563 ]
1564 sort_name = "union." + union_id
1565 uf_name = "access.union." + union_id
1567 _, to_record_uf = self._ensure_record_deref(
1568 sort_name, sort_name, uf_name, components)
1569 dereference = smt.Function_Application(to_record_uf,
1570 prefix_value)
1572 # Perform the field access on the dereferenced record
1573 field_value = smt.Record_Access(dereference,
1574 n_expr.n_field.name + ".value")
1575 if isinstance(prefix_typ, Union_Type):
1576 info = prefix_typ.get_field_map()[n_expr.n_field.name]
1577 has_valid = (info["count"] != info["total"] or
1578 info["optional_in_any"])
1579 else:
1580 has_valid = n_expr.n_field.optional
1582 if has_valid:
1583 field_valid = smt.Record_Access(
1584 dereference,
1585 n_expr.n_field.name + ".valid")
1586 else:
1587 field_valid = smt.Boolean_Literal(True)
1589 else:
1590 self.mh.ice_loc(n_expr.n_prefix.location,
1591 "unexpected type %s as prefix of field access" %
1592 n_expr.n_prefix.typ.__class__.__name__)
1594 # pylint: disable=possibly-used-before-assignment
1595 return field_value, field_valid