some small changes to Legion + SV

Legion.py

@@ -192,6 +192,8 @@ def best_child(self) -> 'TreeNode':
  Select the child of the highest uct score, break tie uniformly
  :return: a tree node
  """
+
+ LOGGER.info("Selecting from children: {}".format(self.children))
  # TODO: more elegant method, if time permitted
  max_score, candidates = -inf, [] # type: float, List[TreeNode]
  for child in self.children.values():
@@ -204,7 +206,7 @@ def best_child(self) -> 'TreeNode':
  candidates = [child]
 
  # TODO: choose one from candidates uniformly
- return candidates[int(random.uniform(0, len(candidates) - 1))]
+ return random.choice(candidates)
 
  def is_root(self) -> bool:
  """
@@ -275,7 +277,7 @@ def byte_len() -> int:
  target = self.state.posix.stdin.load(0, self.state.posix.stdin.size)
 
  if not self.samples:
- self.samples = self.state.solver.iterate(e=target)
+ self.samples = self.state.solver.batch_iterate(target)
 
  results = []
  while len(results) < MAX_SAMPLES:

Makefile

@@ -68,5 +68,13 @@ uninstall:
  rm $(PREFIX)/bin/trace/as
  rmdir $(PREFIX)/bin/trace
 
+LOGS = $(wildcard test/results/legion.*.logfiles/*.files)
+ZIPS = $(addsuffix /test-suite.zip,$(LOGS))
 
+.PHONY: zips
+
+%/test-suite.zip: %/Principes
+ zip $@ $^ -r
+
+zips: $(ZIPS)
 

__VERIFIER.c

@@ -7,17 +7,52 @@ void __VERIFIER_error() {
  exit(100);
 }
 
+_Bool __VERIFIER_nondet_bool() {
+ _Bool x = 0;
+ read(0, &x, sizeof(x));
+ printf(" <input type=\"bool\">%d</input>\n", x);
+ return x;
+}
+
+char __VERIFIER_nondet_char() {
+ char x = 0;
+ read(0, &x, sizeof(x));
+ printf(" <input type=\"char\">%d</input>\n", x);
+ return x;
+}
+
+unsigned char __VERIFIER_nondet_uchar() {
+ unsigned char x = 0;
+ read(0, &x, sizeof(x));
+ printf(" <input type=\"unsigned char\">%d</input>\n", x);
+ return x;
+}
+
+short __VERIFIER_nondet_short() {
+ short x = 0;
+ read(0, &x, sizeof(x));
+ printf(" <input type=\"short\">%d</input>\n", x);
+ return x;
+}
+
+unsigned short __VERIFIER_nondet_ushort() {
+ unsigned short x = 0;
+ read(0, &x, sizeof(x));
+ printf(" <input type=\"unsigned short\">%d</input>\n", x);
+ return x;
+}
+
 int __VERIFIER_nondet_int() {
  int x = 0;
  read(0, &x, sizeof(x));
  printf(" <input type=\"int\">%d</input>\n", x);
  return x;
 }
 
-short __VERIFIER_nondet_short() {
- short x = 0;
+unsigned __VERIFIER_nondet_unsigned() {
+ unsigned x = 0;
  read(0, &x, sizeof(x));
- printf(" <input type=\"short\">%hd</input>\n", x);
+ printf(" <input type=\"unsigned\">%d</input>\n", x);
  return x;
 }
 
@@ -35,10 +70,10 @@ float __VERIFIER_nondet_float() {
  return x;
 }
 
-char __VERIFIER_nondet_char() {
- char x = 0;
+float __VERIFIER_nondet_double() {
+ double x = 0.0;
  read(0, &x, sizeof(x));
- printf(" <input type=\"char\">%hhd</input>\n", x);
+ printf(" <input type=\"double\">%f</input>\n", x);
  return x;
 }
 

tbf.xml

@@ -0,0 +1,64 @@
+<?xml version="1.0"?>
+<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-1.9.dtd">
+<benchmark tool="tbf_testsuite_validator" displayName="TBF Test-Suite Validator" timelimit="15 min" memlimit="7 GB" cpuCores="1">
+
+ <require cpuModel="Intel" cpuCores="2"/>
+
+ <resultfiles>**test-suite/*</resultfiles>
+
+ <columns>
+ <column title="lines_covered">Lines covered</column>
+ <column title="branches_covered">Branches covered</column>
+ </columns>
+
+ <option name="--verbose" />
+ <option name="--sequence-file">cov-seq.txt</option>
+ <option name="-r" />
+
+ <rundefinition name="test-comp19_prop-coverage-error-call">
+ <option name="--stop-after-found-violation" />
+
+ <requiredfiles>test/results/legion.2019-08-21_1207.logfiles/${rundefinition_name}.${taskdef_name}.files/test-suite.zip</requiredfiles>
+ <option name="--test-suite">test/results/legion.2019-08-21_1207.logfiles/${rundefinition_name}.${taskdef_name}.files/test-suite.zip</option>
+ <propertyfile>../sv-benchmarks/c/properties/coverage-error-call.prp</propertyfile>
+ </rundefinition>
+
+<!--
+ <rundefinition name="test-comp19_prop-coverage-branches">
+ <requiredfiles>test/results/legion.2019-08-21_1207.logfiles/${rundefinition_name}.${taskdef_name}.files/test-suite.zip</requiredfiles>
+ <option name="-test-suite">test/results/legion.2019-08-21_1207.logfiles/${rundefinition_name}.${taskdef_name}.yml.files/test-suite.zip</option>
+ <propertyfile>../sv-benchmarks/c/properties/coverage-branches.prp</propertyfile>
+ </rundefinition>
+-->
+
+
+ <tasks name="ReachSafety-Arrays">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Arrays.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-BitVectors">
+ <includesfile>../sv-benchmarks/c/ReachSafety-BitVectors.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-ControlFlow">
+ <includesfile>../sv-benchmarks/c/ReachSafety-ControlFlow.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-ECA">
+ <includesfile>../sv-benchmarks/c/ReachSafety-ECA.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-Floats">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Floats.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-Heap">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Heap.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-Loops">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Loops.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-Recursive">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Recursive.set</includesfile>
+ </tasks>
+ <tasks name="ReachSafety-Sequentialized">
+ <includesfile>../sv-benchmarks/c/ReachSafety-Sequentialized.set</includesfile>
+ </tasks>
+
+</benchmark>
+

validate

@@ -0,0 +1,4 @@
+#!/bin/sh
+
+make zips
+/home/ernst/workspace/cpachecker/scripts/benchmark.py --read-only-dir / --cloud --cloudMaster localhost tbf.xml