From c95e8e4e2fcbbc20b1000d8e4b5c64403ec99a51 Mon Sep 17 00:00:00 2001 From: laurayuwen Date: Wed, 14 Oct 2015 10:30:24 -0500 Subject: [PATCH 1/4] one semantics: add one config and java module --- src/common/configuration.k | 348 ++++++++++++++++++++++++++++++++++ src/common/core-sorts.k | 8 - src/common/java.k | 82 ++++++++ src/exec/statements.k | 6 +- src/prep/process-type-names.k | 7 + 5 files changed, 442 insertions(+), 9 deletions(-) create mode 100644 src/common/configuration.k create mode 100644 src/common/java.k diff --git a/src/common/configuration.k b/src/common/configuration.k new file mode 100644 index 00000000..b881dcc1 --- /dev/null +++ b/src/common/configuration.k @@ -0,0 +1,348 @@ +module CONFIGURATION + imports CORE-SORTS + imports CORE-FUNCTIONS + +configuration + + //Configuration part 1: threads + + + .K + + .List + + /*The execution context of the current method - local names environment, return type, + context type and current object.*/ + + + //The map from local vars to their location in the store. Also includes outer local vars, for local classes. + .Map + + //current class during all phases, including early preprocessing + noClass + + // OL - location of "this" in store, or noValue in static context + .K + + +
+ //Multithreading-related cells + + //Thread Id + 0 + + //Map[OL |-> Count] - the amount of times this thread holds the monitor objects referred bu the keys + .Map + + //Whether this thread was interrupted by another thread by a call to Thread.interrupt() + false + + + +
+ //cell type: Map[PackageId->Map[Id->ClassType]], Id = simple name, ClassType = full name + //Computed during ProcTypeNamesPhase. Used in all the elaboration phases. + .Map + +
+
+ //Global phase Process Compilation Units + + //Types imported by the current compilation unit. Created in module PROCESS-IMPORTS, part of + //ProcCompUnitsPhase. Used in ProcCompUnitsPhase when imports for a compilation unit are computed, + //and in ProcClassDecsPhase, when they are used to lookup extends/implements clauses. + //Type: Map[Id -> ClassType] + .Map +
+ //The local variable environment, created and used during elaboration phase. + //Represents a stack. Each ListItem contains a Map[Id -> Type] + ListItem(mapWrap(.Map)) + + /*Current method/block context type - either staticCT or instanceCT + Used both during elaboration*/ + staticCT + + //The global registry of all local classes + //When a local class is first encountered in the elaboration phase, a global class name is generated for it + //and the class is registered in this map. + //Type: Map[Id->ClassType] - map from simple local names to global names. + //Used in elaboration phase. + ListItem(mapWrap(.Map)) + + //Counter used to generate unique package names for local classes. Elaboration phase only. + 1 + + //A list of terms that are collected during elaboration phase by a call to appendToElabBuffer() + //and are restored back to by a call to loadElabBuffer() + [.KList] + +
+
+ + + + + + //Class Phase Discovered + + //sort ClassType. Contains the fully qualified class name. + .K + + //Either classMetaT or interfaceMetaT. Used in many semantics phases, including execution. + .K + + //Class access mode - either public or package. + .K + + //The major phase of lifecycle. See ClassPhase definition. + .K + +
+ //Class Phase Created + + //Used by object instantiation + //noClass if this is a top-level class, + //ClassType of the enclosing class otherwise + noClass + + .K + .K + + //The list of class members, in their raw form. + .K + + //Created in ProcCompUnitsPhase, used in ProcClassDecsPhase + .Map //imports of the enclosing CU, for top-level classes only. + + //Either staticCT or instanceCT + .K + + +
+
+ //Class phase Bases Resolved + + .K + +
+
+ + //The base class, or noClass for interfaces and Object. + .K + + /*Directly implemented interfaces, the resolved content of implements clause. + Only used during preprocessing. Mostly to compute , and when transitive list of + interfaces is not needed.*/ + .Set + + /*Map[Id -> ClassType]. Map of classes accessible by simple name inside this class. + Used by type resolution in elaboration phase.*/ + .Map + + //Transitively implemented interfaces. Used by subtyping rules. + .Set + + /*Signatures of methods accessible to this class (both declared and inherited) + Map[Sig -> Class] + Used in elaboration of method calls.*/ + .Map + +
+
+ + /*All methods declared in this class. + Used in elaboration of method calls.*/ + + + + + //Method signature, of type Signature + .K + + .K + + //Method params + .Params + + // first line, constructors only. Either of: + // 'SuperInv - superclass constructor invocation + // 'AltConstrInv - alternate this class constructor invocation + // .K - none, if this class is Object + // For methods this argument is noValue + //The content of this cell is moved into method body during elaboration. + .K + + //Method body + .K + + .K + + //Either staticCT or instanceCT + .K + + //Either methodMMT or constructorMMT + .K + + + + +
+
+ + //[...,, 'LocalVarDec(_),, ...] - Instance field declarations. Used during object instantiation. + .ClassBodyDecList + .BlockStmList + + //[...,, 'FieldDec('Static(_),,T,,_),, ...] - Static field declarations. Used during class instantiation. + .ClassBodyDecList + + //The sequence of static initializers (that also includes field initializers) + //see static-init.k for more details. + .BlockStmList + + //The map of compile-time constant fields. We consider compile-time constants only final static fields + //initialized with a literal expression. + //Constant references are replaced by their values during elaboration phase. + //Created during process classes phase. + //Map[Id -> TypedVal] + .Map + +
+
+ //Global phase Elaboration + + //For local classes only. Map[Id -> Type] of vars accessible from the DIRECT enclosing local env. + //If we have more levels of Local classes nesting, more external local environments + //will be attached to more external classes. + //Used during elaboration phase only. + .Map + +
+
+ //Class Phase Folding + + //The whole class folded back into a 'ClassDec(...) node + .K + +
+
+ //Class Phase Execution - cells only used during execution + + //Initialization status of this class. See static-init.k for more details. + //Only used during execution phase. + StaticUninitialized + + /*The map of static fields declared in this class only, and NOT in superclasses or superinterfaces. + Map[Id -> Location] Used during static variable lookup.*/ + .Map + + + + +
+
+ + //Initial cells, loaded by krun and initial configuration. + + //The initial program loaded by krun. For full mode and preprocessing this is + //the initial java program, for execution mode it is the folded java program. + $PGM:K + + //Main class, passed as krun argument. We need it from the outside, just like JDK Java. + $MainClass:List + + ProcTypeNamesPhase + +
+
+ //Global Phase Execution + + //Execution memory. Map[Location:Int->Value:TypedVal]. Both local vars and heap vars are stored here. + .Map + + //Counter for next location to be used in the cell . + 0 + + //A map from types to objectRef() terms that represent their T.class value + //Created an used in execution phase, by expressions of the form X.class + //Type: Map[Type->TypedVal]. Type may be any reference type. + .Map + +
+
+ + //Represents the storage of objects. Since objects have a complex inner structure, + //we need to hold them separately if we want to represent that structure as a cell tree. + + + + //The id of this object. Same as store location for the newly created object reference. + .K + + //The actual object class + .K + + //One layer for each class in the inheritance chain of this object + + + //The class corresponding to the given chain + .K + + //Map[Id |-> Loc] -> fields defined in this layer + .Map + + //objectRef() ::_ - a reference to the directly enclosing object, or noValue if none. + noValue:>KItem + + + + + + + .K + .K + .Map + + + +
+
+ + //Standard input. Each token is a ListItem. + .List + + //Standard output. Each token is a ListItem. + .List + +
+
+ //Multithreading-related global cells + + //Set[OL:Int] - the set of locations of used monitor objects + .Set + + //Map[ThreadId:Int |-> OL:Int] - map from threads to objects they are waiting on + //waiting on those objects used by methods Object.wait(), Object.notify(), Object.notifyAll(). + .Map + + //Set[ThreadId:Int] The set of terminated threads. + .Set + +
+
+ //Cells used for debugging. Not related to the semantics. + + + + false + + //When computation finishes, dissolve all cells except , + //in order to avoid duplicate solutions during model checking. + $DissolveAllExceptOut:Bool + + .List + + + + +endmodule diff --git a/src/common/core-sorts.k b/src/common/core-sorts.k index c719695a..6cac931e 100644 --- a/src/common/core-sorts.k +++ b/src/common/core-sorts.k @@ -57,14 +57,6 @@ syntax GlobalPhase ::= */ | "ElaborationPhase" - /* Folds the cells into a preprocessed Java program. The last step of elaboration semantics. - */ - | "FoldingPhase" - - /* Unfolds each class from its preprocessed 'ClassDec or 'InterfaceDec form back into a cell. - */ - | "UnfoldingPhase" - /* When all preprocessing / elaboration phases are finished, the actual execution begins. */ | "ExecutionPhase" diff --git a/src/common/java.k b/src/common/java.k new file mode 100644 index 00000000..e2bee658 --- /dev/null +++ b/src/common/java.k @@ -0,0 +1,82 @@ +require "configuration.k" +require "core-sorts.k" +require "core-functions.k" +require "core-classes.k" +require "aux-strings.k" +require "primitive-types.k" +require "subtyping.k" +require "java-syntax.k" + +require "../prep/core-preprocessing.k" +require "../prep/process-type-names.k" +require "../prep/process-comp-units.k" +require "../prep/process-imports.k" +require "../prep/process-class-decs.k" +require "../prep/process-class-members.k" +require "../prep/elaboration-categories.k" +require "../prep/elaboration-core.k" +require "../prep/elaboration-top-blocks.k" +require "../prep/elaboration-statements.k" +require "../prep/elaboration-expressions.k" +require "../prep/elaboration-vars.k" +require "../prep/elaboration-method-invoke.k" +require "../prep/elaboration-new-instance.k" +require "../prep/elaboration-arrays.k" +require "../prep/elaboration-types.k" +require "../prep/literals.k" +require "../prep/process-local-classes.k" +require "../prep/process-anonymous-classes.k" + +require "../exec/core-exec.k" +require "../exec/syntax-conversions.k" +require "../exec/to-string.k" +require "../exec/expressions.k" +require "../exec/expressions-classes.k" +require "../exec/statements.k" +require "../exec/arrays.k" +require "../exec/static-init.k" +require "../exec/new-instance.k" +require "../exec/var-lookup.k" +require "../exec/method-invoke.k" +require "../exec/api-core.k" +require "../exec/api-threads.k" + +module JAVA + imports CONFIGURATION + imports CORE-SORTS + imports AUX-STRINGS + imports PRIMITIVE-TYPES + imports SUBTYPING + + imports JAVA-SYNTAX + + imports PROCESS-TYPE-NAMES + imports PROCESS-COMP-UNITS + imports PROCESS-IMPORTS + imports PROCESS-CLASS-DECS + imports PROCESS-CLASS-MEMBERS + imports ELABORATION-TOP-BLOCKS + imports ELABORATION-STATEMENTS + imports ELABORATION-EXPRESSIONS + imports ELABORATION-VARS + imports ELABORATION-METHOD-INVOKE + imports ELABORATION-NEW-INSTANCE + imports ELABORATION-ARRAYS + imports ELABORATION-TYPES + imports PROCESS-LOCAL-CLASSES + imports PROCESS-ANONYMOUS-CLASSES + imports LITERALS + + imports EXPRESSIONS + imports EXPRESSIONS-CLASSES + imports STATEMENTS + imports ARRAYS + imports STATIC-INIT + imports NEW-INSTANCE + imports NEW-INSTANCE-REST + imports VAR-LOOKUP + imports METHOD-INVOKE + imports METHOD-INVOKE-REST + imports API-CORE + imports API-THREADS +endmodule diff --git a/src/exec/statements.k b/src/exec/statements.k index 8ccbc1f6..1f50609a 100644 --- a/src/exec/statements.k +++ b/src/exec/statements.k @@ -14,6 +14,8 @@ rule isStmt('For(_)) => true //first argument //For now main class may only be placed in the default package. rule [ExecutionPhase-Start]: + + //K-AST for new ().main(new String[0]); . => getClassType(packageId(String2Id("")), String2Id(MainClassS)) @@ -24,8 +26,10 @@ rule [ExecutionPhase-Start]: (( new classString ([0] .DimExps) .Dims), .Exps ); .Map + ... + ListItem(MainClassS:String) - UnfoldingPhase => ExecutionPhase + ElaborationPhase => ExecutionPhase diff --git a/src/prep/process-type-names.k b/src/prep/process-type-names.k index 8375bfea..30dd7ee5 100644 --- a/src/prep/process-type-names.k +++ b/src/prep/process-type-names.k @@ -15,6 +15,13 @@ The initial configuration contains the initial program in cells and + . => Program ... + + Program:K + ProcTypeNamesPhase + rule [CompilationUnit-DefaultPackage-Desugar]: 'CompilationUnit( ( 'None(_) => 'Some('PackageDec(.AnnoList,, 'PackageName( .IdList ))) ),, From ce93de94b26a67baf309a180319fac3d306f6ee8 Mon Sep 17 00:00:00 2001 From: laurayuwen Date: Wed, 14 Oct 2015 10:44:45 -0500 Subject: [PATCH 2/4] move method isOverridden to core-functions --- src/common/core-functions.k | 17 +++++++++++++++++ src/exec/method-invoke.k | 17 ----------------- src/exec/statements.k | 2 -- src/prep/process-class-members.k | 10 ---------- 4 files changed, 17 insertions(+), 29 deletions(-) diff --git a/src/common/core-functions.k b/src/common/core-functions.k index cfbd837c..1b26e8fe 100644 --- a/src/common/core-functions.k +++ b/src/common/core-functions.k @@ -258,6 +258,23 @@ rule getSimpleName(class ClassId:Id) rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) +Int 1 )) +/* +Tests if a method declared in class BaseC with access mode Acc is overridden by a method + with the same signature declared in a subclass SubC. + +The method is overridden if either: + - Acc is protected or public + - Acc is package and BaseC and SubC are declared in the same package (JLS \S6.6) +*/ +syntax KItem ::= isOverridden ( + ClassType, //BaseC + AccessMode, //BaseAcc + ClassType //SubC + ) + +rule isOverridden(_, public, _) => true +rule isOverridden(_, protected, _) => true + /*@ \subsection{Identifiers}*/ // 'Id(Str:String) diff --git a/src/exec/method-invoke.k b/src/exec/method-invoke.k index 3dad3582..b3bc4f0f 100644 --- a/src/exec/method-invoke.k +++ b/src/exec/method-invoke.k @@ -589,23 +589,6 @@ rule [lookupPackageMethod-new-method]: ... -/* -Tests if a method declared in class BaseC with access mode Acc is overridden by a method - with the same signature declared in a subclass SubC. - -The method is overridden if either: - - Acc is protected or public - - Acc is package and BaseC and SubC are declared in the same package (JLS \S6.6) -*/ -syntax KItem ::= isOverridden ( - ClassType, //BaseC - AccessMode, //BaseAcc - ClassType //SubC - ) - -rule isOverridden(_, public, _) => true -rule isOverridden(_, protected, _) => true - // Object class cannot match this rule since it has public access mode rule isOverridden(BaseC:ClassType, package, SubC:ClassType) => eqAux(getPackage(getTopLevel(BaseC)) , getPackage(getTopLevel(SubC))) diff --git a/src/exec/statements.k b/src/exec/statements.k index 1f50609a..1af44af6 100644 --- a/src/exec/statements.k +++ b/src/exec/statements.k @@ -31,8 +31,6 @@ rule [ExecutionPhase-Start]: ListItem(MainClassS:String) ElaborationPhase => ExecutionPhase - - //@ \subsection{Blocks} JLS \$14.2 rule [Block]: diff --git a/src/prep/process-class-members.k b/src/prep/process-class-members.k index 310390c5..b282762a 100644 --- a/src/prep/process-class-members.k +++ b/src/prep/process-class-members.k @@ -181,16 +181,6 @@ rule [isInheritable]: Class BaseClass:ClassType -//A copy of isOverridden from METHOD-INVOKE -syntax KItem ::= isOverridden ( - ClassType, //BaseC - AccessMode, //BaseAcc - ClassType //SubC - ) - -rule isOverridden(_, public, _) => true -rule isOverridden(_, protected, _) => true - // Object class cannot match this rule since it has public access mode rule isOverridden(BaseC:ClassType, package, SubC:ClassType) => eqAux(getPackage(getTopLevel(BaseC)), getPackage(getTopLevel(SubC))) From f8a05a44a6582e84815476f2902ce278c04988b3 Mon Sep 17 00:00:00 2001 From: laurayuwen Date: Wed, 14 Oct 2015 17:15:18 -0500 Subject: [PATCH 3/4] add to distinguish some rules that should not be executed in other phases --- src/common/configuration.k | 9 +-------- src/exec/new-instance.k | 1 + src/exec/static-init.k | 1 + src/prep/process-class-members.k | 2 ++ src/prep/process-comp-units.k | 4 ++-- 5 files changed, 7 insertions(+), 10 deletions(-) diff --git a/src/common/configuration.k b/src/common/configuration.k index b881dcc1..e257e786 100644 --- a/src/common/configuration.k +++ b/src/common/configuration.k @@ -191,7 +191,7 @@ configuration //[...,, 'LocalVarDec(_),, ...] - Instance field declarations. Used during object instantiation. .ClassBodyDecList - .BlockStmList + .BlockStmList //[...,, 'FieldDec('Static(_),,T,,_),, ...] - Static field declarations. Used during class instantiation. .ClassBodyDecList @@ -217,13 +217,6 @@ configuration //Used during elaboration phase only. .Map -
-
- //Class Phase Folding - - //The whole class folded back into a 'ClassDec(...) node - .K -

