verify: announce MIN_M minlen limits for CBMC

smart-tool · Mar 29, 2024 · 0969ad7 · 0969ad7
1 parent 8870ef5
commit 0969ad7
Show file tree

Hide file tree

Showing 68 changed files with 100 additions and 29 deletions.
diff --git a/GNUmakefile b/GNUmakefile
@@ -116,18 +116,15 @@ CBMC_CHECKS=--bounds-check --pointer-check --memory-leak-check            \
 # UNSATISFIABLE. passes, but needs more depth
 UNSATISFIABLE  = ac akc aoso2 aoso4 aoso6 bf bfs blim bmh-sbndm bndml bndmq2 bndmq4 \
 	bndmq6 br bsdm6 bsdm7 bsdm8
-FAIL_VERIFY    = bsdm bww bxs faoso4
+FAIL_VERIFY    = bsdm bww bxs faoso4 ksa fs-w4 ssecp libc
 FAIL = gs tunbm gg rcolussi graspm simon ldm bmh-sbndm faoso4 faoso6 blim \
        bsdm4 bxs fs-w2 fs-w4 fsbndmq32 fsbndmq42 fsbndmq43 fsbndmq62 fsbndmq64 \
        fsbndmq82 fsbndmq84 fsbndmq86 qf26 sbndm-w2 sbndm-w4 tsa tsa-q2 tvsbs-w4 \
        tvsbs-w6 tvsbs-w8 ssecp libc
-TIMEOUT_VERIFY = ag askip aut bsdm2 bm bom2 bom bsdm3 bsdm4 bsdm5 
+TIMEOUT_VERIFY = ag askip aut bsdm2 bm bom2 bom bsdm3 bsdm4 bsdm5 gg gs simon ldm
 NON_CBMC_SRC   =
 # $(addsuffix .c, $(addprefix source/algos/,$(FAIL_VERIFY)))
 verify:
-	@echo unsatisfiable $(UNSATISFIABLE)
-	@echo fail verfify $(FAIL_VERIFY)
-	@echo timeout skipped $(TIMEOUT_VERIFY)
 	for c in $(filter-out $(NON_CBMC_SRC),$(ALGOSRC)); do \
 	  echo $$c; \
 	  echo $(TIMEOUT_1m) cbmc $(CBMC_ARGS_0) $(CBMC_CHECKS) $$c; \

