Merge branch 'release-1.0'

Makefile

@@ -36,6 +36,7 @@ OBJ=\
 	src/args/performance_term.o \
 	src/args/strategy.o \
 	src/args/testcases.o \
+	src/args/timeout.o \
 	src/args/tunit.o \
 	\
 	src/cfg/cfg.o \

README.md

@@ -260,7 +260,7 @@ where `search.conf` contains:
 
 --testcases popcnt.tc # Path to testcase file
 --training_set "{ 0 ... 7 }" # Testcases to use for measuring correctness during search
---test_set "{ 0 ... 1023 }"  # Testcases to use as holdout set for checking correctness
+--test_set "{ 8 ... 1023 }"  # Testcases to use as holdout set for checking correctness
 
 --distance hamming # Metric for measuring error between live-outs
 --relax_reg # Allow partial credit for results that appear in wrong locations
@@ -287,17 +287,18 @@ where `search.conf` contains:
 
 --statistics_interval 100000 # Print statistics every 100k proposals
 --timeout 1000000 # Propose 1m modifications before giving up
---verification_cycles 16 # Attempt to verify 16 zero cost rewrites before giving up
+--timeout_action testcase # Try adding a new testcase from the testset when search times out
+--timeout_cycles 16 # Timeout up to 16 times before giving up
 
 --strategy hold_out # Verify results using a larger hold out testcase set
 ```
 
-STOKE search will produce two types of status messages. Progress update messages will be printed whenever STOKE discovers a new lowest cost verified or unverified rewrite. The code shown on the left is not equivalent to the target code; the code shown on the right is.
+STOKE search will produce two types of status messages. Progress update messages will be printed whenever STOKE discovers a new lowest cost verified or unverified rewrite. The code shown on the left is not equivalent to the target code; the code shown on the right is with respect to the current set of testcases.
 
 ```
 Progress Update: 
 
-Best Unverified (9)                Best Verified (15)     
+Lowest Cost Discovered (9)         Lowest Known Correct Cost (15)     
                                                          
 btrq $0xffffffffffffffc0, %rdi     testq %rdi, %rdi      
 retq                               je .L_X64ASM_0        
