KJ-22 Symbolic execution - tools support. Full support implemented for kjrun and kjtest. Added kjtest output files for symbolic execution examples. ready to be integrated into jenkins. Untested.

Author: denis-bogdanas

symbolic/symbolic_01_max3.search.out

@@ -0,0 +1 @@
+3

symbolic/symbolic_02_BasicList.search.out

@@ -0,0 +1 @@
+4

symbolic/symbolic_03_OrderedList.search.out

@@ -0,0 +1 @@
+11

tools/aux-kjtest.sh

@@ -7,7 +7,7 @@
 # If only four arguments are provided, test directory is assumed to be ../programs
 
 if (( "$#" < 10 )); then
-    echo "Usage: `basename $0` -mode <run/search> -threads <num_threads> -timeout <timeout in s> /
+    echo "Usage: `basename $0` -mode <run|search|symbolic|jdk> -threads <num_threads> -timeout <timeout in s> /
           -encodeXML <true/false> -clean <true/false> [target files/dirs]"
     exit
 fi
@@ -38,12 +38,19 @@ GEN_CMD="$(cross-sh.sh ${TOOLS_DIR}/jdk-run.sh) --keep-temp"
 case "$MODE" in
 "run")
     RUN_CMD="$(cross-sh.sh ${TOOLS_DIR}/kjrun.sh) --cached"
+    EXPECTED_OUT_EXT=out
     ;;
 "search")
     RUN_CMD="$(cross-sh.sh ${TOOLS_DIR}/kjrun.sh) --search-cached"
+    EXPECTED_OUT_EXT=out
+    ;;
+"symbolic")
+    RUN_CMD="$(cross-sh.sh ${TOOLS_DIR}/kjrun.sh) --symbolic-cached"
+    EXPECTED_OUT_EXT=search.out
     ;;
 "jdk")
     RUN_CMD=$(cross-sh.sh ${TOOLS_DIR}/aux-echo.sh)
+    EXPECTED_OUT_EXT=out
     ;;
 *)
     echo "Invalid MODE: ${MODE}"
@@ -63,6 +70,7 @@ java -jar ${TEST_RUNNER_JAR} \
   -gen \"${GEN_CMD}\" \
   -run \"${RUN_CMD}\" \
   -taskExt java \
+  -expectedOutExt \"${EXPECTED_OUT_EXT}\" \
   -testsuiteName java-semantics \
   -classnameStyle simple \
   -threads ${THREADS} \

tools/kjrun.sh

@@ -6,7 +6,7 @@ if (( "$#" < 1 )) || (( "$#" > 2 )); then
     echo "Your command:"
     echo `basename $0` $@
     echo "Usage: `basename $0` <javaFile>"
-    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic> <javaFile>"
+    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic|--symbolic-cached> <javaFile>"
     echo "For more options use aux-kjrun.sh"
     exit 1
 fi
@@ -64,10 +64,13 @@ case "$OPTION" in
     aux-kjrun.sh --time true --timeout ${SYMBOLIC_TIMEOUT} --mode symbolic \
       --output pretty --kast-cache false ${JAVA_FILE}
     ;;
+"--symbolic-cached")
+    aux-kjrun.sh --time false --timeout 0 --mode symbolic-count --output raw --kast-cache true ${JAVA_FILE}
+    ;;
 *)
     echo "Invalid option: $OPTION"
     echo "Usage: `basename $0` <javaFile>"
-    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic> <javaFile>"
+    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic|--symbolic-cached> <javaFile>"
     echo "For more options use aux-kjrun.sh"
     exit 1
     ;;

tools/kjtest.sh

@@ -21,13 +21,16 @@ fi
 
 case "$OPTION" in
 "--run")
-    aux-kjtest.sh -mode run    -threads 12 -timeout 120 -encodeXML false -clean false ${@}
+    aux-kjtest.sh -mode run      -threads 12 -timeout 120 -encodeXML false -clean false ${@}
     ;;
 "--search")
-    aux-kjtest.sh -mode search -threads  6 -timeout 600 -encodeXML false -clean false ${@}
+    aux-kjtest.sh -mode search   -threads  6 -timeout 600 -encodeXML false -clean false ${@}
+    ;;
+"--symbolic")
+    aux-kjtest.sh -mode symbolic -threads  6 -timeout 600 -encodeXML false -clean false ${@}
     ;;
 "--jdk")
-    aux-kjtest.sh -mode jdk    -threads 12 -timeout  10 -encodeXML false -clean true  ${@}
+    aux-kjtest.sh -mode jdk      -threads 12 -timeout  10 -encodeXML false -clean true  ${@}
     ;;
 "--t1")
     aux-kjtest.sh -mode run    -threads  1 -timeout 120 -encodeXML false -clean false ${@}