diff --git a/source/algorithms.h b/source/algorithms.h
@@ -378,7 +378,7 @@ const struct algo ALGOS[] = {
   [_AOSO2] = {_AOSO2, OK, "aoso2", "average optimal shift-or (q=2)", 3, 0},
   [_AOSO4] = {_AOSO4, OK, "aoso4", "average optimal shift-or (q=4)", 5, 0},
   [_AOSO6] = {_AOSO6, OK, "aoso6", "average optimal shift-or (q=6)", 7, 0},
-  [_BLIM] = {_BLIM, FAIL, "blim", "bit-parallel length invariant matcher", 0, 0},
+  [_BLIM] = {_BLIM, FAIL, "blim", "bit-parallel length invariant matcher", 0, 0}, // UNSATISFIABLE
   [_FSBNDM] = {_FSBNDM, OK, "fsbndm", "forward sbndm", 0, 0},
   [_BNDMq2] = {_BNDMq2, OK, "bndmq2", "bndm with q-grams", 2, 0},
   [_BNDMq4] = {_BNDMq4, OK, "bndmq4", "bndm with q-grams", 4, 0},
@@ -394,13 +394,13 @@ const struct algo ALGOS[] = {
   [_SABP] = {_SABP, OK, "sabp", "Small Alphabet Bit Parallel", 0, 0},
   [_DBWW] = {_DBWW, OK, "dbww", "Double BWW", 0, 0},
   [_DBWW2] = {_DBWW2, OK, "dbww2", "Double BWW", 0, 0},
-  [_KSA] = {_KSA, OK, "ksa", "Factorized Shift-And", 0, 0},VERIFICATION FAILED
+  [_KSA] = {_KSA, FAIL, "ksa", "Factorized Shift-And", 0, 0}, // VERIFICATION FAILED occ
   [_KBNDM] = {_KBNDM, OK, "kbndm", "Factorized BNDM", 0, 0},
   // new algorithms
   [_BSDM] = {_BSDM, OK, "bsdm", "Backward SNR DAWG Matching", 0, 0},
   [_BSDM2] = {_BSDM2, OK, "bsdm2", "Backward SNR DAWG Matching (m>=2)", 2, 0},
   [_BSDM3] = {_BSDM3, OK, "bsdm3", "Backward SNR DAWG Matching (m>=3)", 3, 0},
-  [_BSDM4] = {_BSDM4, FAIL, "bsdm4", "Backward SNR DAWG Matching (m>=4)", 4, 0},
+  [_BSDM4] = {_BSDM4, FAIL, "bsdm4", "Backward SNR DAWG Matching (m>=4)", 4, 0}, // TIMEOUT
   [_BSDM5] = {_BSDM5, OK, "bsdm5", "Backward SNR DAWG Matching (m>=5)", 5, 0},
   [_BSDM6] = {_BSDM6, OK, "bsdm6", "Backward SNR DAWG Matching (m>=6)", 6, 0},
   [_BSDM7] = {_BSDM7, OK, "bsdm7", "Backward SNR DAWG Matching (m>=7)", 7, 0},
@@ -506,13 +506,13 @@ const struct algo ALGOS[] = {
   [_WFRQ7] = {_WFRQ7, OK, "wfrq7", "Weak Factor Recognizer with q-grams", 7, 0},
   [_WFRQ8] = {_WFRQ8, OK, "wfrq8", "Weak Factor Recognizer with q-grams", 8, 0},
   [_TWFR] = {_TWFR, OK, "twfr", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR2] = {_TWFR2, OK, "twfr2", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR3] = {_TWFR3, OK, "twfr3", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR4] = {_TWFR4, OK, "twfr4", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR5] = {_TWFR5, OK, "twfr5", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR6] = {_TWFR6, OK, "twfr6", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR7] = {_TWFR7, OK, "twfr7", "Tuned Weak Factor Recognizer", 0, 0},
-  [_TWFR8] = {_TWFR8, OK, "twfr8", "Tuned Weak Factor Recognizer", 0, 0},
+  [_TWFR2] = {_TWFR2, OK, "twfr2", "Tuned Weak Factor Recognizer", 2, 0},
+  [_TWFR3] = {_TWFR3, OK, "twfr3", "Tuned Weak Factor Recognizer", 3, 0},
+  [_TWFR4] = {_TWFR4, OK, "twfr4", "Tuned Weak Factor Recognizer", 4, 0},
+  [_TWFR5] = {_TWFR5, OK, "twfr5", "Tuned Weak Factor Recognizer", 5, 0},
+  [_TWFR6] = {_TWFR6, OK, "twfr6", "Tuned Weak Factor Recognizer", 6, 0},
+  [_TWFR7] = {_TWFR7, OK, "twfr7", "Tuned Weak Factor Recognizer", 7, 0},
+  [_TWFR8] = {_TWFR8, OK, "twfr8", "Tuned Weak Factor Recognizer", 8, 0},
   [_TWFRQ2] = {_TWFRQ2, OK, "twfrq2", "Tuned Weak Factor Recognizer with q-grams", 2, 0},
   [_TWFRQ3] = {_TWFRQ3, OK, "twfrq3", "Tuned Weak Factor Recognizer with q-grams", 3, 0},
   [_TWFRQ4] = {_TWFRQ4, OK, "twfrq4", "Tuned Weak Factor Recognizer with q-grams", 4, 0},

diff --git a/source/algos/aoso4.c b/source/algos/aoso4.c
@@ -21,7 +21,7 @@
  * Practical and Optimal String Matching. SPIRE, Lecture Notes in Computer
  * Science, vol.3772, pp.376--387, Springer-Verlag, Berlin, (2005).
  *
- * Constraints: requires m>=4
+ * Constraints: requires m>4
  */
 
 #define MIN_M 5
@@ -54,7 +54,7 @@ int search_large(unsigned char *x, int m, unsigned char *y, int n, int q);
 int search(unsigned char *x, int m, unsigned char *y, int n) {
   unsigned int B[SIGMA], D, h, mm, tmp;
   int i, j, count;
-  int q = 4;
+  const int q = 4;
 
   if (m <= q)
     return search_small(x, m, y, n);

diff --git a/source/algos/aoso6.c b/source/algos/aoso6.c
@@ -21,7 +21,7 @@
  * Practical and Optimal String Matching. SPIRE, Lecture Notes in Computer
  * Science, vol.3772, pp.376--387, Springer-Verlag, Berlin, (2005).
  *
- * Constraints: requires m>=6
+ * Constraints: requires m>6
  */
 
 #define MIN_M 7

diff --git a/source/algos/bndmq2.c b/source/algos/bndmq2.c
@@ -26,6 +26,7 @@
  * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bndmq4.c b/source/algos/bndmq4.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=4
  */
 
+#define MIN_M 4
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bndmq6.c b/source/algos/bndmq6.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=6
  */
 
+#define MIN_M 6
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm2.c b/source/algos/bsdm2.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm3.c b/source/algos/bsdm3.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=3
  */
 
+#define MIN_M 3
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm4.c b/source/algos/bsdm4.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=4
  */
 
+#define MIN_M 4
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm5.c b/source/algos/bsdm5.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=5
  */
 
+#define MIN_M 5
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm6.c b/source/algos/bsdm6.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=6
  */
 
+#define MIN_M 6
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm7.c b/source/algos/bsdm7.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=7
  */
 
+#define MIN_M 7
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bsdm8.c b/source/algos/bsdm8.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=8
  */
 
+#define MIN_M 8
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/bww.c b/source/algos/bww.c
@@ -68,7 +68,7 @@ int search(unsigned char *x, int m, unsigned char *y, int n) {
   for (k = 1; k < end; ++k) {
     /* Left to right scanning */
     r = pre = left = 0;
-    R = ~0;
+    R = ~0U;
     cur = s;
     while (R != 0 && k * m - 1 + r < n) {
       R &= B[y[k * m - 1 + r]];
@@ -81,7 +81,7 @@ int search(unsigned char *x, int m, unsigned char *y, int n) {
       cur >>= 1;
     }
     /* Right to left scanning */
-    L = ~0;
+    L = ~0U;
     cur = 1;
     ell = 0;
     while (L != 0 && left > ell) {
@@ -112,11 +112,10 @@ int search(unsigned char *x, int m, unsigned char *y, int n) {
  */
 
 int search_large(unsigned char *x, int m, unsigned char *y, int n) {
-  int i, k, left, r, ell, end, count, p_len, first, j;
+  int i, k, left, r, ell, end, count, first, j;
   unsigned int B[SIGMA], C[SIGMA], s, t, R, L;
   unsigned int pre, cur;
-
-  p_len = m;
+  const int p_len = m;
   m = 30;
 
   /* Preprocessing */
@@ -151,7 +150,7 @@ int search_large(unsigned char *x, int m, unsigned char *y, int n) {
   for (k = 1; k < end; ++k) {
     /* Left to right scanning */
     r = pre = left = 0;
-    R = ~0;
+    R = ~0U;
     cur = s;
     while (R != 0 && k * m - 1 + r < n) {
       R &= B[y[k * m - 1 + r]];
@@ -164,7 +163,7 @@ int search_large(unsigned char *x, int m, unsigned char *y, int n) {
       cur >>= 1;
     }
     /* Right to left scanning */
-    L = ~0;
+    L = ~0U;
     cur = 1;
     ell = 0;
     while (L != 0 && left > ell) {

diff --git a/source/algos/faoso2.c b/source/algos/faoso2.c
@@ -24,6 +24,7 @@
  * Constraints: requires m>2
  */
 
+#define MIN_M 3
 #include "include/define.h"
 #include "include/log2.h"
 #include "include/main.h"

diff --git a/source/algos/sbndm-bmh.c b/source/algos/sbndm-bmh.c
@@ -24,6 +24,7 @@
  * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/sbndm-w2.c b/source/algos/sbndm-w2.c
@@ -48,6 +48,7 @@
  *       e.g. sbndm-w2 aba 3 ababababab 10
  */
 
+#define MIN_M 2
 #include <assert.h>
 #include "include/define.h"
 #include "include/main.h"

diff --git a/source/algos/sbndm-w4.c b/source/algos/sbndm-w4.c
@@ -43,6 +43,7 @@
  
  */
 
+#define MIN_M 4
 #include <assert.h>
 #include "include/define.h"
 #include "include/main.h"

diff --git a/source/algos/sbndm-w6.c b/source/algos/sbndm-w6.c
@@ -40,10 +40,9 @@
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
  OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
  SUCH DAMAGE.
-
- * Note: inexact m>32
  */
 
+#define MIN_M 6
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_large.h"

diff --git a/source/algos/sbndmq2.c b/source/algos/sbndmq2.c
@@ -26,6 +26,7 @@
  * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/sbndmq4.c b/source/algos/sbndmq4.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=4
  */
 
+#define MIN_M 4
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/sbndmq6.c b/source/algos/sbndmq6.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=6
  */
 
+#define MIN_M 4
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/sbndmq8.c b/source/algos/sbndmq8.c
@@ -25,6 +25,7 @@
  * Constraints: requires m>=8
  */
 
+#define MIN_M 8
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/simdkr.c b/source/algos/simdkr.c
@@ -28,8 +28,11 @@
  * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
  * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
  * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 

diff --git a/source/algos/skip2.c b/source/algos/skip2.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip3.c b/source/algos/skip3.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=3
  */
 
+#define MIN_M 3
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip4.c b/source/algos/skip4.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=4
  */
 
+#define MIN_M 4
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip5.c b/source/algos/skip5.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=5
  */
 
+#define MIN_M 5
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip6.c b/source/algos/skip6.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=6
  */
 
+#define MIN_M 6
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip7.c b/source/algos/skip7.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=7
  */
 
+#define MIN_M 7
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/skip8.c b/source/algos/skip8.c
@@ -27,6 +27,7 @@
  * Constraints: requires m>=8
  */
 
+#define MIN_M 8
 #include "include/define.h"
 #include "include/main.h"
 #include "include/AUTOMATON.h"

diff --git a/source/algos/tvsbs-w2.c b/source/algos/tvsbs-w2.c
@@ -19,6 +19,7 @@
  * Optimized TVSBS algorithm.
  */
 
+//#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 

diff --git a/source/algos/tvsbs-w4.c b/source/algos/tvsbs-w4.c
@@ -20,6 +20,7 @@
  * Constraints: requires n >= m + 2, and m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/tvsbs-w6.c b/source/algos/tvsbs-w6.c
@@ -20,6 +20,7 @@
  * Constraints: requires n >= m + 2, and m>=2
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"

diff --git a/source/algos/tvsbs-w8.c b/source/algos/tvsbs-w8.c
@@ -20,6 +20,7 @@
  * Constraints: requires n >= m + 2, and m>=2 and m<XSIZE
  */
 
+#define MIN_M 2
 #include "include/define.h"
 #include "include/main.h"
 #include "include/search_small.h"