Generate witnesses in version 2.1

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:

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
 

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,

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:

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();

transforms/InstrumentNontermination.cpp

@@ -260,10 +260,10 @@ bool InstrumentNontermination::instrumentLoop(Loop *L, const std::set<llvm::Valu
 
     if (insertHeader) {
         auto *CI = CallInst::Create(getHeaderFun(M));
-        // copy the location from terminator, so that we have
+        // copy the location from the instruction so that we have
         // the right debug loc
-        CloneMetadata(header->getTerminator(), CI);
-        CI->insertBefore(header->getTerminator());
+        CloneMetadata(where, CI);
+        CI->insertBefore(where);
     }
   }