//Class Phase Execution - cells only used during execution diff --git a/src/exec/new-instance.k b/src/exec/new-instance.k index d891190d..09a3dca6 100644 --- a/src/exec/new-instance.k +++ b/src/exec/new-instance.k @@ -253,6 +253,7 @@ module NEW-INSTANCE-REST rule [FieldDec-instance]: 'FieldDec(.AnnoFieldModList,, T:Type,,'VarDecList('VarDec(X:Id),, .VarDecList)) => . ... Env:Map => Env[X <- default(T) ] + ExecutionPhase //@\subsection{Execution of QSuperConstrInv, AltConstrInv} diff --git a/src/exec/static-init.k b/src/exec/static-init.k index e6e34a28..5c289535 100644 --- a/src/exec/static-init.k +++ b/src/exec/static-init.k @@ -99,5 +99,6 @@ rule [FieldDec-static]: Class:ClassType Class Env:Map => Env[X <- default(T)] + ExecutionPhase endmodule diff --git a/src/prep/process-class-members.k b/src/prep/process-class-members.k index b282762a..4e421784 100644 --- a/src/prep/process-class-members.k +++ b/src/prep/process-class-members.k @@ -389,6 +389,7 @@ rule [FieldDec-Instance]: Class:ClassType Class C:ClassBodyDecList => addElementToClassBodyDecListEnd(C, 'FieldDec(.AnnoFieldModList,, T,, 'VarDecList('VarDec(X:Id),, .VarDecList)) ) + ProcClassMembersPhase when getContextType(Modifiers) ==K instanceCT [structural] @@ -422,6 +423,7 @@ rule [FieldDec-Static]: Class C:ClassBodyDecList => addElementToClassBodyDecListEnd(C, 'FieldDec('AnnoFieldModList('Static(.KList),, .AnnoFieldModList),, T,, 'VarDecList('VarDec(X),, .VarDecList)) ) + ProcClassMembersPhase when getContextType(Modifiers) ==K staticCT [structural] diff --git a/src/prep/process-comp-units.k b/src/prep/process-comp-units.k index b9dac484..464420e3 100644 --- a/src/prep/process-comp-units.k +++ b/src/prep/process-comp-units.k @@ -28,8 +28,8 @@ process declarations in a less-restricted order. rule [ProcCompUnitsPhase-start]: . => Program - ( Program:K => .) - ProcTypeNamesPhase => ProcCompUnitsPhase + Program:K => . + ProcTypeNamesPhase => ProcCompUnitsPhase //ImpDecs will be processed in the module PROCESS-IMPORTS rule [CompilationUnit]: From 349484c87b6626201cf2070bf95f1d17b6ee6d70 Mon Sep 17 00:00:00 2001 From: laurayuwen Date: Mon, 19 Oct 2015 12:29:25 -0500 Subject: [PATCH 4/4] update kjrun.sh --- tools/kjrun.sh | 117 ++++++++++++------------------------------------- 1 file changed, 27 insertions(+), 90 deletions(-) diff --git a/tools/kjrun.sh b/tools/kjrun.sh index 6828649a..85c8592a 100755 --- a/tools/kjrun.sh +++ b/tools/kjrun.sh @@ -50,9 +50,6 @@ function setSearchPattern() { fi } -#If true then we have to run preprocessing semantics first -PREP_FIRST=true - TIME=true # OS-dependent choice of timeout @@ -63,11 +60,7 @@ fi TIMEOUT=$((120 * $TIMEOUT_FACTOR)) SEARCH_TIMEOUT_FACTOR=2 -MODE=run-exec -PREP_OUTPUT=kast -OUTPUT=pretty -PREP_INPUT=java -INPUT=kast +INPUT=java # Pattern example: " OUT:List _" PATTERN="" @@ -83,15 +76,7 @@ CLEAN=false #If true then we display the built command in kjrun and aux-kjrun VERBOSE=false -#If true then don't show any messages besides the actual output -SILENT=false - CMD_SUFFIX="" -COUNT_CMD_SUFFIX="| grep \"Solution\" | wc -l" -PREP_AST_CMD_SUFFIX="| sed 's/\s*\([[:graph:]].*[[:graph:]]\)\s*/\1/g'" -PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | tr -d '\n'" -PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | sed -r 's/.*//g' | sed -r 's/<\/program>.*//g'" -PREP_AST_CMD_SUFFIX="$PREP_AST_CMD_SUFFIX | sed 's/KListWrap/ListWrap/g'" while [[ ${1:0:1} == - ]]; do PARAM=`echo $1 | awk -F= '{print $1}'` @@ -104,31 +89,7 @@ while [[ ${1:0:1} == - ]]; do usage exit ;; - "--prep-ast") - PREP_FIRST=false - MODE=run-prep-ast - CMD_SUFFIX=${PREP_AST_CMD_SUFFIX} - OUTPUT=kast - INPUT=java - TIME=false - TIMEOUT=0 - - ;; - "--prep-pretty") - PREP_FIRST=false - MODE=run-prep-config - INPUT=java - ;; - "--prep-raw") - PREP_FIRST=false - MODE=run-prep-config - OUTPUT=kast - INPUT=java - ;; - "--exec-pretty") - PREP_FIRST=false - MODE=run-exec - ;; + "--split") #everything default ;; "--split-cached") @@ -136,26 +97,12 @@ while [[ ${1:0:1} == - ]]; do TIMEOUT=0 PREP_INPUT=kast-cache OUTPUT=none - SILENT=true ;; "--split-none") PREP_INPUT=kast-cache OUTPUT=none ;; - "--search") - TIMEOUT=$(($TIMEOUT * $SEARCH_TIMEOUT_FACTOR)) - MODE=search - setSearchPattern - ;; - "--search-cached") - TIME=false - TIMEOUT=0 - PREP_INPUT=kast-cache - MODE=search - CMD_SUFFIX=${COUNT_CMD_SUFFIX} - SILENT=true - setSearchPattern - ;; + "--debug") TIME=false TIMEOUT=0 @@ -172,7 +119,6 @@ while [[ ${1:0:1} == - ]]; do PREP_INPUT=kast-cache MODE=symbolic CMD_SUFFIX=${COUNT_CMD_SUFFIX} - SILENT=true setSearchPattern ;; @@ -212,48 +158,39 @@ if [[ ${JAVA_FILE} == "" ]]; then fi BASE_JAVA_FILE=`basename ${JAVA_FILE}` #simple file/dir name -PKAST_FILE=`echo "$BASE_JAVA_FILE" | sed 's#/*$##'` # remove trailing slashes, important if JAVA_FILE is dir -PKAST_FILE=${PKAST_FILE}.pkast +MAIN_CLASS=`echo "$BASE_JAVA_FILE" | cut -d'.' -f1` #simple file minus extension +TOOLS_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +WORK_DIR="$(pwd)" +SEMANTICS_DIR=$(cross-path-native.sh ${TOOLS_DIR}/../src/common) -#Actual execution -if [[ ${SILENT} == false ]]; then - echo "preprocess:" +# OS-dependent selection of krun. +if !(( $TIME == false )); then + KRUN_CMD="time" fi -if [[ ${PREP_FIRST} == true ]]; then - if [ ! -e ${PKAST_FILE} ]; then - CMD="aux-kjrun.sh --time=${TIME} --timeout=${TIMEOUT} --mode=run-prep-ast --output=${PREP_OUTPUT} \ - --cmd-suffix=\"${PREP_AST_CMD_SUFFIX}\" \ - --input=${PREP_INPUT} --verbose=${VERBOSE} ${JAVA_FILE} > ${PKAST_FILE}" - if [[ ${VERBOSE} == true ]]; then - echo "PREP cmd:" - echo ${CMD} - echo - fi - eval ${CMD} - fi -else - PKAST_FILE=${JAVA_FILE} -fi +KRUN_CMD="$KRUN_CMD timeout $TIMEOUT" -if [[ ${SILENT} == false ]]; then - echo - echo "execute:" - echo -fi +KRUN_CMD="$KRUN_CMD $(cross-k.sh krun)" + +KRUN_CMD="$KRUN_CMD --directory \"$SEMANTICS_DIR\"" -CMD="aux-kjrun.sh --time=${TIME} --timeout=${TIMEOUT} --mode=${MODE} --output=${OUTPUT} --input=${INPUT} \ - --pattern=\"${PATTERN}\" --ltlmc=\"${LTLMC}\" --config=\"${CONFIG}\" \ - --verbose=${VERBOSE} --cmd-suffix=\"${CMD_SUFFIX}\" ${PKAST_FILE}" -if [[ ${VERBOSE} == true ]]; then - echo "EXEC cmd:" - echo ${CMD} - echo +if (( $OUTPUT == "none" )); then +KRUN_CMD="$KRUN_CMD --output none" fi +KRUN_CMD="$KRUN_CMD --symbolic-execution -w none" + +KRUN_CMD="$KRUN_CMD --parser \"$(cross-sh.sh kj-parse-aggreg.sh)\"" + +KRUN_CMD="$KRUN_CMD -cMainClass=\"ListItem(\\\"$MAIN_CLASS\\\")\"" + +KRUN_CMD="$KRUN_CMD -cDissolveAllExceptOut=\"true\"" + +KRUN_CMD="$KRUN_CMD $JAVA_FILE" + # Actual command evaluation -eval ${CMD} +eval ${KRUN_CMD} if [[ ${CLEAN} == true ]]; then rm -rf *.kast