@@ -546,20 +547,7 @@ Cost CostFunction::extension_correctness(const Cfg& cfg, Cost max) {
   // that compute res iteratively may stop executing and return max once res                                     
   // equals or exceeds that value.                                                                               
 
-  // This method should set the testcases_evaluated_ attribute to reflect the                                    
-  // number of testcases that were examined prior to a possible early exit. The                                  
-  // final testcase that was used (testcases_evaluted_-1) is returned by a hold_out                              
-  // verifier as a counter-example following a failed proof of correctness (a hold-out
-  // verifier uses a max cost of 0; for non-zero results, the evaluation of this testcase 
-  // is presumably responsible for res exceeding max).
-
-  testcases_evaluated_ = 1;
-
-  // Invariant 1: 0 < testcases_evaluated_ < sandbox_->size()                                                    
-  assert(testcases_evaluated_ > 0);                                                                              
-  assert(testcases_evaluated_ < sandbox_->size());                                                               
-
-  // Invariant 2: Return value should not exceed max_correctness_cost                                            
+  // Invariant 1: Return value should not exceed max_correctness_cost                                            
   assert(res <= max_correctness_cost);                                                                           
 
   return res;                                                                                                    
@@ -614,11 +602,18 @@ Strategy type is specified using the `--strategy` command line argument. This va
 
 ```c++
 bool Verifier::extension_verify(const Cfg& target, const Cfg& rewrite) {                                         
-  // Add user-defined implementation here ...
+	// Add user-defined implementation here ...
+
+	// Invariant 1. If this method returns false and is able to produce a 
+	// counter example explaining why, counter_example_available_ should be
+	// set to true.
+
+	// Invariant 2. If this method returns false, and it is able (see above), 
+	// counter_example_ should be set to a CpuState that will cause target and 
+	// rewrite to produce different values.
 
-  // Invariant 1. If this method returns false, counter_example_ should be                                       
-  // set to a CpuState that will cause target and rewrite to produce different                                   
-  // values.                                                                                                     
+	// Invariant 3. If this method produces a counter example, it should be
+	// unique relative to all previously produced counter examples.
 
   return true;
 } 

examples/bansal/optimization.conf

@@ -15,9 +15,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases ./bansal.tc
 --training_set "{ 0 ... 15 }"
+--test_set "{ 16 ... 1023 }"
 
 ##### Correctness options:
 
@@ -59,7 +59,8 @@
 --max_instrs 32
 --statistics_interval 10000000
 --timeout 100000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 16
 
 ##### Verification options:
 

examples/libimf/log/optimization.conf

@@ -13,9 +13,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases log.tc
 --training_set "{ 0 ... 255 }"
+--test_set "{ 256 ... 1023 }"
 
 ##### Correctness options:
 
@@ -53,7 +53,8 @@
 --max_instrs 80
 --statistics_interval 1000000
 --timeout 10000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 16
 
 ##### Verification options:
 

examples/libimf/sin/optimization.conf

@@ -13,9 +13,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases sin.tc
 --training_set "{ 0 ... 255 }"
+--test_set "{ 256 ... 1023 }"
 
 ##### Correctness options:
 
@@ -53,7 +53,8 @@
 --max_instrs 80
 --statistics_interval 1000000
 --timeout 10000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 16
 
 ##### Verification options:
 

examples/libimf/tan/optimization.conf

@@ -13,9 +13,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases tan.tc
 --training_set "{ 0 ... 255 }"
+--test_set "{ 256 ... 1023 }"
 
 ##### Correctness options:
 
@@ -53,7 +53,8 @@
 --max_instrs 120
 --statistics_interval 1000000
 --timeout 10000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 32
 
 ##### Verification options:
 

examples/mont_mul/optimization.conf

@@ -12,9 +12,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases mont_mul.tc
 --training_set "{ 0 ... 31 }"
+--test_set "{ 32 ... 1023 }"
 
 ##### Correctness options:
 
@@ -49,7 +49,8 @@
 --max_instrs 32
 --statistics_interval 10000000
 --timeout 100000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 16
 
 ##### Verification options:
 

examples/mont_mul/synthesis.conf

@@ -10,9 +10,9 @@
 
 ##### Testcase options:
 
---test_set "{ 0 ... 1023 }"
 --testcases mont_mul.tc
---training_set "{ 0 ... 32 }"
+--training_set "{ 0 ... 31 }"
+--test_set "{ 32 ... 1023 }"
 
 ##### Correctness options:
 
@@ -47,7 +47,8 @@
 --max_instrs 32
 --statistics_interval 10000000
 --timeout 100000000
---verification_cycles 32
+--timeout_action testcase
+--timeout_cycles 16
 
 ##### Verification options:
 

examples/tutorial/search.conf

@@ -10,7 +10,7 @@
 
 --testcases popcnt.tc # Path to testcase file
 --training_set "{ 0 ... 7 }" # Testcases to use for measuring correctness during search
---test_set "{ 0 ... 1023 }"  # Testcases to use as holdout set for checking correctness
+--test_set "{ 8 ... 1023 }"  # Testcases to use as holdout set for checking correctness
 
 --distance hamming # Metric for measuring error between live-outs
 --relax_reg # Allow partial credit for results that appear in wrong locations
@@ -37,6 +37,7 @@
 
 --statistics_interval 100000 # Print statistics every 100k proposals
 --timeout 1000000 # Propose 1m modifications before giving up
---verification_cycles 16 # Attempt to verify 16 zero cost rewrites before giving up
+--timeout_action testcase # Try adding a new testcase from the testset when search times out
+--timeout_cycles 16 # Timeout up to 16 times before giving up
 
 --strategy hold_out # Verify results using a larger hold out testcase set

src/args/timeout.cc

@@ -0,0 +1,52 @@
+// Copyright 2014 eric schkufza
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include <array>
+#include <string>
+#include <utility>
+
+#include "src/args/generic.h"
+#include "src/args/timeout.h"
+
+using namespace std;
+using namespace stoke;
+
+namespace {
+
+array<pair<string, Timeout>, 3> pts {{
+    {"quit", Timeout::QUIT},
+		{"restart", Timeout::RESTART},
+    {"testcase", Timeout::TESTCASE}
+  }
+};
+
+} // namespace
+
+namespace stoke {
+
+void TimeoutReader::operator()(std::istream& is, Timeout& t) {
+  string s;
+  is >> s;
+  if (!generic_read(pts, s, t)) {
+    is.setstate(ios::failbit);
+  }
+}
+
+void TimeoutWriter::operator()(std::ostream& os, const Timeout t) {
+  string s;
+  generic_write(pts, s, t);
+  os << s;
+}
+
+} // namespace stoke

src/args/timeout.h

@@ -0,0 +1,36 @@
+// Copyright 2014 eric schkufza
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef STOKE_SRC_ARGS_TIMEOUT_H
+#define STOKE_SRC_ARGS_TIMEOUT_H
+
+#include <iostream>
+
+#include "src/search/timeout.h"
+
+namespace stoke {
+
+struct TimeoutReader {
+  void operator()(std::istream& is, Timeout& t);
+};
+
+struct TimeoutWriter {
+  void operator()(std::ostream& os, const Timeout t);
+};
+
+} // namespace stoke
+
+#endif
+
+

src/cost/cost_function.cc

@@ -99,7 +99,6 @@ Cost CostFunction::max_correctness(const Cfg& cfg, Cost max) {
     res = std::max(res, evaluate_error(reference_out_[i], *(sandbox_->get_result(i))));
     assert(res <= max_testcase_cost);
   }
-	testcases_evaluated_ = i;
 
 	assert(res <= max_correctness_cost);
   return res;
@@ -119,7 +118,6 @@ Cost CostFunction::sum_correctness(const Cfg& cfg, Cost max) {
 
     res += err;
   }
-	testcases_evaluated_ = i;
 
 	assert(res <= max_correctness_cost);
   return res;
@@ -134,19 +132,7 @@ Cost CostFunction::extension_correctness(const Cfg& cfg, Cost max) {
 	// that compute res iteratively may stop executing and return max once res
 	// equals or exceeds that value.
 
-	// This method should set the testcases_evaluated_ attribute to reflect the                                    
-	// number of testcases that were examined prior to a possible early exit. The                                  
-	// final testcase that was used (testcases_evaluted_-1) is returned by a hold_out                              
-	// verifier as a counter-example following a failed proof of correctness (a hold-out
-	// verifier uses a max cost of 0; for non-zero results, the evaluation of this testcase 
-	// is presumably responsible for res exceeding max).
-	testcases_evaluated_ = 1;
-
-	// Invariant 1: 0 < testcases_evaluated_ < sandbox_->size()
-	assert(testcases_evaluated_ > 0);
-	assert(testcases_evaluated_ < sandbox_->size());
-
-	// Invariant 2: Return value should not exceed max_correctness_cost
+	// Invariant 1: Return value should not exceed max_correctness_cost
 	assert(res <= max_correctness_cost);
 
 	return res;

src/cost/cost_function.h

@@ -121,14 +121,14 @@ class CostFunction {
     return result_type(correct, cost);
   }
 
-	/** Returns the number of testcases evaluated by the last invocation of operator(). */
-	size_t testcases_evaluated() const {
-		return testcases_evaluated_;
+	/** Returns the number of testcases used in this function's correctness term. */
+	size_t num_testcases() const {
+		return sandbox_->size();
 	}
-	/** Returns the last testcase evaluated by the last invocation of operator(). */
-	const CpuState& last_testcase_evaluated() const {
-		assert(testcases_evaluated() < sandbox_->size());
-		return sandbox_->get_input(testcases_evaluated()-1);
+	/** Returns the ith testcase used in this function's correctness term. */
+	const CpuState& get_testcase(size_t i) const {
+		assert(i < num_testcases());
+		return sandbox_->get_input(i);
 	}
 
  private:
@@ -164,9 +164,6 @@ class CostFunction {
 	/** Performance term type. */
   PerformanceTerm pterm_;
 
-	/** The number of testcases evaluated by the last invocation of operator(). */
-	size_t testcases_evaluated_;
-
 	/** The results produced by executing the target on testcases. */
   std::vector<CpuState> reference_out_;