String solver: support bounded-length intermediate strings

This adds support for the string solver to use constant-sized arrays to store
variable-length strings (which may be cheaper since smaller formulas are generally needed
to represent them and their constraints to the solver)

This is off-by-default for now since it has not been heavily studied: I expect constant-sized
arrays would be expensive in the case where strings are numerous and sparsely constrained,
but cheaper when there are many index expressions leading to an explosion of Ackermann
constraints.

Author: smowton

.gitignore

@@ -60,8 +60,7 @@ regression/**/tests-*.log
 regression/**/*.goto-cc-saved
 regression/**/*.gb
 regression/**/*.smt2
-jbmc/regression/**/tests.log
-jbmc/regression/**/tests-symex-driven-loading.log
+jbmc/regression/**/*.log
 
 # regression/coverage file
 /regression/coverage_**

jbmc/regression/jbmc-strings/CMakeLists.txt

@@ -2,6 +2,13 @@ add_test_pl_tests(
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
+add_test_pl_profile(
+    "jbmc-strings-fixed-size-arrays"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity"
+    "-C;-s;fixed-size-strings;-X;limited-size-strings-expected-failure"
+    "CORE"
+)
+
 add_test_pl_profile(
     "jbmc-strings-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"

jbmc/regression/jbmc-strings/Makefile

@@ -4,18 +4,22 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CF -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CFTK -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:

jbmc/regression/jbmc-strings/StringContains03/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.check
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringIndexOf/test.desc

@@ -1,6 +1,9 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.check --unwind 4 --max-nondet-string-length 3 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Actually works fine with limited size strings, just takes a very long time.

jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.det 
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.nonDet  --max-nondet-string-length 1000
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

@@ -8,3 +8,4 @@ assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are added correctly.
+

jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.det
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.nonDet --max-nondet-string-length 1000
 ^EXIT=10$