diff --git a/klee b/klee index b24c1608..77fff2ca 160000 --- a/klee +++ b/klee @@ -1 +1 @@ -Subproject commit b24c1608db8626b2b2a7095e12065e0cfda7b29b +Subproject commit 77fff2ca53b8e67ef6ffaafbbb07e1d32821a55a diff --git a/lib/symbioticpy/symbiotic/targets/klee.py b/lib/symbioticpy/symbiotic/targets/klee.py index fb6e56be..d19638b5 100644 --- a/lib/symbioticpy/symbiotic/targets/klee.py +++ b/lib/symbioticpy/symbiotic/targets/klee.py @@ -363,7 +363,9 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}): cmd.append('-write-witness') if opts.property.memsafety() or \ opts.property.unreachcall() or \ - opts.property.signedoverflow(): + opts.property.assertions() or \ + opts.property.signedoverflow() or \ + opts.property.termination(): cmd.append('-write-waypoints') if opts.executable_witness: diff --git a/lib/symbioticpy/symbiotic/targets/kleebase.py b/lib/symbioticpy/symbiotic/targets/kleebase.py index d196d498..b1b8bc5a 100644 --- a/lib/symbioticpy/symbiotic/targets/kleebase.py +++ b/lib/symbioticpy/symbiotic/targets/kleebase.py @@ -227,8 +227,8 @@ def generate_graphml(path, source, is_correctness_wit, opts, saveto): def generate_yaml(path, source, is_correctness_wit, opts, saveto): assert saveto is not None - gen = YAMLWriter(source, opts.property.ltl(), - opts.is32bit, is_correctness_wit) + gen = YAMLWriter(source, opts.property, + opts.is32bit, is_correctness_wit, saveto) if not is_correctness_wit: gen.generate_violation_witness(path) else: @@ -267,10 +267,11 @@ def generate_yaml_witness(bindir, sources, is_correctness_wit, opts, saveto): generate_yaml(None, sources[0], is_correctness_wit, opts, saveto) return - yaml_support = opts.property.signedoverflow() or opts.property.unreachcall() or \ - opts.property.assertions() - - if not yaml_support: + if not opts.property.memsafety() and \ + not opts.property.unreachcall() and \ + not opts.property.assertions() and \ + not opts.property.signedoverflow() and \ + not opts.property.termination(): print('Failed generating YAML witness: Property not supported by format') return diff --git a/lib/symbioticpy/symbiotic/targets/slowbeast.py b/lib/symbioticpy/symbiotic/targets/slowbeast.py index 6c95887c..06cf865c 100644 --- a/lib/symbioticpy/symbiotic/targets/slowbeast.py +++ b/lib/symbioticpy/symbiotic/targets/slowbeast.py @@ -3,6 +3,7 @@ from shutil import copy as copyfile from symbiotic.utils.utils import dbg, print_stdout from symbiotic.witnesses.witnesses import GraphMLWriter +from symbiotic.witnesses.YAMLwitnesswriter import YAMLWriter from . tool import SymbioticBaseTool try: @@ -93,6 +94,19 @@ def passes_before_verification(self): return passes + ["-O3", "-remove-constant-exprs", "-reg2mem"] def generate_witness(self, llvmfile, sources, has_error): + assert len(sources) == 1 + + # Generate trivial YAML correctness witness + if self._options.witness_output and not has_error: + print_stdout('Generating trivial correctness witness: {0}' + .format(self._options.witness_output)) + gen = YAMLWriter(sources[0], self._options.property, + self._options.is32bit, not has_error, + self._options.witness_output) + + gen.generate_correctness_witness() + gen.write(self._options.witness_output) + if not self._options.graphml_witness_output: return @@ -104,7 +118,6 @@ def generate_witness(self, llvmfile, sources, has_error): witnesses = [abspath(pathjoin(sbdir, f)) for f in listdir(sbdir) if f.endswith('.graphml')] - assert len(sources) == 1 gen = GraphMLWriter(sources[0], self._options.property.ltl(), self._options.is32bit, diff --git a/lib/symbioticpy/symbiotic/witnesses/YAMLwitnesswriter.py b/lib/symbioticpy/symbiotic/witnesses/YAMLwitnesswriter.py index 6c63e157..91d8c23c 100644 --- a/lib/symbioticpy/symbiotic/witnesses/YAMLwitnesswriter.py +++ b/lib/symbioticpy/symbiotic/witnesses/YAMLwitnesswriter.py @@ -2,11 +2,12 @@ import clang.cindex from hashlib import sha256 as hashfunc +from os.path import relpath, dirname import datetime import yaml import sys -from .. utils.utils import print_stderr import uuid +from .. utils.utils import print_stderr from ..options import get_versions def get_hash(source): @@ -19,8 +20,9 @@ def get_hash(source): return hsh.hexdigest() class YAMLWriter(object): - def __init__(self, source, prps, is32bit, is_correctness_wit): + def __init__(self, source, prps, is32bit, is_correctness_wit, saveto): self._source = source + self._relsource = relpath(source, dirname(saveto)) self._prps = prps self._is32bit = is32bit self._correctness_wit = is_correctness_wit @@ -35,15 +37,15 @@ def add_metadata(self): witness = {} witness['entry_type'] = "violation_sequence" if not self._correctness_wit else "invariant_set" witness['metadata'] = { - 'format_version' : "2.0", + 'format_version' : "2.1", 'creation_time' : '{date:%Y-%m-%dT%T}Z'.format(date=datetime.datetime.utcnow()), 'producer' : {'name' : 'symbiotic', 'version' : get_versions()[0] }, 'uuid' : str(uuid.uuid4()), 'task' : - { 'input_files' : [self._source], - 'input_file_hashes' : { self._source : get_hash(self._source)}, - 'specification' : ','.join(self._prps), + { 'input_files' : [self._relsource], + 'input_file_hashes' : { self._relsource : get_hash(self._source)}, + 'specification' : ','.join(self._prps.ltl()), 'data_model' : "ILP32" if self._is32bit else "LP64", 'language' : "C"} } @@ -59,7 +61,7 @@ def generate_violation_witness(self, path): """ self.parse(path) - assert self.errorLoc, "Failed generating a YAML witness" + assert self.errorLoc or self._prps.termination(), "Failed generating a YAML witness" self.add_metadata() self.create_content() @@ -82,7 +84,10 @@ def write(self, to): # Traverse the AST, find the right brackets of functions and the full expression of the target def traverse_AST(self, node): - # Recurse for children of this node + + # get infinitely recurring location + if self._prps.termination() and self.errorLoc and not self.errorExpr: + self.errorExpr = _get_recurring_location(node, self.errorLoc) for child in node.get_children(): @@ -95,7 +100,7 @@ def traverse_AST(self, node): if child.kind == clang.cindex.CursorKind.CALL_EXPR and (start.line, start.column) in self.calls: self.calls[(start.line, start.column)] = end.line, end.column - 1 - if self.errorExpr or not child.kind.is_expression(): + if self.errorExpr or not self.errorLoc or not child.kind.is_expression(): self.traverse_AST(child) continue @@ -118,8 +123,9 @@ def create_content(self): root = tu.cursor self.traverse_AST(root) - if not self.errorExpr: + if self.errorLoc and not self.errorExpr: print_stderr("Warning: Could not get target location for witness") + self.errorExpr = self.errorLoc content = [] @@ -129,13 +135,13 @@ def create_content(self): segment = [] waypoint = { 'type' : 'function_return', - 'action' : 'follow', + 'action' : 'cycle' if call[3] else 'follow', 'constraint' : { - 'format' : 'c_expression', + 'format' : 'ext_c_expression', 'value' : '\\result == ' + call[2] }, 'location' : { - 'file_name' : self._source, + 'file_name' : self._relsource, 'line' : new_location[0], 'column' : new_location[1] } @@ -144,36 +150,99 @@ def create_content(self): segment.append({'waypoint' : waypoint}) content.append({'segment' : segment}) - target_segment = [] - target = { 'type' : 'target', - 'action' : 'follow', - 'location' : { - 'file_name' : self._source, + if self.errorLoc: + last_segment = [] + location = { 'file_name' : self._relsource, 'line' : self.errorExpr[0], 'column' : self.errorExpr[1] + } + + if self._prps.termination(): + last = { 'type' : 'assumption', + 'action' : 'cycle', + 'location' : location, + 'constraint' : { + 'format' : 'c_expression', + 'value' : '1' } + } + else: + last = { 'type' : 'target', + 'action' : 'follow', + 'location' : location + } - } - target_segment.append({'waypoint' : target}) - content.append({'segment' : target_segment}) + last_segment.append({'waypoint' : last}) + content.append({'segment' : last_segment}) self.witness[0]['content'] = content def parse(self, path): with open(path, "r") as testfile: + cycle = False for line in testfile.readlines(): if line[0] == '@': - self.errorLoc = list(map(int, line.strip('\n').split(':')[2:])) + self.errorLoc = tuple(map(int, line.strip('\n').split(':')[2:])) break call = line.strip('\n').split(':') line = int(call[1]) col = int(call[2]) value = call[3] - self.test.append((line, col, value)) + cycle = (len(call) == 5) # is there the cycle flag? + self.test.append((line, col, value, cycle)) self.calls[(line, col)] = None + # No need for this if we have cycle waypoints + if cycle: + self.errorLoc = None + + +def _get_recurring_location(node, error_loc): + n_start = node.extent.start + n_end = node.extent.end + children = list(node.get_children()) + + recurring_node = None + + if (node.kind == clang.cindex.CursorKind.FOR_STMT or \ + node.kind == clang.cindex.CursorKind.WHILE_STMT): + + if (error_loc[0] == n_start.line and error_loc[1] == n_start.column) or \ + location_in_range(error_loc[0], error_loc[1], + children[0].extent.start.line, children[0].extent.start.column, + children[-2].extent.end.line, children[-2].extent.end.column): + return children[-1].extent.start.line, children[-1].extent.start.column + + if node.kind == clang.cindex.CursorKind.DO_STMT: + + if (error_loc[0] == children[0].extent.end.line and \ + error_loc[1] == children[0].extent.end.column - 1) or \ + location_in_range(error_loc[0], error_loc[1], + children[1].extent.start.line, children[1].extent.start.column, + children[1].extent.end.line, children[1].extent.end.column): + return children[0].extent.start.line, children[0].extent.start.column + + if node.kind == clang.cindex.CursorKind.IF_STMT: + + if (error_loc[0] == children[0].extent.start.line and \ + error_loc[1] == children[0].extent.start.column) or \ + location_in_range(error_loc[0], error_loc[1], + children[0].extent.start.line, children[0].extent.start.column, + children[0].extent.end.line, children[0].extent.end.column): + return n_start.line, n_start.column + + if node.kind == clang.cindex.CursorKind.SWITCH_STMT and \ + error_loc[0] == n_start.line and \ + error_loc[1] == n_start.column: + return n_start.line, n_start.column + + if (node.kind.is_statement() or node.kind.is_declaration()) and \ + error_loc[0] == n_start.line and \ + error_loc[1] == n_start.column: + return n_start.line, n_start.column + def location_in_range(line, col, startline, startcol, endline, endcol): if startline > line or endline < line: diff --git a/transforms/BreakInfiniteLoops.cpp b/transforms/BreakInfiniteLoops.cpp index bcaee5fa..35683195 100644 --- a/transforms/BreakInfiniteLoops.cpp +++ b/transforms/BreakInfiniteLoops.cpp @@ -95,6 +95,9 @@ class BreakInfiniteLoops : public LoopPass { BasicBlock *exitBB = getExitBB(header->getParent()); BasicBlock *nb = BasicBlock::Create(Ctx, "break.inf.loop"); + // insert the new block before header + nb->insertInto(header->getParent(), header); + GlobalVariable * gv = getConstantTrueGV(*M); LoadInst *LI = new LoadInst( gv->getType()->getPointerElementType(), @@ -113,9 +116,6 @@ class BreakInfiniteLoops : public LoopPass { << *Br << "\n"; } - // insert the new block before header - nb->insertInto(header->getParent(), header); - // now change the jump instructions for (auto& pr : to_change) { auto TI = pr.first->getTerminator(); diff --git a/transforms/InstrumentNontermination.cpp b/transforms/InstrumentNontermination.cpp index c61b0fce..9e686b67 100644 --- a/transforms/InstrumentNontermination.cpp +++ b/transforms/InstrumentNontermination.cpp @@ -260,10 +260,10 @@ bool InstrumentNontermination::instrumentLoop(Loop *L, const std::setgetTerminator(), CI); - CI->insertBefore(header->getTerminator()); + CloneMetadata(where, CI); + CI->insertBefore(where); } }