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