KJ-22 Symbolic execution - tools support. Untested yet. On Windows don't work presumably because windows maude is on 32 bits.

Author: denis-bogdanas

symbolic/symbolic_01_max3.cIN.in

@@ -0,0 +1 @@
+ListItem(3) ListItem(#symInt(x)) ListItem(8)

symbolic/symbolic_02_BasicList.cIN.in

@@ -0,0 +1 @@
+ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))

symbolic/symbolic_03_OrderedList.cIN.in

@@ -0,0 +1 @@
+ListItem(#symInt(e1)) ListItem(#symInt(e2)) ListItem(#symInt(x))

tools/aux-kjrun.sh

@@ -11,7 +11,7 @@ if (( "$#" != 11 )); then
     echo "Your command:"
     echo `basename $0` $@
     echo "Usage: `basename $0` --time <true|false> --timeout <timeout in s> \
-      --mode <run|search|search-count|debug> --output <none|raw|pretty> \
+      --mode <run|search|search-count|symbolic|symbolic-count|debug> --output <none|raw|pretty> \
       --kast-cache <true|false> \
       <javaFile>"
     exit 1
@@ -64,6 +64,11 @@ case "$MODE" in
 "search"|"search-count")
     KRUN_CMD="$KRUN_CMD --search-final -cModelCheck=\"true\""
     ;;
+"symbolic"|"symbolic-count")
+    IN_FILE=${JAVA_FILE%.java}.cIN.in
+    IN_VALUE=$(<${IN_FILE})
+    KRUN_CMD="$KRUN_CMD --search -cModelCheck=\"true\" -cPC=true -cIN=\"$IN_VALUE\""
+    ;;
 "debug")
     KRUN_CMD="$KRUN_CMD --debug -cModelCheck=\"false\""
     ;;
@@ -93,7 +98,7 @@ if [ ${KAST_CACHE} == false ];
     eval ${PARSER_CMD}
 fi
 
-if [ ${MODE} == "search-count" ];
+if [ ${MODE} == "search-count" ] || [ ${MODE} == "symbolic-count" ];
   then KRUN_CMD="$KRUN_CMD  | grep \"Solution\" | wc -l"
 fi
 

tools/kjkompile.sh

@@ -33,6 +33,9 @@ case "$OPTION" in
 "threading")
     $KOMPILE_CMD -v -transition "transition-threading" java
     ;;
+"symbolic")
+    $KOMPILE_CMD -v --backend symbolic --symbolic-rules "symbolic-rule" java
+    ;;
 "latex")
     $KOMPILE_CMD -v --backend latex --doc-style "style=math" java
     ;;
@@ -41,7 +44,7 @@ case "$OPTION" in
     ;;
 *)
     echo "Invalid option: $OPTION"
-    echo "Usage: `basename $0` or `basename $0` <exec|strictness|threading|latex|pdf>"
+    echo "Usage: `basename $0` or `basename $0` <exec|strictness|threading|symbolic|latex|pdf>"
     exit 1
     ;;
 esac

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> <javaFile>"
+    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic> <javaFile>"
     echo "For more options use aux-kjrun.sh"
     exit 1
 fi
@@ -20,18 +20,24 @@ if (( "$#" == 1 ));
     JAVA_FILE=$2
 fi
 
-# OS-dependent choice of default timeout
+# OS-dependent choice of timeout
 if [[ $(uname) == *Linux* ]]
   then DEFAULT_TIMEOUT=30
   else DEFAULT_TIMEOUT=120
 fi
 
-# OS-dependent choice of default timeout
+# OS-dependent choice of timeout
 if [[ $(uname) == *Linux* ]]
   then SEARCH_TIMEOUT=60
   else SEARCH_TIMEOUT=120
 fi
 
+# OS-dependent choice of timeout
+if [[ $(uname) == *Linux* ]]
+  then SYMBOLIC_TIMEOUT=120
+  else SYMBOLIC_TIMEOUT=240
+fi
+
 case "$OPTION" in
 "--pretty")
     aux-kjrun.sh --time true --timeout ${DEFAULT_TIMEOUT} --mode run --output pretty --kast-cache false ${JAVA_FILE}
@@ -54,10 +60,14 @@ case "$OPTION" in
 "--debug")
     aux-kjrun.sh --time false --timeout 0 --mode debug --output pretty --kast-cache false ${JAVA_FILE}
     ;;
+"--symbolic")
+    aux-kjrun.sh --time true --timeout ${SYMBOLIC_TIMEOUT} --mode symbolic \
+      --output pretty --kast-cache false ${JAVA_FILE}
+    ;;
 *)
     echo "Invalid option: $OPTION"
     echo "Usage: `basename $0` <javaFile>"
-    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug> <javaFile>"
+    echo "Or:    `basename $0` <--pretty|--raw|--none|--search|--cached|--search-cached|--debug|--symbolic> <javaFile>"
     echo "For more options use aux-kjrun.sh"
     exit 1
     ;;