diff --git a/.gitignore b/.gitignore index 5c18354..11bd18c 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ test/rvm/property-db test/mop/property-db *-kompiled/ +*.bak \ No newline at end of file diff --git a/ToDo.txt b/ToDo.txt new file mode 100644 index 0000000..50ed25a --- /dev/null +++ b/ToDo.txt @@ -0,0 +1,20 @@ +1. develop a template of c program. +2. rewrite the template to real c code string. + +3. handle the case where multiple formulas are inside one spec. + +For each property, there will be a matrix of integers encoding the transition functions. + +Each row of the matrix encodes an event transition function, and the row number is the index of the corresponding event. + +So for each property, we can simple keep a matrix and two string arrays (one for events and one for states). + +*** +P.S. Need to consider the corner cases: +a) A defined event never occurs inside the formula. + +b) Undefined event occurs in the formula. + +c) Duplicate definitions for events/states. + +d) Undefined state in the formula. \ No newline at end of file diff --git a/problems-identified.txt b/problems-identified.txt new file mode 100644 index 0000000..d73aea5 --- /dev/null +++ b/problems-identified.txt @@ -0,0 +1,16 @@ +1. current rv-monitor for c part only supports one pair of property and handler +in one spec. + +the part for java is better, but the generated code does not compile due to +re-define some vars in the same runtime monitor function (the method in which +event dispatching occurs). + +*** +In fact, even if the compile-time errors are corrected, the generated code for +multi-properties spec is still incorrect. + +The transition functions for each property can be generated, but +the monitor is not keeping track of the states of multiple fsm. +It only keeps track of a single current state, which is not +the combination of states for each fsm, no matter how many +properties you have. \ No newline at end of file diff --git a/src/c-monitor-code-template/c-monitor-event-action.k b/src/c-monitor-code-template/c-monitor-event-action.k new file mode 100644 index 0000000..7112844 --- /dev/null +++ b/src/c-monitor-code-template/c-monitor-event-action.k @@ -0,0 +1,143 @@ +require "../rvm/rvm-compiler-core.k" +require "c-monitor-template-syntax.k" +require "../helper/code-gen.k" +require "../helper/util.k" + +module C-MONITOR-EVENT-ACTION + imports RVM-COMPILER-CORE + imports C-MONITOR-TEMPLATE-SYNTAX + imports CODE-GEN + imports UTIL + + rule $main4 => $eventFuncs(size(EL)) + EL:List + _:Map => .Map + CL:List (.List => ListItem("\n")) + + rule $eventFuncs(I:Int) => ($eFunc(0), $eventFuncs(I)) + when I >Int 0 + + rule $eventFuncs(I:Int) => .K + when I <=Int 0 + + rule $eFunc(I:Int), $eventFuncs(0) => .K + .K + .K + + rule $eFunc(I:Int), $eventFuncs(J:Int) => $eFunc(I +Int 1), $eventFuncs(J -Int 1) + .K => $eFunc(I) + _ => .List + CL:List (.List => ListItem("\n")) + when J >Int 0 + + rule $eFunc(I:Int) => $methHeader(I) {$mbody} + + //print method header + rule $methHeader(I:Int) {$mbody} => $mbody2 + EL:List + SN:String + //the params of each event, indexed by event id + EPs:List + //the list of event action code, indexed by event id. + EAs:List + Code:List + //method header of event I. + (.List => ListItem(printMethodHeader(SN, getStringI(EL, I), getStringI(EPs, I)))) + + (.List => ListItem("{\n")) + + (.List => ListItem(getStringI(EAs, I))) //the event I's action code + + +
HeaderCode:List (.List => + ListItem(printMethodHeader(SN, getStringI(EL, I), getStringI(EPs, I)) +String ";")) +
+ + //store the current event name which will be used to infer event transition function. + .List => ListItem(getStringI(EL, I)) + + +////////////////////////////////////////////////////////////////////////////// + //state updates + rule $mbody2 => ($stateUpdates(PS) ;; $handlers) + PS:Int + + rule ($stateUpdates(PS:Int) ;; $handlers) => + $sUpdate(0) ,, $stateUpdates(PS) ;; $handlers + + + rule + ($sUpdate(I:Int) ,, $stateUpdates(PS:Int) ;; $handlers) + => $handlers + + when PS <=Int 0 + + rule + ($sUpdate(I:Int) ,, $stateUpdates(PS:Int) ;; $handlers) => + ($sUpdate(I +Int 1) ,, $stateUpdates(PS -Int 1) ;; $handlers) + + + .K => $gsUpdate(I), $lsUpdates(getSize(SML, I)) + SML:List + + //cache the state map of property I + .Map => getMapI(SML, I) + + _:Int => I //the cur property rank is I +when PS >Int 0 + +//finish the state updates code + rule + ($sUpdate(I:Int) ,, $stateUpdates(0) ;; $handlers) => + $handlers + + .K + +//generate global state update code +//when the property size > 1, the event transition function will have property rank as prefix +rule $gsUpdate(I:Int), $lsUpdates(J:Int) => $lsUpdates(J) + SN:String + ListItem(EN:String) //the tmpList stores the current event name + C:List (.List => ListItem( +globalStateUpdate(globalStateVarI(I), propXEventE(SN, I, EN)) +)) + + PS:Int +when PS >Int 1 + +//only a single property is defined +rule $gsUpdate(I:Int), $lsUpdates(J:Int) => $lsUpdates(J) + SN:String + ListItem(EN:String) //the tmpList stores the current event name + C:List (.List => ListItem( +globalStateUpdate(globalStateVarI(I), propXEventE(SN, EN)) +)) + + PS:Int +when PS <=Int 1 + +//update local states +rule $lsUpdate(I:Int) $lsUpdates(0) => .K + M:Map => .Map + + +rule $lsUpdates(I:Int) => $lsUpdate(0) $lsUpdates(I) + +rule $lsUpdate(I:Int) $lsUpdates(J:Int) => $lsUpdate(I +Int 1) $lsUpdates(J -Int 1) + G:Int + SN:String + M:Map +//the three args are local state var, global state var, state rank +//localStateVarI(spec name, property rank, state name) + C:List (.List => ListItem(localStateUpdate( localStateVarI(SN, G, getStrKey(M, I)), +globalStateVarI(G), I))) + +when J >Int 0 + +//handler code and closing parenthesis +rule $handlers => .K + .K + HDM:Map + C:List (.List => getHandlerCode(HDM)) (.List => ListItem("\n}\n")) + +endmodule \ No newline at end of file diff --git a/src/c-monitor-code-template/c-monitor-template-syntax.k b/src/c-monitor-code-template/c-monitor-template-syntax.k new file mode 100644 index 0000000..4c52ff8 --- /dev/null +++ b/src/c-monitor-code-template/c-monitor-template-syntax.k @@ -0,0 +1,89 @@ +require "domains.k" + +module C-MONITOR-TEMPLATE-SYNTAX + imports DOMAINS + +//the state transition function is encoded using int array. +syntax CTemplate ::= Include MainBody + +syntax MainBody ::= GlobalStatesInit MainBody1 + +syntax MainBody1 ::= PropStatesInit MainBody2 +syntax MainBody2 ::= ResetFunc MainBody3 +syntax MainBody3 ::= StateTransitions MainBody4 +syntax MainBody4 ::= EventMethods + +syntax CTemplate ::= "$CMonitor" +syntax Include ::= "$incl" +syntax MainBody ::= "$main" +syntax MainBody1 ::= "$main1" +syntax MainBody2 ::= "$main2" +syntax MainBody3 ::= "$main3" +syntax MainBody4 ::= "$main4" + + +syntax GStateVar ::= "$gSVar" "(" Int ")" +syntax GlobalStatesInit ::= "$globalInit" "(" Int ")" +syntax GlobalStatesInit ::= GStateVar "," GlobalStatesInit + +syntax StateVar ::= "$sVar" "(" Int "," Int ")" //prop rank, state rank +//args of $localInit: the prop rank, the number of states in the property +syntax LocalStatesInit ::= "$localInit" "(" Int "," Int ")" +syntax LocalStatesInit ::= StateVar "," LocalStatesInit + +syntax PropStatesInit ::= "$pStates" "(" Int ")" +syntax PropStatesInit ::= LocalStatesInit ":" PropStatesInit + + +syntax ResetFunc ::= "$reset" + +//the state functions are indexed by property rank and event rank +syntax StateTransitions ::= "$stateFuncs" "(" Int "," Int ")" +syntax StateFunc ::= "$sFunc" "(" Int "," Int ")" +syntax StateTransitions ::= StateFunc + | StateFunc "," StateTransitions + | "$emptyTransition" + +syntax EventMethods ::= "$eventFuncs" "(" Int ")" +syntax EventMethod ::= "$eFunc" "(" Int ")" +syntax EventMethods ::= EventMethod | EventMethod "," EventMethods + +//the structure of an event action method +//based on the configuration, the same method body prototype +//can be rewritten to different concrete method bodies. +syntax MethodHeader ::= "$methHeader" "(" Int ")" + +syntax EventAction ::= "$eAction" "(" Int ")" + +//update the states in each property. +syntax MonitorStateUpdates ::= "$stateUpdates" "(" Int ")" +syntax MonitorStateUpdate ::= "$sUpdate" "(" Int ")" +syntax MonitorStateUpdates ::= MonitorStateUpdate + | MonitorStateUpdate ",," MonitorStateUpdates + +syntax HandlerActions ::= "$handlers" + +syntax MethodBody ::= EventAction ";;" MethodBody2 +syntax MethodBody2 ::= MonitorStateUpdates ";;" HandlerActions + +syntax EventMethod ::= MethodHeader "{" MethodBody "}" + +syntax MethodBody ::= "$mbody" +syntax MethodBody2 ::= "$mbody2" + +//in the section of monitor state updates, there are two parts: +//1. update the current state of the monitor, +//2. update the state predicates for each state in the automata (whether that state is on) +syntax MonitorStateUpdate ::= GlobalStateUpdate "," LocalStateUpdates +//the int argument is the property rank of the state var +syntax GlobalStateUpdate ::= "$gsUpdate" "(" Int ")" + +//the arg is the number of states in the current property +syntax LocalStateUpdates ::= "$lsUpdates" "(" Int ")" + +//by querying the configuration, we can build the entry of state name (string) |-> state rank (int) +syntax LocalStateUpdate ::= "$lsUpdate" "(" Int ")" + +syntax LocalStateUpdates ::= LocalStateUpdate | LocalStateUpdate LocalStateUpdates + +endmodule \ No newline at end of file diff --git a/src/c-monitor-code-template/c-monitor-template.k b/src/c-monitor-code-template/c-monitor-template.k new file mode 100644 index 0000000..be439fa --- /dev/null +++ b/src/c-monitor-code-template/c-monitor-template.k @@ -0,0 +1,178 @@ +require "../rvm/rvm-compiler-core.k" +require "c-monitor-template-syntax.k" +require "../helper/code-gen.k" +require "../helper/util.k" + +require "c-monitor-event-action.k" + +module C-MONITOR-TEMPLATE + imports RVM-COMPILER-CORE + imports C-MONITOR-TEMPLATE-SYNTAX + imports C-MONITOR-EVENT-ACTION + + imports CODE-GEN + imports UTIL + +rule + "c" + false + 1 => 2 + .K => $CMonitor + + +rule + "c" + false + + $CMonitor => + $incl $main + + +//generate the include part. +//TODO: incorporate the user provided includes +rule $incl $main => $main + L:List (.List => ListItem(IDL) + ListItem("#include \n\n") ) + + IDL:String + +//incorporate the user provided declarations +rule $main + DBL:DecBubbleList => .K + L:List (.List => + ListItem(declBubbleList2String(DBL))) + + +///////// +//rewrite the global var declarations. + rule $main => $globalInit(0) $main1 + +rule $globalInit(P:Int) $main1 => $main1 + PS:Int +when P >=Int PS + +rule ($globalInit(I:Int) $main1) => ($globalInit(I +Int 1) $main1) + + L:List (.List => ListItem(getGlobalStateVarInit(I))) + PS:Int +when I $pStates(0) $main2 + +rule $pStates(I:Int) $main2 => $main2 + PN:Int //the number of properties + when I >=Int PN + +rule $pStates(I:Int) $main2 => ($localInit(I, getSize(L, I)) : $pStates(I +Int 1)) + $main2 + PN:Int //the number of properties + L:List + _:Map => getMapI(L, I) + when I ($localInit(R:Int, 0):$pStates(I:Int) $main2) => ($pStates(I) $main2) + L:List => .List //the local state vars are stored in tmp cell + C:List (.List => L) + +rule ($localInit(R:Int, I:Int):$pStates(P:Int) $main2) => + (($sVar(R, I -Int 1), $localInit(R, I -Int 1)):$pStates(P) $main2) + +when I >=Int 1 + +rule (($sVar(R:Int, I:Int), $localInit(R, J:Int)):$pStates(P:Int) $main2) => + (($localInit(R, J):$pStates(P)) $main2) + + StateMap:Map + SpecName:String +//localStateVarInit(SpecName:String, R:Int, StateName:String) +//state name: getStrKey(StateMap, I) + (.List => ListItem(localStateVarInit(SpecName, R, getStrKey(StateMap, I)))) + L:List + +rule $main2 => $reset $main3 + +rule $reset $main3 => $main3 + SN:String + P:Int + Code:List (.List => ListItem(printResetFunc(SN, P):String)) +
Header:List (.List => +ListItem(printResetFuncHeader(SN, P) +String ";"))
+ +//rewrite $main3 to state transitions and $main4 +rule + P:Int + L:List + $main3 => ($stateFuncs(P, size(L)) $main4) + +rule ($stateFuncs(P:Int, E:Int) $main4) => (getListofStateFuncs(0, 0, P, E) $main4) + +//gen the state transition function from the structure + rule ($emptyTransition $main4) => $main4 + +//print transition function (multiple properties in one spec) + rule + (($sFunc(I:Int, J:Int):StateFunc, L:StateTransitions) $main4) => (L $main4) + EL:List + X:Id + + ... + + I + M:Map + IA:List + + ... + + SN:String + PS:Int + Code:List (.List => + ListItem(stateTransitionPropXEventE(SN, I, Id2String(X), IA))) +when + (getStringI(EL, J) ==String Id2String(X)) andBool + PS >Int 1 + +//single property + rule + (($sFunc(I:Int, J:Int):StateFunc, L:StateTransitions) $main4) => (L $main4) + EL:List + X:Id + + ... + + I + M:Map + IA:List + + ... + + SN:String + PS:Int + Code:List (.List => + ListItem(stateTransitionPropXEventE(SN, Id2String(X), IA))) +when getStringI(EL, J) ==String Id2String(X) + andBool PS <=Int 1 + +////////////////////////////////////////////////////////////////////////////////// +//generate the output monitor file and header file + rule 2 => 3 + //the output c file name and header file name are stored in cell and resp. + .K => "__RVC_" +String SN +String "_Monitor.c" + .K => "__RVC_" +String SN +String "_Monitor.h" + .K + SN:String + + rule 3 + OutCFileName:String => #write(#open(OutCFileName), StringList2String(CL)) + CL:List => .List + + //generate the output header file + OutHFileName:String => #write(#open(OutHFileName), + addCTemplate(StringList2String(HL), SN)) +
HL:List => .List
+ SN:String + +////////////////////////////////////////////////////////////////////////////////// + +endmodule \ No newline at end of file diff --git a/src/c-monitor-code-template/seatbelt.c.origin b/src/c-monitor-code-template/seatbelt.c.origin new file mode 100644 index 0000000..e31d420 --- /dev/null +++ b/src/c-monitor-code-template/seatbelt.c.origin @@ -0,0 +1,57 @@ +#include +#include + +static int __RVC_state = 0; +static int __RVC_SEATBELT_SEATBELTREMOVED[] = {-1,0, }; +static int __RVC_SEATBELT_SEATBELTATTACHED[] = {1, -1,}; + + +int __RVC_SeatBelt_safe = 0; +int __RVC_SeatBelt_unsafe = 0; + +void +__RVC_SeatBelt_reset(void) +{ + __RVC_state = 0; + } + + + +void +__RVC_SeatBelt_seatBeltRemoved() +{ +{fprintf(stderr, "Seat belt removed.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTREMOVED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + +void __RVC_SeatBelt_seatBeltAttached() +{ +{fprintf(stderr, "Seat belt attached.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTATTACHED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + + diff --git a/src/c-monitor-code-template/template.c.try b/src/c-monitor-code-template/template.c.try new file mode 100644 index 0000000..543db91 --- /dev/null +++ b/src/c-monitor-code-template/template.c.try @@ -0,0 +1,73 @@ +$0 // #include + // #include + +$1 // "static int __RVC_state = 0;\n" + +$2 // "int __RVC_" + +$spec // spec name + +$u // underscore: "_" + +$4 // " = 0;\n" //init to 0 + +$state // will rewrite to: for each $i in #numOfStates { $state_i_init } + +$state_i //rewrite to the name of state i + +$state_i_init //rewrite to: $2 $spec $u $state_i $4 + + +////////////////////////////// + +_safe = 0; +int __RVC_SeatBelt_unsafe = 0; + +void +__RVC_SeatBelt_reset(void) +{ + __RVC_state = 0; + } + +static int __RVC_SEATBELT_SEATBELTREMOVED[] = {-1,0, }; +static int __RVC_SEATBELT_SEATBELTATTACHED[] = {1, -1,}; + +void +__RVC_SeatBelt_seatBeltRemoved() +{ +{fprintf(stderr, "Seat belt removed.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTREMOVED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + +void +__RVC_SeatBelt_seatBeltAttached() +{ +{fprintf(stderr, "Seat belt attached.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTATTACHED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + + diff --git a/src/c-monitor-code-template/template.h.origin b/src/c-monitor-code-template/template.h.origin new file mode 100644 index 0000000..8c1dc40 --- /dev/null +++ b/src/c-monitor-code-template/template.h.origin @@ -0,0 +1,10 @@ +#ifndef __RVC_SEATBELT_MONITOR_H +#define __RVC_SEATBELT_MONITOR_H +void +__RVC_SeatBelt_reset(void); +void +__RVC_SeatBelt_seatBeltRemoved(); +void +__RVC_SeatBelt_seatBeltAttached(); + +#endif diff --git a/src/c-monitor-code-template/template.h.try b/src/c-monitor-code-template/template.h.try new file mode 100644 index 0000000..8c1dc40 --- /dev/null +++ b/src/c-monitor-code-template/template.h.try @@ -0,0 +1,10 @@ +#ifndef __RVC_SEATBELT_MONITOR_H +#define __RVC_SEATBELT_MONITOR_H +void +__RVC_SeatBelt_reset(void); +void +__RVC_SeatBelt_seatBeltRemoved(); +void +__RVC_SeatBelt_seatBeltAttached(); + +#endif diff --git a/src/common/java-bubble-syntax.k b/src/common/java-bubble-syntax.k index 8eca60a..84c2fc6 100644 --- a/src/common/java-bubble-syntax.k +++ b/src/common/java-bubble-syntax.k @@ -4,15 +4,17 @@ module JAVA-BUBBLE-SYNTAX imports PACKAGE-SYNTAX //syntax NoBracket ::= r"[^{}]+" [token] //temp workaround for https://github.com/kframework/k/issues/1863 - syntax NoBracket ::= r"[^<{}][^{}]*" [token, klabel('NoBracket)] + syntax NoBracket //::= r"[^<{}][^{}]*" [token, klabel('NoBracket)] + syntax EmptyBlock ::= "{" "}" [token, klabel(EmptyBlockLabel)] + syntax BalancedBracket ::= - "{" BalancedBracket "}" [klabel('BBracketBlock)] + "{" BalancedBracket "}" [klabel(BBracketBlockLabel)] | BalancedBracket BalancedBracket [left, klabel('BBracketCombination)] | NoBracket [klabel('BBracketAtom)] - | "{" "}" [klabel('BBracketEmpty)] + | EmptyBlock - syntax BlockBubble ::= "{" BalancedBracket "}" [prefer, token, klabel('BlockBubble)] - | "{" "}" [prefer, token, klabel('BlockBubbleEmpty)] + syntax BlockBubble //::= "{" BalancedBracket "}" [prefer, token, klabel('BlockBubble)] + // | "{" "}" [prefer, token, klabel('BlockBubbleEmpty)] syntax DecStart ::= IdModifier | IdModifier DecStart @@ -20,7 +22,7 @@ module JAVA-BUBBLE-SYNTAX syntax ClassDecBubble ::= DecStart BlockBubble - syntax ParamsBubble ::= r"\\([^\\)]*\\)" [token, avoid, klabel('ParamsBubble)] + syntax ParamsBubble //::= r"\\([^\\)]*\\)" [token, avoid, klabel('ParamsBubble)] syntax MethodDecBubble ::= DecStart ParamsBubble BlockBubble @@ -33,15 +35,15 @@ module JAVA-BUBBLE-SYNTAX //syntax VarInitBubble ::= r"[^;]+" [token, avoid] //temp workaround for https://github.com/kframework/k/issues/1863 - syntax VarInitBubble ::= r"[^<;][^;]*" [token, avoid, klabel('VarInitBubble)] + syntax VarInitBubble //::= r"[^<;][^;]*" [token, avoid, klabel('VarInitBubble)] - syntax DecBubble ::= ClassDecBubble [token, klabel('DecBubbleClass)] - | MethodDecBubble [token, klabel('DecBubbleMethod)] - | FieldDecBubble [token, klabel('DecBubbleField)] + syntax DecBubble //::= ClassDecBubble [token, klabel('DecBubbleClass)] + // | MethodDecBubble [token, klabel('DecBubbleMethod)] + // | FieldDecBubble [token, klabel('DecBubbleField)] //syntax NoParentheses ::= r"[^()]+" [token] //temp workaround for https://github.com/kframework/k/issues/1863 - syntax NoParentheses ::= r"[^()<][^()]*" [token, klabel('NoParentheses)] + syntax NoParentheses //::= r"[^()<][^()]*" [token, klabel('NoParentheses)] //| "<" [token, klabel('NoParenthesesSingleLT)] syntax BalancedParentheses ::= @@ -50,11 +52,12 @@ module JAVA-BUBBLE-SYNTAX | NoParentheses | "(" ")" - syntax BoolExpBubble ::= BalancedParentheses [token, klabel('BoolExpBubble)] //TODO:removed prefer (for MOP production), check amb + syntax BoolExpBubble //::= BalancedParentheses [token, klabel('BoolExpBubble)] //TODO:removed prefer (for MOP production), check amb - syntax DecBubbleList ::= List{DecBubble, ""} [token, klabel('DecBubbleList)] + syntax DecBubbleList // ::= List{DecBubble, ""} [token, klabel('DecBubbleList)] syntax JavaModifier ::= "abstract" | "final" | "interface" | "native" | "private" | "protected" | "public" | "static" | "strict" | "synchronized" | "transient" | "volatile" -endmodule \ No newline at end of file +endmodule + diff --git a/src/common/package-syntax.k b/src/common/package-syntax.k index 46192f5..8634c04 100644 --- a/src/common/package-syntax.k +++ b/src/common/package-syntax.k @@ -8,6 +8,12 @@ syntax ImportDec ::= "import" TypeName ";" [klabel('TypeImport | "import" "static" TypeName "." Id ";" [klabel('StaticImportDec)] | "import" "static" TypeName "." "*" ";" [klabel('StaticImportOnDemandDec)] +// //for c code + | "#include" "<" Id ".h" ">" [klabel('CInclude1)] + | "#include" String [klabel('CInclude2)] +// | "#include" "\"" Id ".h" "\"" [klabel('CInclude2)] + + syntax PackageDec ::= "package" PackageName ";" [klabel('PackageDec)] syntax OptionalPackageDec ::= PackageDec | None syntax None diff --git a/src/common/property-syntax.k b/src/common/property-syntax.k index b2778dc..9456f91 100644 --- a/src/common/property-syntax.k +++ b/src/common/property-syntax.k @@ -1,16 +1,17 @@ -require "../logic/logic-syntax.k" +require "../logic/syntax/logic-syntax.k" require "java-bubble-syntax.k" module PROPERTY-SYNTAX imports LOGIC-SYNTAX imports JAVA-BUBBLE-SYNTAX - syntax PropertyDec ::= Property HandlerDecList + syntax PropertyDec ::= Property | Property HandlerDecList syntax Property ::= LogicName ":" LogicFormula syntax HandlerDec ::= HandlerDecHead HandlerBody syntax HandlerDecHead ::= "@" LogicState syntax HandlerBody ::= BlockBubble - syntax HandlerDecList ::= List{HandlerDec, ""} [klabel('HandlerDecList)] + syntax HandlerDecList ::= List{HandlerDec, ""} [klabel(HandlerDecListFunc)] + syntax PropertyDecList ::= List{PropertyDec, ""} [klabel('PropertyDecList)] endmodule \ No newline at end of file diff --git a/src/common/type-syntax.k b/src/common/type-syntax.k index 083eb35..a23a3c3 100644 --- a/src/common/type-syntax.k +++ b/src/common/type-syntax.k @@ -2,20 +2,30 @@ require "domains.k" module TYPE-SYNTAX imports DOMAINS-SYNTAX - syntax PackageName ::= IdList [klabel('PackageName)] - syntax PackageOrTypeName ::= Id [klabel('PackageOrTypeName)] - | PackageOrTypeName "." Id [strict(1), klabel('PackageOrTypeName)] - syntax TypeName ::= Id [klabel('TypeName)] - | PackageOrTypeName "." Id [strict(1), klabel('TypeName)] + //syntax PackageName ::= IdList [klabel('PackageName)] + //syntax PackageOrTypeName ::= Id [klabel('PackageOrTypeName)] + // | PackageOrTypeName "." Id [strict(1), klabel('PackageOrTypeName)] + //syntax TypeName ::= Id [klabel('TypeName), avoid] //TODO: added avoid to resolve amb with K internal syntax in rules + // | PackageOrTypeName "." Id [strict(1), klabel('TypeName)] + + syntax PackageName ::= Id [klabel('PackageNameSingle), avoid] + | PackageName "." Id [strict(1), klabel('PackageNameMulti), avoid] + syntax TypeName ::= Id [klabel('TypeNameSingle), avoid] + | TypeName "." Id [klabel('TypeNameMulti), avoid] + +//PackageName [klabel('TypeName)] + + + syntax IdList ::= List{Id,"."} [klabel('IdList)] - syntax Dim ::= "[" "]" - syntax Dims ::= List{Dim, ""} - syntax ArrayType ::= Type "[" "]" + syntax Dim ::= "[]" + syntax Dims ::= Dim | Dim Dims + syntax ArrayType ::= Type Dim // "[" "]" syntax Type ::= TypeName | ArrayType - syntax VarDecId ::= Id Dims + syntax VarDecId ::= Id | Id Dims syntax Param ::= Type VarDecId syntax Params ::= List{Param, ","} [klabel('FormalParamList)] @@ -25,4 +35,4 @@ module TYPE-SYNTAX //context 'FormalParamList(_,,HOLE) [result(Params)] -endmodule \ No newline at end of file +endmodule diff --git a/src/helper/code-gen.k b/src/helper/code-gen.k new file mode 100644 index 0000000..f64c856 --- /dev/null +++ b/src/helper/code-gen.k @@ -0,0 +1,141 @@ +require "../rvm/rvm-syntax.k" +require "domains.k" + +module CODE-GEN + imports RVM-SYNTAX + imports DOMAINS-SYNTAX + +syntax String ::= staticIntPrefix(String) [function] +rule staticIntPrefix(Str:String) => "static int " +String Str + +syntax String ::= constPrefix(String) [function] +rule constPrefix(Str:String) => "const " +String Str + +syntax String ::= propertyPrefix(Int) [function] +rule propertyPrefix(I:Int) => "Prop_" +String Int2String(I) +String "_" + +syntax String ::= globalStateVarI(Int) [function] +rule globalStateVarI(I:Int) => propertyPrefix(I) +String "RVC_state" + +//the code for resetting global state var i +syntax String ::= resetGlobalStateI(Int) [function] +rule resetGlobalStateI(I:Int) => globalStateVarI(I) +String " = 0;\n" + + syntax String ::= getGlobalStateVarInit(Int) [function] + rule getGlobalStateVarInit(I:Int) => staticIntPrefix(resetGlobalStateI(I)) + + /*Return the string of reset function, given the name of the specification, + and the number of properties*/ + syntax String ::= printResetFunc(String, Int) [function] + syntax String ::= printResetFuncHeader(String, Int) [function] + +rule printResetFuncHeader(SpecName:String, I:Int) => "void __RVC_" +String SpecName + +String "_reset(void)" + + rule printResetFunc(SpecName:String, 0) => "" + + rule printResetFunc(SpecName:String, I:Int) => printResetFuncHeader(SpecName, I) + +String "\n{\n" +String resetGlobalStates(I) +String "}\n" + when I =/=Int 0 + + syntax String ::= resetGlobalStates(Int) [function] + rule resetGlobalStates(I:Int) => "" when I <=Int 0 + rule resetGlobalStates(1) => resetGlobalStateI(0) + rule resetGlobalStates(I:Int) => resetGlobalStates(I -Int 1) +String + resetGlobalStateI(I -Int 1) when I >Int 1 + +//////////////////////////////////////////////////////////////////////////////////// +///////////////The code for local state var initialization +//the three args are spec name, property rank and state name +syntax String ::= localStateVarI(String, Int, String) [function] +rule localStateVarI(SpecName:String, P:Int, StateName:String) => + SpecName +String "_" +String propertyPrefix(P) +String StateName + +syntax String ::= localStateVarInit(String, Int, String) [function] +rule localStateVarInit(SpecName:String, P:Int, StateName:String) => + ("int " +String localStateVarI(SpecName:String, P:Int, StateName:String) + +String " = 0;") +///////////////////Get the code of state transition functions/////////////////////// + +/*Return the state transition function for Spec S, property X, event E*/ +syntax String ::= propXEventE(String, Int, String) [function] +/*The version for spec which only has one property: the args are spec name s and event name e*/ +syntax String ::= propXEventE(String, String) [function] + +rule propXEventE(SpecName:String, X:Int, EventName:String) => + SpecName +String "_" +String propertyPrefix(X) +String EventName + +rule propXEventE(SpecName:String, EventName:String) => + SpecName +String "_" +String EventName + +syntax String ::= printIntArr(List) [function] +syntax String ::= addCurlyBraces(String) [function] +syntax String ::= printIntSeq(List) [function] + +rule addCurlyBraces(Str:String) => ("{" +String Str +String "}") + +rule printIntSeq(.List) => "" +rule printIntSeq(ListItem(I:Int)) => Int2String(I) +rule printIntSeq(ListItem(I:Int) ListItem(J:Int)) => + Int2String(I) +String ", " +String Int2String(J) +rule printIntSeq(ListItem(I:Int) ListItem(J:Int) L:List) => +Int2String(I) +String ", " +String Int2String(J) +String ", " +String printIntSeq(L) + +rule printIntArr(L:List) => addCurlyBraces(printIntSeq(L)) + +//args are spec name, property rank, event name and transition function array +syntax String ::= stateTransitionPropXEventE(String, Int, String, List) [function] +//only one property in the spec +syntax String ::= stateTransitionPropXEventE(String, String, List) [function] + +rule stateTransitionPropXEventE(Spec:String, X:Int, Event:String, L:List) + => (constPrefix(staticIntPrefix(propXEventE(Spec, X, Event))) + +String "[]= " +String printIntArr(L) +String ";") + +rule stateTransitionPropXEventE(Spec:String, Event:String, L:List) + => (constPrefix(staticIntPrefix(propXEventE(Spec, Event))) +String "[] = " + +String printIntArr(L) +String ";") + +////////////print method header given the spec name, event name and args +syntax String ::= printMethodHeader(String, String, String) [function] +rule printMethodHeader(SpecName:String, EventName:String, Args:String) + => "void __RVC_" +String SpecName +String "_" +String + EventName +String "(" +String Args +String ")" + +////////////the two args are global state var name and transition function name +syntax String ::= globalStateUpdate(String, String) [function] +rule globalStateUpdate(GSV:String, TF:String) => + GSV +String " = " +String TF +String "[" +String GSV +String "];" + +/////////////the three args are local state var, global state var, state rank +syntax String ::= localStateUpdate(String, String, Int) [function] +rule localStateUpdate(LSV:String, GSV:String, SR:Int) => + LSV +String " = " +String GSV +String " == " +String Int2String(SR) +String ";" + +//////////////////////////////////////////////////////////////////////////////// +//generate the event handler code +//the complete code will be generated by structural induction. +//given the , in the form of a map of (string |-> string) +//return the map of state name to handler code string +syntax List ::= getHandlerCode(Map) [function] + +//handling map +rule getHandlerCode(.Map) => .List + +rule getHandlerCode(K:String |-> V:String) => ListItem("if (" +String K +String ") {\n" + +String V +String "\n}") + +rule getHandlerCode((K:String |-> V:String) M:Map) => +ListItem("if (" +String K +String "){\n" +String V +String "\n}") +getHandlerCode(M) + +//wrap the given content with the C's header file's template +//two args are: 1) main part of the header file, 2) spec name +//the wrapper code will be generated based on the spec name +syntax String ::= addCTemplate(String, String) [function] +rule addCTemplate(Content:String, SpecName:String) + => "#ifndef __RVC_" +String SpecName +String "_MONITOR_H\n" + +String "#define __RVC_" +String SpecName +String "_MONITOR_H\n\n" ++String Content +String "\n\n#endif" + +endmodule \ No newline at end of file diff --git a/src/helper/print-ast.k b/src/helper/print-ast.k new file mode 100644 index 0000000..c5c1b6e --- /dev/null +++ b/src/helper/print-ast.k @@ -0,0 +1,140 @@ +require "../rvm/rvm-syntax.k" +require "../c-monitor-code-template/c-monitor-template-syntax.k" +require "domains.k" + +module PRINT-AST + imports RVM-SYNTAX + imports DOMAINS-SYNTAX + imports C-MONITOR-TEMPLATE-SYNTAX + + //print package ast + syntax String ::= PackageDec2String(OptionalPackageDec) [function] + rule PackageDec2String(package X:PackageName ;) => "package " +String PackageName2String(X) + +String ";" + rule PackageDec2String(None:OptionalPackageDec) => "\n" + + syntax String ::= PackageName2String(PackageName) [function] + rule PackageName2String(X:Id) => Id2String(X) + rule PackageName2String(P:PackageName . X:Id) => PackageName2String(P) +String "." +String Id2String(X) + + //get logic name + syntax LogicName ::= getLogicName(PropertyDec) [function] + rule getLogicName(LN:LogicName : F:LogicFormula HDL:HandlerDecList) => LN + + //get formula + syntax LogicFormula ::= getFormula(PropertyDec) [function] + rule getFormula(LN:LogicName : F:LogicFormula HDL:HandlerDecList) => F + + //get handlers of the given property + syntax HandlerDecList ::= getHandlers(PropertyDec) [function] + rule getHandlers(LN:LogicName : F:LogicFormula HDL:HandlerDecList) => HDL + + //get event name in string + syntax String ::= getEventName(EventName) [function] + rule getEventName(E:Id) => Id2String(E) + + //get state name from an item + syntax String ::= getStateName(Item) [function] + syntax String ::= printStateName(StateName) [function] + + syntax TransitionList ::= getTransitionList(Item) [function] + + rule getStateName(SN:StateName[TL:TransitionList]) => printStateName(SN) + rule printStateName(SN:Id) => Id2String(SN) + + rule getTransitionList(SN:StateName[TL:TransitionList]) => TL + +syntax Int ::= sizeOf(PropertyDecList) [function] +rule sizeOf(.PropertyDecList) => 0 +rule sizeOf(Prop:PropertyDec Props:PropertyDecList) => 1 +Int sizeOf(Props) + +//given the number of properties and events, generate a list of state transition functions, +//indexed by property rank and event rank +//the first two args are the current prop rank and event rank, the third and fourth args are the +//total number of properties and events resp. +syntax StateTransitions ::= getListofStateFuncs(Int, Int, Int, Int) [function] +rule getListofStateFuncs(I:Int, J:Int, PN:Int, EN:Int) => $emptyTransition +when I >=Int PN + +rule getListofStateFuncs(I:Int, J:Int, PN:Int, EN:Int) => getListofStateFuncs(I +Int 1, 0, PN, EN) +when I =Int EN + +rule getListofStateFuncs(I:Int, J:Int, PN:Int, EN:Int) => +($sFunc(I, J):StateFunc , getListofStateFuncs(I, J +Int 1, PN, EN)) +when I "" +rule Params2Str(P:Param) => Param2Str(P) +rule Params2Str(P:Param, .Params) => Param2Str(P) +rule Params2Str(P:Param, Ps:Params) => Param2Str(P) +String ", " +String Params2Str(Ps) + +rule Param2Str(T:Type V:VarDecId) => Type2Str(T) +String " " +String VarDecId2Str(V) + +//Type ::= TypeName | ArrayType +syntax String ::= TypeName2String(TypeName) [function] +syntax String ::= ArrayType2String(ArrayType) [function] + +rule Type2Str(T:TypeName) => TypeName2String(T) +rule Type2Str(AT:ArrayType) => ArrayType2String(AT) + +rule TypeName2String(X:Id) => Id2String(X) +rule TypeName2String(T:TypeName . X:Id) => TypeName2String(T) +String "." +String Id2String(X) + +rule ArrayType2String(T:Type []) => Type2Str(T) +String "[]" + +//VarDecId ::= Id Dims +syntax String ::= Dims2Str(Dims) +rule VarDecId2Str(X:Id) => Id2String(X) +rule VarDecId2Str(X:Id Ds:Dims) => Id2String(X) +String Dims2Str(Ds) +rule Dims2Str(D:Dim) => "[]" +rule Dims2Str(D:Dim Ds:Dims) => "[]" +String Dims2Str(Ds) + +/** +Print the method body. +*/ +syntax String ::= Block2Str(BlockBubble) +[function, hook(STRING.token2string), klabel(Block2StringFunc)] + +/**Get the state name from a handler dec head.*/ +syntax String ::= getStateNameOf(LogicState) [function] +rule getStateNameOf(fail) => "fail" +rule getStateNameOf(X:Id) => Id2String(X) + +/*Get the string of handler code*/ +syntax String ::= getHandlerCodeStr(HandlerBody) [function] +rule getHandlerCodeStr(BB:BlockBubble) => Block2Str(BB) + +/*Print the Decl list as string*/ +syntax String ::= declBubbleList2String(DecBubbleList) [function, hook(STRING.token2string)] + +/*Print import decl list as a string*/ +syntax String ::= importList2String(ImportDecList) [function] +syntax String ::= importDecl2String(ImportDec) [function] + +rule importList2String(.ImportDecList) => "\n" +rule importList2String(I:ImportDec) => importDecl2String(I) +String "\n" +rule importList2String(I:ImportDec IDL:ImportDecList) => importDecl2String(I) +String "\n" + +String importList2String(IDL) + +rule importDecl2String(import TN:TypeName ;) => "import " +String TypeName2String(TN) +String ";" +rule importDecl2String(import PN:PackageName .*;) => "import " +String PackageName2String(PN) + +String ".*;" +rule importDecl2String(import static TN:TypeName . X:Id ;) => "import static " +String + TypeName2String(TN) +String "." +String Id2String(X) +String ";" + +rule importDecl2String(import static TN:TypeName . * ;) => "import static " +String + TypeName2String(TN) +String ".*;" + +rule importDecl2String(#include ) => "#include <" +String Id2String(X) +String ".h>" + +rule importDecl2String(#include Str:String) => "#include \"" +String Str +String "\"" + +endmodule \ No newline at end of file diff --git a/src/helper/util.k b/src/helper/util.k new file mode 100644 index 0000000..ecbb01f --- /dev/null +++ b/src/helper/util.k @@ -0,0 +1,81 @@ +module UTIL + +/*This function takes an int -> int map as input, sort it via keys and return the values as a list* +* If an event does not map a given state to any normal state, then it maps to error state, +and the error state is by default having rank 'size' of the number of normal states*/ +/*The int represents the number of the states*/ +syntax List ::= toIntArray(Map, Int) [function] +rule toIntArray(M:Map, I:Int) => toIntArray(M, 0, I) + +/*The second int is the index of the current state, the third is the number of states.*/ +syntax List ::= toIntArray(Map, Int, Int) [function] + +rule toIntArray(M:Map, Cur:Int, Siz:Int) => ListItem(Siz) when Cur ==Int Siz + +rule toIntArray(M:Map, I:Int, Siz:Int) => + ListItem(M[I]) toIntArray(M, I +Int 1, Siz) + when I + ListItem(Siz) toIntArray(M, I +Int 1, Siz) + when I V:Int) M:Map, V) => S + +rule getStrKey((_:String |-> V1:Int) M:Map, V2:Int) => getStrKey(M, V2) +when V1 =/=Int V2 + +/*Get the size of the i-th map in the map list*/ +syntax Int ::= getSize(List, Int) [function] +rule getSize(.List, I:Int) => 0 +rule getSize(ListItem(M:Map), 0) => size(M) +rule getSize(ListItem(M:Map), I:Int) => 0 when I =/=Int 0 + +rule getSize(ListItem(M:Map) L:List, 0) => size(M) +rule getSize(ListItem(M:Map) L:List, I:Int) => getSize(L, I -Int 1) when I >Int 0 +rule getSize(ListItem(M:Map) L:List, I:Int) => 0 when I false +rule isLastItem(ListItem(X:String), Y:Id) => X ==String Id2String(Y) +rule isLastItem(ListItem(X:String) L:List, Y:Id) => isLastItem(L, Y) + +//get the no. i map in the map list +syntax Map ::= getMapI(List, Int) [function] +rule getMapI(.List, I:Int) => .Map +rule getMapI(ListItem(M:Map), 0) => M +rule getMapI(ListItem(M:Map), I:Int) => .Map when I =/=Int 0 + +rule getMapI(ListItem(M:Map) L:List, 0) => M +rule getMapI(ListItem(M:Map) L:List, I:Int) => .Map when I + getMapI(L, I -Int 1) when I >Int 0 + +//get the no. i id name in a string list +syntax String ::= getStringI(List, Int) [function] +rule getStringI(.List, I:Int) => "" +rule getStringI(ListItem(X:String), 0) => X +rule getStringI(ListItem(X:String), I:Int) => "" when I =/=Int 0 + +rule getStringI(ListItem(X:String) L:List, 0) => X +rule getStringI(ListItem(X:String) L:List, I:Int) => "" when I + getStringI(L, I -Int 1) when I >Int 0 + +//convert a list of strings into a single string +syntax String ::= StringList2String(List) [function] +rule StringList2String(.List) => "\n" +rule StringList2String(ListItem(S:String)) => S +String "\n" +rule StringList2String(ListItem(S:String) L:List) => S +String "\n" +String StringList2String(L) + + +endmodule + + diff --git a/src/logic/semantics/ere.k b/src/logic/semantics/ere.k new file mode 100644 index 0000000..0438de3 --- /dev/null +++ b/src/logic/semantics/ere.k @@ -0,0 +1,16 @@ +require "../syntax/ere-syntax.k" + +require "../../rvm/rvm-compiler-core.k" + + +module ERE + imports RVM-COMPILER-CORE + imports ERE-SYNTAX + +//test rule +rule + ere + _:EREFormula => .K + true + +endmodule \ No newline at end of file diff --git a/src/logic/semantics/fsm.k b/src/logic/semantics/fsm.k new file mode 100644 index 0000000..e557435 --- /dev/null +++ b/src/logic/semantics/fsm.k @@ -0,0 +1,166 @@ +require "../syntax/fsm-syntax.k" +require "../../rvm/rvm-compiler-core.k" + +require "../../helper/print-ast.k" +require "../../helper/util.k" + +module FSM + imports FSM-SYNTAX + imports RVM-COMPILER-CORE + imports PRINT-AST + imports UTIL + +/*First scan: Gathering the state ranks*/ +rule fsm + IT:Item IL:ItemList AL:AliasList => (IL AL) + true + CurMap:Map => CurMap[getStateName(IT) <- size(CurMap)] + 0 + +// if do not need this constraint, then comment the condition below as well as the next rule. + when notBool (getStateName(IT) in keys(CurMap)) + + //We may or may not forbid the behavior of defining transitions for the same state + //in multiple places + +rule fsm + IT:Item IL:ItemList AL:AliasList + CurMap:Map + true => false + 0 + (.List => ListItem("State " +String getStateName(IT) +String + " defined in multiple places")) ErrList:List +when (getStateName(IT) in keys(CurMap)) + +////////////////////////////////////////////////////////////////////////////////////////////////// +/*2nd scan starts: restore the formula for the second scan*/ +rule + fsm + .ItemList AL:AliasList => FC + FC:K + true + _:Int => -1 + 0 => 1 + +/*2nd scan: get the raw transition mapping associated with the current state +Inside the item: + +s0[e1 -> s1 +e2 -> s2] + +The raw transitions associated with state s0 is: e1 -> s1, e2 -> s2. +*/ +rule fsm + IT:Item IL:ItemList AL:AliasList => (IL AL) + I:Int => I +Int 1 + .K => getTransitionList(IT) + true + 1 + +/**consume the transition functions defined for the current state.*/ +/*Handle unknown event*/ +rule _ => .K + fsm + (E:EventName -> SN:StateName) TL:TransitionList + EL:List + 1 + (.List => ListItem("Undefined event " +String getEventName(E))) ErrList:List + true => false + when notBool (getEventName(E) in EL) + +/*Handle unknown state*/ +rule _ => .K + fsm + (E:EventName -> SN:StateName) TL:TransitionList + SM:Map + 1 + (.List => ListItem("Undefined state " +String printStateName(SN))) ErrList:List + true => false + when notBool (printStateName(SN) in keys(SM)) + +//////////////////////////////////////////////////////////////////// +/*Update the event transition function for event E and property P.*/ +rule fsm + P:Int + + (E:EventName -> SN:StateName) TL:TransitionList => TL + S1:Int + SM:Map (printStateName(SN):String |-> S2:Int):Map + + ... + + + E + + ... + + + P + (.Map => (S1 |-> S2):Map) M:Map + ... + + + ... + + + + ... + + 1 [prefer] + +//////////////////////////////////////////////// +///////////collect the handler info + +rule (@LS:LogicState HB:HandlerBody) HDL:HandlerDecList => HDL + P:Int + SN:String + HDM:Map (.Map => (localStateVarI(SN, P, getStateNameOf(LS)):String + |-> (getHandlerCodeStr(HB)):String ) ) + + +/////////////the three args are spec name, property rank and state name +// localStateVarI(SN, P, getStateNameOf(LS)) +//////////////////////////////////////////////// + +rule + fsm + .TransitionList => .K + true + 1 + +/*when all the computation related to the formula completes, +translate the transition function from map to int array*/ +rule fsm + AllStatesMap:Map + .ItemList .AliasList + .K + PN:Int + + N:Int => N +Int 1 + + + ... + PN + SM:Map + .List => toIntArray(SM, size(AllStatesMap)) + + 1 + true + +/*All the event transition functions have been generated, +stop the processing of the current property, +reset the cells and wait for the processing of the next property*/ +rule N:Int => 0 + _:K => .K + EL:List + true => false + SM:Map => .Map + _:Int => 0 + _:K => .K + _:K => .K + .HandlerDecList + SL:List (.List => ListItem(SM)) + +when N ==Int size(EL) + +endmodule \ No newline at end of file diff --git a/src/logic/boolop-syntax.k b/src/logic/syntax/boolop-syntax.k similarity index 100% rename from src/logic/boolop-syntax.k rename to src/logic/syntax/boolop-syntax.k diff --git a/src/logic/cfg-syntax.k b/src/logic/syntax/cfg-syntax.k similarity index 100% rename from src/logic/cfg-syntax.k rename to src/logic/syntax/cfg-syntax.k diff --git a/src/logic/ere-syntax.k b/src/logic/syntax/ere-syntax.k similarity index 100% rename from src/logic/ere-syntax.k rename to src/logic/syntax/ere-syntax.k diff --git a/src/logic/fsm-syntax.k b/src/logic/syntax/fsm-syntax.k similarity index 100% rename from src/logic/fsm-syntax.k rename to src/logic/syntax/fsm-syntax.k diff --git a/src/logic/logic-syntax.k b/src/logic/syntax/logic-syntax.k similarity index 100% rename from src/logic/logic-syntax.k rename to src/logic/syntax/logic-syntax.k diff --git a/src/logic/ltl-syntax.k b/src/logic/syntax/ltl-syntax.k similarity index 94% rename from src/logic/ltl-syntax.k rename to src/logic/syntax/ltl-syntax.k index da71423..8bb109a 100644 --- a/src/logic/ltl-syntax.k +++ b/src/logic/syntax/ltl-syntax.k @@ -2,6 +2,7 @@ require "domains.k" require "boolop-syntax.k" module LTL-SYNTAX + imports BOOL-SYNTAX imports DOMAINS-SYNTAX imports BOOLOP-SYNTAX @@ -9,9 +10,7 @@ syntax LogicName ::= "ltl" syntax LogicFormula ::= LTLFormula -syntax LTLFormula ::= - "true" - | "false" +syntax LTLFormula ::= Bool | EventName | "(" LTLFormula ")" [bracket] > "[]" LTLFormula diff --git a/src/logic/srs-syntax.k b/src/logic/syntax/srs-syntax.k similarity index 88% rename from src/logic/srs-syntax.k rename to src/logic/syntax/srs-syntax.k index 6ce93f8..af004c5 100644 --- a/src/logic/srs-syntax.k +++ b/src/logic/syntax/srs-syntax.k @@ -15,7 +15,7 @@ syntax SRSState ::= "succeed" | "fail" syntax Rule ::= SRSLeftHandSide "->" SRSRightHandSide -syntax SRSLeftHandSide ::= OptionalBegin SRSString OptionalEnd +syntax SRSLeftHandSide ::= OptionalBegin SRSString OptionalEnd [avoid] syntax SRSRightHandSide ::= SRSString | "#" SRSState | "#epsilon" syntax OptionalBegin ::= "^" | None diff --git a/src/mop/mop-compiler.k b/src/mop/mop-compiler.k index a502403..c297f45 100644 --- a/src/mop/mop-compiler.k +++ b/src/mop/mop-compiler.k @@ -3,10 +3,37 @@ require "domains.k" module MOP-COMPILER-SYNTAX imports MOP-SYNTAX + imports DOMAINS-SYNTAX + + syntax NoBracket ::= r"[^<{}][^{}]*" [token, klabel('NoBracket)] + syntax ParamsBubble ::= r"\\([^\\)]*\\)" [token, avoid, klabel('ParamsBubble)] + syntax VarInitBubble ::= r"[^<;][^;]*" [token, avoid, klabel('VarInitBubble)] + syntax NoParentheses ::= r"[^()<][^()]*" [token, klabel('NoParentheses)] + + syntax BoolExpBubble ::= BalancedParentheses [token, klabel('BoolExpBubble)] //TODO:removed prefer (for MOP production), check amb + + syntax DecBubbleList ::= List{DecBubble, ""} [token, klabel('DecBubbleList)] + + syntax DecBubble ::= ClassDecBubble [token, klabel('DecBubbleClass)] + | MethodDecBubble [token, klabel('DecBubbleMethod)] + | FieldDecBubble [token, klabel('DecBubbleField)] + + syntax BlockBubble ::= "{" BalancedBracket "}" [prefer, token, klabel('BlockBubble)] + | "{" "}" [prefer, token, klabel('BlockBubbleEmpty)] + + + + + + syntax IdPattern ::= //id with * and .. wildcards (it can start with * but not with .. , same about end) + // r"(? $PGM:MOP endmodule \ No newline at end of file diff --git a/src/mop/mop-syntax.k b/src/mop/mop-syntax.k index 097161d..ca006ca 100644 --- a/src/mop/mop-syntax.k +++ b/src/mop/mop-syntax.k @@ -9,7 +9,7 @@ module MOP-SYNTAX //top level sort (aka CompilationUnit) - syntax MOP ::= OptionalPackageDec ImportDecList SpecDec [prefer, klabel('MOP)] + syntax MOP ::= OptionalPackageDec ImportDecList SpecDec //[prefer, klabel('MOP)] diff --git a/src/mop/pointcut-syntax.k b/src/mop/pointcut-syntax.k index 9e00118..3ecfec0 100644 --- a/src/mop/pointcut-syntax.k +++ b/src/mop/pointcut-syntax.k @@ -53,10 +53,10 @@ module ASPECTJ-POINTCUT-SYNTAX syntax ModifiersPattern ::= ModifierList | "!" ModifierList - syntax IdPattern ::= //id with * and .. wildcards (it can start with * but not with .. , same about end) + syntax IdPattern// ::= //id with * and .. wildcards (it can start with * but not with .. , same about end) // r"(? substrString(Str, 0, Count) - -//@Retain the last Count chars in the string -syntax String ::= retainTail ( String, Int ) [function] -rule retainTail(Str:String, Count:Int) => substrString(Str, lengthString(Str) -Int Count, lengthString(Str)) - -//@Trim the first Count chars in the string -syntax String ::= trimHead ( String, Int ) [function] -rule trimHead(Str:String, Count:Int) => substrString(Str, Count, lengthString(Str)) - -//@Trim the last Count chars in the string -syntax String ::= trimTail ( String, Int ) [function] -rule trimTail(Str:String, Count:Int) => substrString(Str, 0, lengthString(Str) -Int Count) - -syntax String ::= lastChar ( String ) [function] -rule lastChar(Str:String) => retainTail(Str, 1) - -endmodule diff --git a/src/old/java/class-syntax.k b/src/old/java/class-syntax.k deleted file mode 100644 index 6f3ab3e..0000000 --- a/src/old/java/class-syntax.k +++ /dev/null @@ -1,134 +0,0 @@ -module CLASS-SYNTAX - imports EXP-SYNTAX - -//@ \subsection{ClassDeclarations.sdf} -syntax ClassDecHead ::= - AnnoClassModList "class" Id OptionalTypeParams OptionalSuper OptionalInterfaces - [klabel('ClassDecHead)] -syntax ClassBody ::= "{" ClassBodyDecList "}" [klabel('ClassBody)] - -syntax ClassDec ::= ClassDecHead ClassBody [klabel('ClassDec)] -syntax ClassDec ::= EnumDec - -syntax ClassMod ::= Public - | Private - | Protected - | Abstract - | Final - | Static - | StrictFP - -z - -syntax AnnoClassMod ::= Anno | ClassMod - -syntax Super ::= "extends" JavaClassType [klabel('SuperDec)] - -syntax Interfaces ::= "implements" InterfaceTypeList [klabel('ImplementsDec)] - -syntax ClassBodyDec ::= InstanceInit | StaticInit | ClassMemberDec | ConstrDec - -syntax ClassMemberDec ::= FieldDec | ClassDec | MethodDec | InterfaceDec | SemiColon - -syntax InterfaceDec - -syntax SemiColon ::= ";" [klabel('SemiColon)] - -//@ \subsection{ConstructorDeclarations.sdf} -syntax ConstrHead ::= - AnnoConstrModList OptionalTypeParams Id "(" Params ")" OptionalThrows - [klabel('ConstrDecHead)] -syntax ConstrBody ::= "{" OptionalConstrInv BlockStmList "}" [klabel('ConstrBody)] - -syntax ConstrDec ::= ConstrHead ConstrBody [klabel('ConstrDec)] - -syntax ConstrInv ::= OptionalTypeArgs "this" "(" Exps ")" ";" [klabel('AltConstrInv)] -syntax ConstrInv ::= OptionalTypeArgs "super" "(" Exps ")" ";" [klabel('SuperConstrInv)] -syntax ConstrInv ::= Exp "." OptionalTypeArgs "super" "(" Exps ")" ";" [klabel('QSuperConstrInv)] - -syntax ConstrMod ::= Public - | Private - | Protected - -syntax AnnoConstrMod ::= Anno | ConstrMod - - -//@ \subsection{EnumDeclarations.sdf} -syntax EnumDecHead ::= AnnoClassModList "enum" Id OptionalInterfaces [klabel('EnumDecHead)] -/* -Java allows , at the end of List. -This makes copy-pasting easier, especially with one element per line. -*/ -syntax EnumBody ::= "{" EnumConstList OptionalEnumBodyDecs"}" [klabel('EnumBody)] - | "{" EnumConstList "," OptionalEnumBodyDecs "}" [klabel('EnumBody)] - -syntax EnumDec ::= EnumDecHead EnumBody [klabel('EnumDec)] - -syntax EnumConst ::= Id OptionalEnumConstArgs OptionalClassBody [klabel('EnumConst)] - -syntax EnumConstArgs ::= "(" Exps ")" [bracket] - -syntax EnumBodyDecs ::= ";" ClassBodyDecList [klabel('EnumBodyDecs)] - - -//@ \subsection{FieldDeclarations.sdf} -syntax FieldDec ::= AnnoFieldModList Type VarDecList ";" [klabel('FieldDec)] - -syntax VarDec ::= VarDecId [klabel('VarDec)] - | VarDecId "=" VarInit [klabel('VarDec)] - -syntax VarDecId ::= Id | Id Dims [klabel('ArrayVarDecId)] - -syntax VarInit ::= Exp | ArrayInit - -syntax FieldMod ::= Public - | Private - | Protected - | Final - | Static - | Transient - | Volatile - -syntax AnnoFieldMod ::= Anno | FieldMod - - -//@ \subsection{MethodDeclarations.sdf} -syntax MethodDecHead ::= - AnnoMethodModList OptionalTypeParams Type Id "(" Params ")" OptionalThrows - [klabel('MethodDecHead)] -syntax MethodBody ::= Block | ";" [klabel('NoMethodBody)] -syntax MethodDec ::= MethodDecHead MethodBody [klabel('MethodDec)] - -syntax Param ::= AnnoVarModList Type VarDecId [strict(2), klabel('Param)] -syntax Param ::= AnnoVarModList Type "..." VarDecId [klabel('VarArityParam)] - -syntax Throws ::= "throws" ExceptionTypeList [klabel('ThrowsDec)] - -syntax ExceptionType ::= JavaClassType - -syntax MethodMod ::= Public - | Private - | Protected - | Abstract - | Final - | Static - | Native - | Synchronized - | StrictFP - -syntax AnnoMethodMod ::= Anno | MethodMod - -syntax VarMod ::= Final - -syntax AnnoVarMod ::= Anno | VarMod - - -//@ \subsection{InstanceInitializers.sdf} -syntax InstanceInit ::= Block [klabel('InstanceInit)] - - -//@ \subsection{StaticInitializers.sdf} -syntax StaticInit ::= "static" Block [klabel('StaticInit)] -syntax Block - -endmodule \ No newline at end of file diff --git a/src/old/java/core-classes.k b/src/old/java/core-classes.k deleted file mode 100644 index 0ea0804..0000000 --- a/src/old/java/core-classes.k +++ /dev/null @@ -1,81 +0,0 @@ -module CORE-CLASSES - imports CORE-SORTS - imports CORE-FUNCTIONS - imports AUX-STRINGS // for retainHead - imports EXP-SYNTAX //for definitions of sort Exp - imports STMT-SYNTAX //for definitions of sort Stmt - -//@ \subsection{Packages} - -/*@A Java package.*/ -syntax PackageId ::= packageId ( Id ) -syntax MKR ::= PackageId - -/*@ Converts a term of type ClassType into a term of type PackageId representing this class. - This is the package for this class' inner classes. -*/ -syntax KItem ::= toPackage ( ClassType ) [function] -rule toPackage(class Class:Id) => packageId(Class) - -/*@Returns the package of the given class*/ -syntax KItem ::= getPackage ( K ) [strict] -rule getPackage(class ClassId:Id) - => packageId( String2Id(retainHead( - Id2String(ClassId), - rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) - )) ) - -//@ \subsection{Classes} - -//@ Converts a pair of PackagId, Id into a fully qualified class name -syntax ClassType ::= getClassType ( - PackageId, // the Package Id - Id // Simple class name - ) - [function] - -rule getClassType(packageId(PackKId:Id), SimpleClass:Id) - => class String2Id(Id2String(PackKId) +String "." +String Id2String(SimpleClass)) - -/*@Returns the top-level class enclosing this class*/ -syntax KItem ::= getTopLevel ( ClassType ) - -rule [getTopLevel-move-up]: - - getTopLevel(Class:ClassType) => getTopLevel(EnclosingClass) - ... - - Class - EnclosingClass:ClassType -when EnclosingClass =/=K noClass - -rule [getTopLevel]: - - getTopLevel(Class:ClassType) => Class - ... - - Class - noClass - -//@ Restore the content of with the given class -syntax KItem ::= restoreCrntClass ( - ClassType //old content of - ) - -rule [restoreAfterProcessLocalClass]: - restoreCrntClass(Class:ClassType) => . ... - _ => Class - -//@ Get the internal constructor name for a given class -syntax KItem ::= getConsName ( ClassType ) [function] -rule getConsName(class ClassId:Id) => String2Id("$cons$" +String Id2String(ClassId)) - - -//@ Since RawVal terms can easily be converted into TypedVal, they are also of sort Exp. -syntax Exp ::= TypedVal | RawVal - - - - - -endmodule diff --git a/src/old/java/core-functions.k b/src/old/java/core-functions.k deleted file mode 100644 index 25d2716..0000000 --- a/src/old/java/core-functions.k +++ /dev/null @@ -1,296 +0,0 @@ -module CORE-FUNCTIONS - imports CORE-SORTS - imports AUX-STRINGS - imports JAVA-SYNTAX - -//@ \subsection{Shortcuts for the most frequently used classes within the semantics} - -syntax ClassType ::= "classObject" - [function, latex(\terminal{Object})] -rule classObject => class String2Id("java.lang.Object") - -syntax ClassType ::= "classString" - [function, latex(\terminal{String})] -rule classString => class String2Id("java.lang.String") - -syntax ClassType ::= "classNullPointerException" - [function, latex(\terminal{NullPointerException})] -rule classNullPointerException => class String2Id("java.lang.NullPointerException") - -syntax ClassType ::= "classArrayImpl" [function] -rule classArrayImpl => class String2Id("java.lang.ArrayImpl") - -//@ \subsubsection{Computation terms produced during elaboration} -/*@ These auxiliary terms functions that should be threated as expressions in the elaboration phase. -*/ -syntax Exp ::= LHS -syntax LHS ::= AuxTermExp -/*@ Wrapper of a statement followed by an expression, to be used in a place where an expression is expected, -such as an anonymous class declaration. Is typed with the type of the expression. -At runtime is rewritten into the statement, that should evaluate into .K, followed by the expression, -that should evaluate to value.*/ -syntax AuxTermExp ::= stmtAndExp ( K, K ) - -syntax AuxTermExp ::= cast ( Type, K ) [strict] //strictness on 1-st arcument - for runtime produced terms - -/*@ Returns the type associated with various K terms. The implementation is scattered among various K files. - For a type - the type itself. For a typed expression - the type component. For some raw values - their most common - type. -*/ -syntax KItem ::= typeOf ( K ) [function] -rule typeOf(T:Type) => T -rule typeOf(_ :: T:Type) => T -rule typeOf(Str:String) => classString -rule typeOf(null) => nullType -rule typeOf(objectRef(_, Class:ClassType)) => Class -rule typeOf(arrayRef( arrayOf T:Type, _, _)) => arrayOf T - -/* Required by getTypes in elaboration phase, invoked by lookupMethod. */ -rule typeOf(cast(T:Type, _)) => T - -// Required for getTypes() -rule typeOf('Param(_:K,, T:Type,, _:Id)) => T - -/*@The default value for all types. Used for field initializers.*/ -syntax KItem ::= default ( Type ) [function] -rule default(IntT:IntType) => 0 :: IntT -rule default(FloatT:FloatType) => 0.0 :: FloatT -rule default(bool) => false :: bool -rule default(RT:RefType) => null :: RT - -/*@ Whenever naked RawVal reaches the top of computation, it have to be converted into TypedVal */ -rule Val:RawVal => toTypedVal(Val) [structural] - -/*@ Converts a RawVal into a TypedVal, by adding a default type for the given value. - Greatly simplifies many rules, because now we can use raw values in the RHS, instead of typed values. - - Have to be [function] for LTL -*/ -syntax KItem ::= toTypedVal ( RawVal ) [function] -rule toTypedVal(I:Int) => I :: int [structural] -rule toTypedVal(B:Bool) => B :: bool [structural] -rule toTypedVal(Str:String) => Str :: classString [structural] -rule toTypedVal(null) => null :: nullType [structural] -rule toTypedVal( objectRef(OL:Int, Class:ClassType) ) - => objectRef(OL:Int, Class:ClassType) :: Class [structural] - -rule toTypedVal(arrayRef(T:Type, L:Int, M:Int)) => arrayRef(T, L, M) :: T [structural] -rule toTypedVal(F:Float) => F :: float [structural] - -//@ Converts a KList of terms to Types. Uses typeOf underneath.todo repitition -syntax KItem ::= getTypes ( Exps ) [function] // a list of source expressions - | getTypes ( Types, Exps ) [function] - -rule getTypes( Ps:Exps ) => getTypes(types(.KList), Ps) -rule getTypes( types(Ts:KList), (T:Exp, Ps:Exps) ) => getTypes( types(Ts,,typeOf(T)), Ps ) -rule getTypes( types(Ts:KList), .Exps) => types(Ts) - -//@ Converts a TypedVals term to Types. Uses typeOf underneath. -syntax KItem ::= getTypes ( TypedVals ) [function] // a list of source values - | getTypes ( Types, TypedVals ) [function] - -rule getTypes( TVs:TypedVals) => getTypes(types(.KList), TVs) -rule getTypes( types(Ts:KList), (_ :: T:Type, TVs:TypedVals) ) => getTypes( types(Ts,,T), TVs ) -rule getTypes( types(Ts:KList), .TypedVals) => types(Ts) - -syntax KItem ::= getTypes ( Params ) [function] - | getTypes ( Types , Params ) [function] - -rule getTypes( Ps:Params ) => getTypes(types(.KList), Ps) -rule getTypes( types(Ts:KList), (_:AnnoVarModList T:Type _:Id , Ps:Params) ) => getTypes( types(Ts,,T), Ps ) -rule getTypes( types(Ts:KList), .Params) => types(Ts) - -//@ \subsubsection{Other auxiliary constructs} - -/*@ Generalized equality with strictness, suitable to compare not only TypedVal-s but any K terms. -*/ -syntax KItem ::= eqAux ( K, K ) [seqstrict] -rule eqAux(KR1:KResult, KR2:KResult) => KR1 ==K KR2 - -/*@ Alternative version of if, to be used whenever semantics needs an if logic. - The original 'If will only be used in the source programs.*/ -syntax KItem ::= ifAux ( K, K, K ) [strict(1)] -rule ifAux(true::bool, S:K, _) => S -rule ifAux(false::bool, _, S:K) => S - -syntax KItem ::= andAux(K, K) [strict(1)] -rule andAux(true::bool, E:K) => E -rule andAux(false::bool, _) => false - -syntax KItem ::= orAux(K, K) [strict(1)] -rule orAux(true::bool, _) => true -rule orAux(false::bool, E:K) => E - -//@ Replaces 'Plus in preprocessing phases -syntax KItem ::= plusAux( K, K ) [strict] -rule plusAux(Str1:String :: _, Str2:String :: _) => (Str1 +String Str2) :: classString - -/*@ A wrapper for maps. Allows holding maps inside an arbitrary expression where a K term is required. - Also used as part of mapUnion operation in PROCESS-CLASS-MEMBERS -*/ -syntax MKR ::= mapWrap ( Map ) - -/*@ The union of two maps. Arguments are of the form mapWrap(Map). In this operation, elements of the second map - overwrite elements of the first map if they collide. -*/ -syntax KItem ::= mapUnion ( - K, //mapWrap(Map) - K //mapWrap(Map) - ) - [strict] - -rule mapUnion(mapWrap( M1:Map => M1[K1 <- K2] ), mapWrap( _:Map (K1:K |-> K2:K => .Map) )) -rule mapUnion(mapWrap(M1:Map), mapWrap(.Map)) => mapWrap(M1) - -//@ Substracts from the given map the value given (match is on the value), may cause infinite loop if not used in the right place -syntax KItem ::= removeMapItemsByValue (Map,K) [function] - | removeMapItemsByValue (Map,K,Map) [function] - | removeMapItemsByValue (K,K,Map,K,Map) [function] - -rule removeMapItemsByValue(M:Map, V:K) => removeMapItemsByValue(M, V, .Map) -rule removeMapItemsByValue((Key:K |-> Value:K) Remains:Map, V:K, M:Map) => removeMapItemsByValue(Key, Value, Remains, V, M) -rule removeMapItemsByValue(Key:K, V, Remains:Map, V:K, M:Map) => removeMapItemsByValue(Remains, V, M) -rule removeMapItemsByValue(Key:K, Value:K, Remains:Map, V:K, M:Map) => removeMapItemsByValue(Remains, V, M (Key |-> Value)) -when Value =/=K V -rule removeMapItemsByValue(.Map, V:K, M:Map) => M - -//todo how to realise non-determinism: remove an arbitrary item with that value -syntax KItem ::= removeOneMapItemByValue (Map,K) [function] - | removeOneMapItemByValue (Map,K,Map) [function] - | removeOneMapItemByValue (K,K,Map,K,Map) [function] - -rule removeOneMapItemByValue(M:Map, V:K) => removeOneMapItemByValue(M, V, .Map) -rule removeOneMapItemByValue((Key:K |-> Value:K) Remains:Map, V:K, M:Map) => removeOneMapItemByValue(Key, Value, Remains, V, M) -rule removeOneMapItemByValue(Key:K, V, Remains:Map, V:K, M:Map) => Remains M -rule removeOneMapItemByValue(Key:K, Value:K, Remains:Map, V:K, M:Map) => removeOneMapItemByValue(Remains, V, M (Key |-> Value)) -when Value =/=K V -rule removeOneMapItemByValue(.Map, V:K, M:Map) => M - -//@ Find map items by partial key, not used now -syntax KItem ::= mapItemsByPartialKey (Map,K) [function] - | mapItemsByPartialKey (Map,K,Map) [function] - | mapItemsByPartialKey (K,K,Map,K,Map) [function] - -rule mapItemsByPartialKey(M:Map, V:K) => mapItemsByPartialKey(M, V, .Map) -rule mapItemsByPartialKey((Key:K |-> Value:K) Remains:Map, V:K, M:Map) => mapItemsByPartialKey(Key, Value, Remains, V, M) -rule mapItemsByPartialKey(sig(I:Id, T:Types), Value:K, Remains:Map, I, M:Map) - => mapItemsByPartialKey(Remains, I, M (sig(I,T) |-> Value)) -rule mapItemsByPartialKey(sig(I:Id, T:Types), Value:K, Remains:Map, V:K, M:Map) => mapItemsByPartialKey(Remains, V, M) -when I =/=K V -rule mapItemsByPartialKey(.Map, V:K, M:Map) => M - -syntax KItem ::= isEmpty( Map ) [function] -rule isEmpty(.Map) => true -rule isEmpty(_) => false [owise] - -/*@A wrapper for sets, similar to the one for maps.*/ -syntax MKR ::= setWrap ( Set ) - -/*The union of two sets. Arguments are of the form setWrap(Set).*/ -syntax KItem ::= setUnion ( - K, //setWrap(Set) - K //setWrap(Set) - ) - [strict] -rule setUnion(setWrap(S1:Set), setWrap(S2:Set)) => setWrap(S1 S2) - -syntax Set ::= getSet ( K ) [function] -rule getSet(setWrap(S1:Set)) => S1 - -/*@ the concatenation of two kr[KList] items */ -syntax KItem ::= klistConcat ( KRListWrap, KRListWrap ) [strict] -rule klistConcat(kr[KL1:KList], kr[KL2:KList]) => kr[KL1,,KL2] - -//@ Counts the number of elements in the KList list. Evaluates to an Int. -syntax KItem ::= length ( KListWrap ) [function] - | length ( Int, KListWrap ) [function] - -rule length([Ks:KList]) => length(0, [Ks]) -rule length(I:Int, [K:K,, Ks:KList]) => length(I +Int 1, [Ks]) -rule length(I:Int, [.KList]) => I - -//syntax KItem ::= getFirstKListElements( KListWrap ) [function] -// | getFirstKListElements( KListWrap, KListWrap ) [function] -// -//rule getFirstKListElements([Kl:KList]) => getFirstKListElements([Kl],,[.KList]) -//rule getFirstKListElements([Ho:K,, Hd:K,, Tl:KList], [Kl:KList]) => getFirstKListElements([Hd,,Tl],[Kl,,Ho]) -//rule getFirstKListElements([Hd:K,, .KList],, [Kl:KList]) => Kl -//rule getFirstKListElements([.KList],, [.KList]) => .KList - -syntax KItem ::= getLastKListElement( KListWrap ) [function] - -rule getLastKListElement([Ho:K,, Hd:K,, Tl:KList]) => getLastKListElement([Hd,,Tl]) -rule getLastKListElement([Hd:K,, .KList]) => Hd -rule getLastKListElement([.KList]) => .K - -syntax Params ::= addElementToParamsEnd (Params, Param) [function] -rule addElementToParamsEnd(.Params, P:Param) => P,.Params -rule addElementToParamsEnd((Hd:Param, Tl:Params), P:Param) => Hd,addElementToParamsEnd(Tl,P) - -syntax ClassBodyDecList ::= addElementToClassBodyDecListEnd (ClassBodyDecList, ClassBodyDec) [function] -rule addElementToClassBodyDecListEnd(.ClassBodyDecList, P:K) => 'ClassBodyDecList(P,, .ClassBodyDecList) -rule addElementToClassBodyDecListEnd('ClassBodyDecList(Hd:K,,Tl:K), P:K) => 'ClassBodyDecList(Hd,, addElementToClassBodyDecListEnd(Tl,P)) - -syntax ClassBodyDecList ::= appendClassBodyDecList(ClassBodyDecList, ClassBodyDecList) [function] -rule appendClassBodyDecList(CBDs:ClassBodyDecList, (Hd:ClassBodyDec Tl:ClassBodyDecList)) => - appendClassBodyDecList(addElementToClassBodyDecListEnd(CBDs, Hd), Tl) -rule appendClassBodyDecList(CBDs:ClassBodyDecList, .ClassBodyDecList) => CBDs - -syntax BlockStmList ::= addElementToBlockStmListEnd (BlockStmList, BlockStmt) [function] -rule addElementToBlockStmListEnd(.BlockStmList, P:K) => 'BlockStmList(P,, .BlockStmList) -rule addElementToBlockStmListEnd('BlockStmList(Hd:K,,Tl:K), P:K) => 'BlockStmList(Hd,, addElementToBlockStmListEnd(Tl,P)) - -syntax Exps ::= addElementToExpsEnd (Exps, Exp) [function] -rule addElementToExpsEnd(.Exps, P:Exp) => P,.Exps -rule addElementToExpsEnd((Hd:Exp, Tl:Exps), P:Exp) => Hd,addElementToExpsEnd(Tl,P) - -syntax Exps ::= appendExps(Exps, Exps) [function] -rule appendExps(AExps:Exps, (Hd:Exp, Tl:Exps)) => appendExps(addElementToExpsEnd(AExps, Hd), Tl) -rule appendExps(AExps:Exps, .Exps) => AExps - -/*@ \subsection{ClassType functions} */ - -//@ Converts a fully qualified class type into a simple name (Id) -syntax KItem ::= getSimpleName ( ClassType ) [function] -rule getSimpleName(class ClassId:Id) - => String2Id(trimHead( - Id2String(ClassId), - rfindString(Id2String(ClassId), ".", lengthString(Id2String(ClassId))) +Int 1 - )) - -/*@ \subsection{Identifiers}*/ - -// 'Id(Str:String) - -/*@Convert the AST representation of an Id into a K Id.*/ -rule 'Id(Str:String) => String2Id(Str) [structural, anywhere] - -/*@ \subsection{Other auxiliary constructs} */ - -/*@ \texttt{Generic guard.} - A generic computational guard (should be builtin): it allows the computation to continue only if a prefix - guard evaluates to true. -*/ -syntax KItem ::= "true?" -rule true::bool ~> true? => . [structural] - -//@ \subsection{Definition-wide rules} - -/*@ Represent a parser form for a sequence of terms. Is desugared into the pretty form [...]*/ -syntax KLabel ::= "'ListWrap" -rule 'ListWrap(Ks:KList) => [Ks] [structural, anywhere] -syntax KListWrap ::= "[" KList "]" [klabel('KListWrap), latex(\terminal{[} {#1} \terminal{]})] - - -//@ Sequence of terms and of any other statements. The first term is moved to the top of computation. -rule [S1:K,, Stmts:KList] => S1 ~> [Stmts] [structural] -rule [.KList] => .K [structural] - -rule 'ClassBodyDecList(Hd:K,,Tl:K) => Hd ~> Tl -rule .ClassBodyDecList => . - -//@ A wrapper over an arbitrary KList, wrapper being of type KResult. -syntax KRListWrap ::= "kr" "[" KList "]" [latex(\terminal{kr[} {#1} \terminal{]})] -syntax MKR ::= KRListWrap - -endmodule diff --git a/src/old/java/core-sorts.k b/src/old/java/core-sorts.k deleted file mode 100644 index d76c69c..0000000 --- a/src/old/java/core-sorts.k +++ /dev/null @@ -1,217 +0,0 @@ -//@ \section{Module CORE-SORTS} -module CORE-SORTS - imports TYPE-SYNTAX - -//@ \subsection{Computation phases} - -/*@ The computation Global Phase. See configuration documentation for details. -*/ -syntax GlobalPhase ::= - /* The content of is computed, of type - Map[PackageName -> Map[SimpleName -> FullyQualifiedName]] - */ - "ProcTypeNamesPhase" - - /* Primary processing of type declarations, including nested. - For each 'ClassDec a is saved, with the following cells: - - - - - - - - imports of the enclosing CU, for top-level classes only. - A class first registered in a cell is in the state StoredCPhase. - */ - | "ProcCompUnitsPhase" - - /* Resolve the fully qualified names of base classes an interfaces. Fills the content of: - - the base class - - the set of directly implemented interfaces - - the map from simple names to full names for use within this class. - */ - | "ProcClassDecsPhase" - - /* Saves into appropriate cells the list of transitively implemented interfaces, and all the - content about this class members. Computes the following cells: - - - - - - temporary cell, deleted after class body is processed. - - - */ - | "ProcClassMembersPhase" - - /* Elaborates the content of each code block. Specifically the content of the following cells: - - - The following transformations over expressions are performed: - - each name is resolved to its specific meaning - fully qualified class name, local variable name, static/instance - field of a specific class, etc. - - for each method call the precise signature is resolved. - - each unqualified method/constructor call is converted into a qualified one with the appropriate qualifier - (that might be empty) - - each expression is elaborated into a typed expression. - */ - | "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" - -/*@ the class phase. See configuration documentation for details.*/ -syntax ClassPhase ::= - "DiscoveredCPhase" - | "StoredCPhase" - | "BasesResolvedCPhase" - | "DecsProcessedCPhase" - | "MembersProcessedCPhase" - | "FoldedCPhase" - | "UnfoldingStartedCPhase" - | "UnfoldedCPhase" - -/*@ - The state of a class in relation to static initialization. See static-init.k for more details. -*/ -syntax StaticInitStatus ::= "StaticUninitialized" - | StaticInitializing ( Int ) - | "StaticInitialized" - - -/*@ A method signature. Required to be KResult by rules in METHOD-INVOKE.*/ -syntax Signature ::= sig ( Id, Types ) -syntax MKR ::= Signature - -/*@ The member accessibility context of the current method - either static or instance.*/ -syntax ContextType ::= "staticCT" [latex(\terminal{static})] - | "instanceCT" [latex(\terminal{instance})] - -syntax MKR ::= ContextType - -//@ \subsection{Values} - -/* Represents a java value. May be either primitive - int, float, bool, of reference. The values nothing and undefined - are special cases required by the semantics. The value nothing is associated with the return type void. The value - undefined is the initial value of uninitialized local variables, before the first assignment. -*/ -syntax RawVal ::= Int | Float | Bool | RawRefVal - | "nothing" - | "undefined" [latex(\bot)] - -/*@ A reference value, in its four forms - as regular object, array, null or String. As mentioned previously - String values have special treatment in this semantics and are implemented as regular strings. - -The object closure has the following structure: -\begin{itemize} -\item OL:Int -- the object location -\item List -- the object content, of the form -\begin{verbatim} - ListItem(layer( - Class, - Env, - enclosingObjClosure::T - )) - ... -\end{verbatim} -\end{itemize} -*/ -syntax ObjectRef ::= objectRef ( - Int, //OL - object location - ClassType //LowestClass - the lowest class where we are allowed to search for method - // implementation, or actual object class if there are no restrictions. - ) - -/*@ The arrayRef has the following structure: -\begin{itemize} -\item Type -- type of the array -\item Int -- location of the first element -\item Int -- array length -\end{itemize} -*/ -syntax ArrayRef ::= arrayRef ( - Type, // Type of the array - Int, // Location of the first element - Int // Length - ) - -syntax RawRefVal ::= ObjectRef | ArrayRef | String | NullLiteral - -/*@ A typed value is a pair of of a raw value and a type. Anywhere during execution we will evaluated typed expressions - into typed values, never into raw values alone. -*/ -syntax TypedVal ::= RawVal "::" Type -syntax TypedVals ::= List{TypedVal, ","} [klabel('ExprList)] -syntax Exps ::= TypedVals - -/*@ The three most common forms of computation result are Typed value or Type. Those are most common results - we will encounter during elaboration. Other result types are more context-specific. -*/ -syntax MKR ::= TypedVal | Type - -/*@ Member access modes*/ -syntax AccessMode ::= Public | Protected | Private | "package" -syntax MKR ::= AccessMode - -syntax AnnoMethodModList ::= accCT(AccessMode, ContextType) -/*@ Types of routines represented by a method closure*/ -syntax MethodMetaType ::= "methodMMT" | "constructorMMT" - -/*@ The two possibilities for a type represented by an objectRef: class or interface.*/ -syntax ClassMetaType ::= "classCMT" [latex(\terminal{class})] - | "interfaceCMT" [latex(\terminal{interface})] - -syntax NoValue ::= "noValue" [latex({\dotCt{K}})] -syntax MKR ::= NoValue -syntax KResult ::= MKR -syntax ElabKResult ::= MKR - -/*@ Represents a reference to a method or constructor. */ -syntax MethodRef ::= methodRef( - Signature, //Method signature - RefType //Usually Class - class defining the method - // Could also be array type, because we may invoke methods over arrays. - ) - | "noMethodRef" [latex({\dotCt{K}})] -syntax MKR ::= MethodRef -syntax MethodName ::= MethodRef - -/*@ A list of types. Elements are of sort Type. Used especially to denote argument types of a method.*/ -syntax Types ::= types ( - KList // List of Type elements, when processed - ) -syntax MKR ::= Types - -//Location type of each store location - either local variable or field -syntax LocMetadata ::= "LocalLocMetadata" [latex(\terminal{Local})] - | "FieldLocMetadata" [latex(\terminal{Field})] - -//Denis' syntax -syntax ClassOrName ::= Id | ClassType -//Denis' syntax -syntax ClassType ::= "class" Id | "noClass" [latex({\dotCt{K}})] - -/* Denis' syntax: A reference type is either a class type, an array type, the null type or a String type. -The null type is specified by the JLS although inaccessible to the programmer. String objects and -types are not threated as regular objects in the present semantics for performance reasons. -*/ -syntax RefType ::= ClassType | "nullType" | "arrayOf" Type -//The sdf syntax of array is different from Denis' syntax ( arrayof ), so added anywhere rule here -rule 'ArrayType(T:Type) => arrayOf T [anywhere] - -rule 'ClassOrInterfaceType(TypeK:K,, _) => TypeK [anywhere] - -rule isBlock('Block(_)) => true - -syntax HeatedInterfaceTypeList ::= List{ClassType, ","} [klabel('InterfaceTypeList), strict] -syntax InterfaceTypeList ::= HeatedInterfaceTypeList -endmodule diff --git a/src/old/java/exp-syntax.k b/src/old/java/exp-syntax.k deleted file mode 100644 index 9779caf..0000000 --- a/src/old/java/exp-syntax.k +++ /dev/null @@ -1,142 +0,0 @@ -module EXP-SYNTAX - imports TYPE-SYNTAX - imports SHARED-SYNTAX - -syntax Exp ::= StmtExp -syntax StmtExp ::= PrefixPostfixExp | AssignExp | MethodInvokeExp | ClassInstanceCreationExp - -//@ \subsection{MethodInvocation.sdf} -syntax MethodInvokeExp ::= MethodSpec "(" Exps ")" [klabel('Invoke)] -syntax MethodSpec ::= MethodName [klabel('Method)] - | Exp "." OptionalTypeArgs Id [klabel('Method)] - | "super" "." OptionalTypeArgs Id [klabel('SuperMethod)] - | TypeName "." "super" "." OptionalTypeArgs Id [klabel('QSuperMethod)] - | AmbName "." TypeArgs Id [klabel('GenericMethod)] - - -//@ \subsection{ClassInstanceCreation.sdf} -syntax ClassInstanceCreationExp ::= - "new" OptionalTypeArgs ClassOrInterfaceType "(" Exps ")" OptionalClassBody - [klabel('NewInstance)] -syntax ClassInstanceCreationExp ::= - Exp "." "new" OptionalTypeArgs Id OptionalTypeArgs "(" Exps ")" OptionalClassBody - [klabel('QNewInstance)] - - -//@ \subsection{AssignmentOperators.sdf} -syntax LHS ::= ExprName | FieldAccess | ArrayAccess - -syntax AssignExp ::= LHS "=" Exp [klabel('Assign)] -syntax AssignExp ::= CompoundAssignExp - -syntax CompoundAssignExp ::= LHS "*=" Exp [klabel('AssignMul)] - | LHS "/=" Exp [klabel('AssignDiv)] - | LHS "%=" Exp [klabel('AssignRemain)] - | LHS "+=" Exp [klabel('AssignPlus)] - | LHS "-=" Exp [klabel('AssignMinus)] - | LHS "<<=" Exp [klabel('AssignLeftShift)] - | LHS ">>=" Exp [klabel('AssignRightShift)] - | LHS ">>>=" Exp [klabel('AssignURightShift)] - | LHS "&=" Exp [klabel('AssignAnd)] - | LHS "^=" Exp [klabel('AssignExcOr)] - | LHS "|=" Exp [klabel('AssignOr)] - - -//@ \subsection{UnaryOperators.sdf} -syntax Exp ::= "(" PrimType ")" Exp [klabel('CastPrim)] -syntax Exp ::= "(" RefType ")" Exp [klabel('CastRef)] - -syntax Exp ::= "~" Exp [strict, klabel('Complement)] - | "!" Exp [strict, klabel('Not)] - | "+" Exp [strict, klabel('Plus)] - | "-" Exp [strict, klabel('Minus)] - -//@ Operators with side effects - prefix, postfix ++/-- -syntax PrefixPostfixExp ::= "++" Exp [klabel('PreIncr)] - | "--" Exp [klabel('PreDecr)] - - -//@ \subsection{Postfix.sdf} -syntax PrefixPostfixExp ::= Exp "++" [klabel('PostIncr)] - | Exp "--" [klabel('PostDecr)] - - -//@ \subsection{BinaryOperators.sdf} -syntax Exp ::= Exp "*" Exp [seqstrict, klabel('Mul)] - | Exp "/" Exp [seqstrict, klabel('Div)] - | Exp "%" Exp [seqstrict, klabel('Remain)] - > Exp "+" Exp [seqstrict, klabel('Plus)] - | Exp "-" Exp [seqstrict, klabel('Minus)] - -syntax Exp ::= Exp "<<" Exp [seqstrict, klabel('LeftShift)] - | Exp ">>" Exp [seqstrict, klabel('RightShift)] - | Exp ">>>" Exp [seqstrict, klabel('URightShift)] - -syntax Exp ::= Exp ">" Exp [seqstrict, klabel('Gt)] -syntax Exp ::= Exp "<" Exp [seqstrict, klabel('Lt)] -syntax Exp ::= Exp ">=" Exp [seqstrict, klabel('GtEq)] - -syntax Exp ::= Exp "||" Exp [strict(1), klabel('LazyOr)] - | Exp "&&" Exp [strict(1), klabel('LazyAnd)] - | Exp "|" Exp [seqstrict, klabel('Or)] - | Exp "^" Exp [seqstrict, klabel('ExcOr)] - | Exp "&" Exp [seqstrict, klabel('And)] - -syntax Exp ::= Exp "?" Exp ":" Exp [klabel('Cond)] - -syntax Exp ::= Exp "instanceof" RefType [strict, klabel('InstanceOf)] - - -//@ \subsection{FieldAccess.sdf} -syntax Exp ::= FieldAccess -syntax FieldAccess ::= Exp "." Id [klabel('Field)] - | "super" "." Id [klabel('SuperField)] - | TypeName "." "super" "." Id [klabel('QSuperField)] - - -//@ \subsection{ArrayAccess.sdf} -syntax Exp ::= ArrayAccess -//syntax ArraySubscript ::= "[" Exp "]" [bracket] -syntax ArrayAccess ::= Exp "[" Exp "]" [seqstrict, klabel('ArrayAccess)] - - -//@ \subsection{ArrayCreation.sdf} -/* Either 'NewArray( T:ElemType,, ['Dim(N1),,'Dim('N2),, ...],, [...,, 'Dim(.KList),, ...] ) - Or 'NewArray( T:ElemType,, [...,, 'Dim(.KList),, ...],, 'ArrayInit(_) ) -*/ -syntax Exp ::= ArrayCreationExp -//todo:cannot put ArrayBaseType instead of Type below, because rules and aux functions use Type -syntax ArrayCreationExp ::= "new" Type DimExps Dims [strict(2), klabel('NewArray)] -syntax ArrayCreationExp ::= "new" Type Dims ArrayInit [klabel('NewArray)] - -syntax ArrayBaseType ::= PrimType - | TypeName - | TypeName "<" "?" ">" [klabel('UnboundWld)] - -syntax Dim ::= "[" "]" [klabel('Dim)] -syntax DimExp ::= "[" Exp "]" [strict, klabel('Dim)] - -//@ \subsection{ArrayInitializers.sdf} -syntax ArrayInit ::= "{" VarInits "}" [klabel('ArrayInit)] -syntax ArrayInit ::= "{" VarInits "," "}" [klabel('ArrayInit)] - - -//@ \subsection{Primary.sdf} -syntax Exp ::= Literal [klabel('Lit)] -syntax Literal ::= IntLiteral - | FloatLiteral - | BoolLiteral - | CharLiteral - | StringLiteral - | NullLiteral - | ClassLiteral - -syntax ClassLiteral ::= Type "." "class" [klabel('Class)] - | "void" "." "class" [klabel('VoidClass)] - -syntax Exp ::= "this" [klabel('This)] - | TypeName "." "this" [klabel('QThis)] - -syntax Exp ::= "(" Exp ")" [bracket] - -endmodule diff --git a/src/old/java/interface-syntax.k b/src/old/java/interface-syntax.k deleted file mode 100644 index a8de460..0000000 --- a/src/old/java/interface-syntax.k +++ /dev/null @@ -1,69 +0,0 @@ -module INTERFACE-SYNTAX - imports CLASS-SYNTAX - -//@ \subsection{AbstractMethodDeclarations.sdf} -syntax AbstractMethodDec ::= - AnnoAbstractMethodModList OptionalTypeParams Type Id "(" Params ")" OptionalThrows ";" - [klabel('AbstractMethodDec)] - -syntax AbstractMethodMod ::= Public | Abstract -syntax AnnoAbstractMethodMod ::= Anno | AbstractMethodMod - - -//@ \subsection{Annotations.sdf} -syntax Anno ::= "@" TypeName "(" ElemValPairList ")" [klabel('Anno)] - | "@" TypeName "(" ElemVal ")" [klabel('SingleElemAnno)] - | "@" TypeName [klabel('MarkerAnno)] - -syntax ElemVal ::= Exp - | Anno - | "{" ElemValList "}" [klabel('ElemValArrayInit)] - | "{" ElemValList "," "}" [klabel('ElemValArrayInit)] - -syntax ElemValPair ::= Id "=" ElemVal [klabel('ElemValPair)] - - -//@ \subsection{AnnotationTypes.sdf} -syntax AnnoDecHead ::= AnnoInterfaceModList "@" "interface" Id [klabel('AnnoDecHead)] - -syntax AnnoDec ::= AnnoDecHead "{" AnnoElemDecList "}" [klabel('AnnoDec)] - -syntax AnnoElemDec ::= ConstantDec | ClassDec | InterfaceDec | EnumDec | AnnoDec | SemiColon -syntax AnnoElemDec ::= AbstractMethodModList Type Id "(" ")" OptionalDefaultVal ";" - [klabel('AnnoMethodDec)] - -syntax DefaultVal ::= "default" ElemVal [klabel('DefaultVal)] - - -//@ \subsection{ConstantDeclarations.sdf} -syntax ConstantDec ::= AnnoConstantModList Type VarDecList ";" [klabel('ConstantDec)] - -syntax ConstantMod ::= Public - | Static - | Final - -syntax AnnoConstantMod ::= Anno | ConstantMod - - -//@ \subsection{InterfaceDeclarations.sdf} -syntax InterfaceDecHead ::= - AnnoInterfaceModList "interface" Id OptionalTypeParams OptionalExtendsInterfaces - [klabel('InterfaceDecHead)] - -syntax InterfaceDec ::= InterfaceDecHead "{" InterfaceMemberDecList "}"[klabel('InterfaceDec)] - -syntax ExtendsInterfaces ::= "extends" InterfaceTypeList [klabel('ExtendsInterfaces)] - -syntax InterfaceMemberDec ::= ConstantDec | AbstractMethodDec | ClassDec | InterfaceDec | SemiColon - -syntax InterfaceMod ::= Public - | Private - | Protected - | Abstract - | Final - | Static - | StrictFP - -syntax AnnoInterfaceMod ::= Anno | InterfaceMod - -endmodule \ No newline at end of file diff --git a/src/old/java/java-doc.k b/src/old/java/java-doc.k deleted file mode 100644 index c25347d..0000000 --- a/src/old/java/java-doc.k +++ /dev/null @@ -1,7 +0,0 @@ -/*! -%contains only markdown env. -\input{sty/custom-commands.tex} - -\usepackage{fullpage} - -*/ diff --git a/src/old/java/java-syntax.k b/src/old/java/java-syntax.k deleted file mode 100644 index d511c21..0000000 --- a/src/old/java/java-syntax.k +++ /dev/null @@ -1,26 +0,0 @@ -require "exp-syntax.k" -require "stmt-syntax.k" -require "list-syntax.k" -require "lexical-syntax.k" -require "literal-syntax.k" -require "name-syntax.k" -require "class-syntax.k" -require "interface-syntax.k" -require "package-syntax.k" -require "optional-syntax.k" -require "type-syntax.k" -require "shared-syntax.k" -module JAVA-SYNTAX - imports LIST-SYNTAX - imports STMT-SYNTAX - imports EXP-SYNTAX - imports LEXICAL-SYNTAX - imports LITERAL-SYNTAX - imports NAME-SYNTAX - imports CLASS-SYNTAX - imports INTERFACE-SYNTAX - imports PACKAGE-SYNTAX - imports OPTIONAL-SYNTAX - imports TYPE-SYNTAX - imports SHARED-SYNTAX -endmodule diff --git a/src/old/java/lexical-syntax.k b/src/old/java/lexical-syntax.k deleted file mode 100644 index 61d4a17..0000000 --- a/src/old/java/lexical-syntax.k +++ /dev/null @@ -1,105 +0,0 @@ -module LEXICAL-SYNTAX -//@ \subsection{Comments.sdf} -//no need to define because K provides fixed layout - -//@ \subsection{Identifiers.sdf} -syntax Id ::= ID [klabel('Id)] -syntax ID ::= Token{[A-Za-z\_\$][A-Za-z0-9\_\$]*} [onlyLabel] - -//@ \subsection{KeyWord.sdf(not needed?)} -/* -syntax Keyword ::= "abstract" - | "assert" - | "boolean" - | "break" - | "byte" - | "case" - | "catch" - | "char" - | "class" - | "const" - | "continue" - | "default" - | "do" - | "double" - | "else" - | "enum" - | "extends" - | "final" - | "finally" - | "float" - | "for" - | "goto" - | "if" - | "implements" - | "import" - | "instanceof" - | "int" - | "interface" - | "long" - | "native" - | "new" - | "package" - | "private" - | "protected" - | "public" - | "return" - | "short" - | "static" - | "strictfp" - | "super" - | "switch" - | "synchronized" - | "this" - | "throw" - | "throws" - | "transient" - | "try" - | "void" - | "volatile" - | "while" -*/ - -//@ \subsection{LineTerminators.sdf} -syntax EndOfFile -syntax CarriageReturn ::= Token{[\r]} [onlyLabel] -syntax LineTerminator ::= EndOfFile - | CarriageReturn - | Token{[\n]} [onlyLabel] - | Token{[\r][\n]} [onlyLabel] - - -//@ \subsection{Modifiers.sdf} -syntax Public ::= "public" [klabel('Public)] -syntax Private ::= "private" [klabel('Private)] -syntax Protected ::= "protected" [klabel('Protected)] -syntax Abstract ::= "abstract" [klabel('Abstract)] -syntax Final ::= "final" [klabel('Final)] -syntax Static ::= "static" [klabel('Static)] -syntax Native ::= "native" [klabel('Native)] -syntax Transient ::= "transient" [klabel('Transient)] -syntax Volatile ::= "volatile" [klabel('Volatile)] -syntax StrictFP ::= "strictfp" [klabel('StrictFP)] -syntax Synchronized ::= "synchronized" [klabel('Synchronized)] - -syntax Modifier ::= Public - | Private - | Protected - | Abstract - | Final - | Static - | Native - | Transient - | Volatile - | StrictFP - | Synchronized - -//@ \subsection{UnicodeEscape.sdf} -syntax UnicodeEscape ::= Token {[\\][u]+ [0-9a-fA-F][0-9a-fA-F][0-9a-fA-F][0-9a-fA-F]} - [onlyLabel, klabel('UnicodeEscape)] -syntax UList ::= List{U,""} [klabel('UList)] -syntax U ::= "u" - -//@ \subsection{WhiteSpace.sdf} -//no need to define because K provides fixed layout -endmodule \ No newline at end of file diff --git a/src/old/java/list-syntax.k b/src/old/java/list-syntax.k deleted file mode 100644 index 43e2b12..0000000 --- a/src/old/java/list-syntax.k +++ /dev/null @@ -1,48 +0,0 @@ -module LIST-SYNTAX - -/*A module for list only, for the easy of implementation and management. - There are six lists ((formal)params, dims, dimexps, exps, varinits, catchclauses) - already defined before, because there is no automatic refactor for rename, and also those - defined are used in semantic rules, we leave them unchanged.*/ - -syntax InterfaceTypeList ::= List{InterfaceType,","} [klabel('InterfaceTypeList), strict] -syntax ExceptionTypeList ::= List{ExceptionType,","} [klabel('ExceptionTypeList)] -syntax IdList ::= List{Id,"."} [klabel('IdList)] -syntax TypeDecList ::= List{TypeDec,""} [klabel('TypeDecList)] -syntax VarDecList ::= List{VarDec,","} [klabel('VarDecList)] -syntax ImportDecList ::= List{ImportDec,""} [klabel('ImportDecList)] -syntax ActualTypeArgList ::= List{ActualTypeArg,","} [klabel('ActualTypeArgList)] -syntax ClassOrInterfaceTypeList ::= List{ClassOrInterfaceType, "&"} [klabel('ClassOrInterfaceTypeList)] -syntax TypeParamList ::= List{TypeParam,","} [klabel('TypeParamList)] -syntax AbstractMethodModList ::= List{AbstractMethodMod, ""} [klabel('AbstractMethodModList)] -syntax AnnoAbstractMethodModList ::= List{AnnoAbstractMethodMod, ""} [klabel('AnnoAbstractMethodModList)] -syntax AnnoMethodModList ::= List{AnnoMethodMod, ""} [klabel('AnnoMethodModList)] -syntax AnnoVarModList ::= List{AnnoVarMod, ""} [klabel('AnnoVarModList)] -syntax AnnoClassModList ::= List{AnnoClassMod, ""} [klabel('AnnoClassModList)] -syntax AnnoConstrModList ::= List{AnnoConstrMod, ""} [klabel('AnnoConstrModList)] -syntax AnnoConstantModList ::= List{AnnoConstantMod, ""} [klabel('AnnoConstantModList)] -syntax AnnoFieldModList ::= List{AnnoFieldMod, ""} [klabel('AnnoFieldModList)] -syntax AnnoInterfaceModList ::= List{AnnoInterfaceMod, ""} [klabel('AnnoInterfaceModList)] -syntax AnnoList ::= List{Anno, ""} [klabel('AnnoList)] -syntax AnnoElemDecList ::= List{AnnoElemDec, ""} [klabel('AnnoElemDecList)] -syntax InterfaceMemberDecList ::= List{InterfaceMemberDec, ""} [klabel('InterfaceMemberDecList)] -syntax ElemValPairList ::= List{ElemValPair,","} [klabel('ElemValPairList)] -syntax ElemValList ::= List{ElemVal,","} [klabel('ElemValList)] -syntax StringPartList ::= List{StringPart,""} [klabel('StringPartList)] -syntax EnumConstList ::= List{EnumConst, ","} [klabel('EnumConstList)] -syntax ClassBodyDecList ::= List{ClassBodyDec, ""} [klabel('ClassBodyDecList)] -syntax BlockStmList ::= List{BlockStmt, ""} [klabel('BlockStmList)] -syntax SwitchGroupList ::= List{SwitchGroup, ""} [klabel('SwitchGroupList)] -syntax SwitchLabelList ::= List{SwitchLabel, ""} [klabel('SwitchLabelList)] - -syntax Exps ::= List{Exp, ","} [klabel('ExprList), seqstrict] -syntax Dims ::= List{Dim,""} [klabel('DimList)] -syntax DimExps ::= List{DimExp,""} [klabel('DimExprList), strict] -syntax VarInits ::= List{VarInit, ","} [klabel('VarInitList)] -syntax CatchClauses ::= List{CatchClause,""} [klabel('CatchClauseList), strict] -syntax Params ::= List{Param, ","} [klabel('FormalParamList)] - -context 'FormalParamList(HOLE,,_) [result(Param)] -context 'FormalParamList(_,,HOLE) [result(Params)] - -endmodule \ No newline at end of file diff --git a/src/old/java/literal-syntax.k b/src/old/java/literal-syntax.k deleted file mode 100644 index 0cf2e03..0000000 --- a/src/old/java/literal-syntax.k +++ /dev/null @@ -1,58 +0,0 @@ -module LITERAL-SYNTAX - imports LEXICAL-SYNTAX - imports LIST-SYNTAX - -//@ \subsection{BooleanLiterals.sdf} -syntax BoolLiteral ::= Boolean [klabel('Bool)] -syntax Boolean ::= "true" [onlyLabel, klabel('True)] -syntax Boolean ::= "false" [onlyLabel, klabel('False)] - - -//@ \subsection{CharacterLiterals.sdf} todo -syntax SingleChar// ::= Token{[\r\n\'\\]}//don't understand ^? - -syntax CharContent ::= SingleChar [klabel('Single)] - | UnicodeEscape - | EscapeSeq -//Problem: Multiple lookahead not fully supported (does not appear when tested in small language) -syntax CharLiteral //::= "'" CharContent "'" [klabel('Char)] - - -//@ \subsection{EscapeSequences.sdf} -syntax EscapeSeq ::= OctaEscape | NamedEscape - -syntax NamedEscape ::= Token{"\\" [btnfr\"\'\\]} [onlyLabel, klabel('NamedEscape)] -syntax OctaEscape ::= Token{"\\" [0-7]} [onlyLabel, klabel('OctaEscape1)] - | Token{"\\" [0-3][0-7]} [onlyLabel, klabel('OctaEscape2)] - | Token{"\\" [4-7][0-7]} [onlyLabel, klabel('OctaEscape2)] - | Token{"\\" [0-3][0-7][0-7]} [onlyLabel, klabel('OctaEscape3)] - - -//@ \subsection{FloatingPointLiterals.sdf} todo -syntax FloatLiteral ::= Float [klabel('Float)] - - -//@ \subsection{IntegerLiterals.sdf} -syntax DeciLiteral ::= Token{[1-9][0-9]* [lL]?} [onlyLabel] -syntax HexaLiteral ::= Token{[0][xX][0-9a-fA-F]+ [lL]?} [onlyLabel] -syntax OctaLiteral ::= Token{[0][0-7]+ [lL]?} [onlyLabel] - -syntax IntLiteral ::= DeciLiteral [klabel('Deci)] - | HexaLiteral [klabel('Hexa)] - | OctaLiteral [klabel('Octa)] - - -//@ \subsection{NullLiteral.sdf} -syntax NullLiteral ::= "null" [klabel('Null)] - - -//@ \subsection{StringLiterals.sdf} todo -syntax StringLiteral ::= "\"" StringPartList "\"" [klabel('String)] - -syntax StringPart ::= StringChars [klabel('Chars)] - | UnicodeEscape - | EscapeSeq - -syntax StringChars //::= Token {~[\"\\\n\13]} - -endmodule \ No newline at end of file diff --git a/src/old/java/name-syntax.k b/src/old/java/name-syntax.k deleted file mode 100644 index 5f5342a..0000000 --- a/src/old/java/name-syntax.k +++ /dev/null @@ -1,21 +0,0 @@ -module NAME-SYNTAX - imports LITERAL-SYNTAX - -syntax PackageName ::= IdList [klabel('PackageName)] - -syntax AmbName ::= Id [klabel('AmbName)] - | AmbName "." Id [klabel('AmbName)] - -syntax PackageOrTypeName ::= Id [klabel('PackageOrTypeName)] - | PackageOrTypeName "." Id [strict(1), klabel('PackageOrTypeName)] - -syntax ExprName::= Id [klabel('ExprName)] - | AmbName "." Id [klabel('ExprName)] - -syntax TypeName ::= Id [klabel('TypeName)] - | PackageOrTypeName "." Id [strict(1), klabel('TypeName)] - -syntax MethodName ::= Id [klabel('MethodName)] - | AmbName "." Id [klabel('MethodName)] - -endmodule \ No newline at end of file diff --git a/src/old/java/optional-syntax.k b/src/old/java/optional-syntax.k deleted file mode 100644 index ef65842..0000000 --- a/src/old/java/optional-syntax.k +++ /dev/null @@ -1,44 +0,0 @@ -module OPTIONAL-SYNTAX -/* -When a particular term is optional in a production, it is represented as OptionalXXX. -Corresponding AST will contain 'Some() if the term exist, 'None(.KList) if not. -All Optionals are defined in this file for management simplicity. -*/ - -syntax None ::= "" [onlyLabel, klabel('None)] - -syntax OptionalId ::= Id [prefer, klabel('Some)] | None -syntax OptionalExp ::= Exp [prefer, klabel('Some)] | None -syntax OptionalWildcardBound ::= WildcardBound [prefer, klabel('Some)] | None -syntax OptionalTypeArgs ::= TypeArgs [prefer, klabel('Some)] | None -syntax OptionalTypeParams ::= TypeParams [prefer, klabel('Some)] | None -syntax OptionalTypeBound ::= TypeBound [prefer, klabel('Some)] | None -syntax OptionalThrows ::= Throws [prefer, klabel('Some)] | None -syntax OptionalDefaultVal ::= DefaultVal [prefer, klabel('Some)] | None -syntax OptionalExtendsInterfaces ::= ExtendsInterfaces [prefer, klabel('Some)] | None -syntax OptionalInterfaces ::= Interfaces [prefer, klabel('Some)] | None -syntax OptionalPackageDec ::= PackageDec [prefer, klabel('Some)] | None -syntax OptionalSuper ::= Super [prefer, klabel('Some)] | None -syntax OptionalConstrInv ::= ConstrInv [prefer, klabel('Some)] | None -syntax OptionalClassBody ::= ClassBody [prefer, klabel('Some)] | None -syntax OptionalEnumBodyDecs ::= EnumBodyDecs [prefer, klabel('Some)] | None -syntax OptionalEnumConstArgs ::= EnumConstArgs [prefer, klabel('Some)] | None - -syntax Id -syntax Exp -syntax WildcardBound -syntax TypeArgs -syntax TypeParams -syntax TypeBound -syntax Throws -syntax DefaultVal -syntax ExtendsInterfaces -syntax Interfaces -syntax PackageDec -syntax Super -syntax ConstrInv -syntax ClassBody -syntax EnumBodyDecs -syntax EnumConstArgs - -endmodule \ No newline at end of file diff --git a/src/old/java/package-syntax.k b/src/old/java/package-syntax.k deleted file mode 100644 index 69b2562..0000000 --- a/src/old/java/package-syntax.k +++ /dev/null @@ -1,19 +0,0 @@ -module PACKAGE-SYNTAX - imports CLASS-SYNTAX - -//@ \subsection{CompilationUnits.sdf} -//syntax CompilationUnit ::= OptionalPackageDec ImportDecList TypeDecList [klabel('CompilationUnit)] - -//@ \subsection{TypeDeclarations.sdf} -syntax TypeDec ::= ClassDec | InterfaceDec | SemiColon - -//@ \subsection{ImportDeclarations.sdf} -syntax ImportDec ::= "import" TypeName ";" [klabel('TypeImportDec)] - | "import" PackageName "." "*" ";" [klabel('TypeImportOnDemandDec)] - | "import" "static" TypeName "." Id ";" [klabel('StaticImportDec)] - | "import" "static" TypeName "." "*" ";" [klabel('StaticImportOnDemandDec)] - -//@ \subsection{PackageDeclarations.sdf} -syntax PackageDec ::= AnnoList "package" PackageName ";" [klabel('PackageDec)] - -endmodule \ No newline at end of file diff --git a/src/old/java/primitive-types.k b/src/old/java/primitive-types.k deleted file mode 100644 index e2ef48b..0000000 --- a/src/old/java/primitive-types.k +++ /dev/null @@ -1,113 +0,0 @@ -module PRIMITIVE-TYPES - imports SUBTYPING - -//@ \subsection{Integer types normalization} - -syntax Int ::= bitCount ( Type ) [function] -rule bitCount(byte) => 8 -rule bitCount(short) => 16 -rule bitCount(int) => 32 -rule bitCount(long) => 64 -rule bitCount(char) => 16 - -/*@ Symbolic execution limitation: this construct cannot be [function] - When conditionals are needed, implementation have to use 'If - the symbolically processed version of if. -*/ -syntax KItem ::= normalize ( TypedVal ) - -rule normalize(I:Int :: IntT:IntType) - => ifAux(isInRange(I::IntT), - I::IntT, - normalizeImpl(I::IntT) - ) -when IntT =/=K char - -rule normalize(I:Int :: char) - => ifAux(isInRange(I::char), - I :: char, - toUnsigned(normalizeImpl(I::char)) - ) - -rule normalize(I:Int :: FloatT:FloatType) => Int2Float(I,53,11)::FloatT - -rule normalize(F:Float :: IntT:IntType) => normalize(Float2Int(F) :: IntT:IntType) - -rule normalize(F:Float :: FloatT:FloatType) => F::FloatT - -//@ Symbolic execution limitation: this construct cannot be [function] -syntax KItem ::= isInRange ( TypedVal ) -rule isInRange(I:Int::byte) => ((I >=Int -128) andBool (I <=Int 127)) -rule isInRange(I:Int::short) => ((I >=Int -32768) andBool (I <=Int 32767)) -rule isInRange(I:Int::int) => ((I >=Int -2147483648) andBool (I <=Int 2147483647)) -rule isInRange(I:Int::long) => ((I >=Int -9223372036854775808) - andBool (I <=Int 9223372036854775807)) -rule isInRange(I:Int::char) => ((I >=Int 0) andBool (I <=Int 65535)) - -rule isInRange(RV:RawVal::_) => true -when notBool (isInt(RV) ==K true) - -/*@ Symbolic execution limitation: this construct cannot be [function] -*/ -syntax KItem ::= normalizeImpl ( TypedVal ) - -rule normalizeImpl(I:Int :: T:Type) - => normalizeSign((((I &Int ((1 < ifAux(I <=Int ((1 < ifAux(I >=Int 0, - I :: T, - I +Int (1 < ILT - -rule normalizeType(FT:FloatType) => FT - -rule normalizeType(IT:IntType) => int -when (IT =/=K int) andBool (IT =/=K long) - -/*@ Important! Binary normalizeType cannot be function because it uses sybtype in implementation. -*/ -syntax KItem ::= normalizeType ( Type, Type ) [function] - -rule normalizeType(NT1:IntType, NT2:IntType) => int -when (NT1 =/=K long) andBool (NT2 =/=K long) - -rule normalizeType(NT1:IntType, NT2:IntType) => long -when (NT1 ==K long) orBool (NT2 ==K long) - -rule normalizeType(T:Type, FT:FloatType) => ifAux(subtype(T, FT), FT, T) -rule normalizeType(FT:FloatType, T:Type) => ifAux(subtype(T, FT), FT, T) - -//not technically primitive types, but here is the most appropriate place to put the rules -rule normalizeType(Class:ClassType, _) => Class -when (Class ==K classString) - -rule normalizeType(_, Class:ClassType) => Class -when (Class ==K classString) - -//Other cases. Required by the rule CompoundAssign -rule normalizeType(T1:Type, T2:Type) => T1 -when notBool (isNumericType(T1) ==K true) andBool (T2 =/=K classString) - -rule normalizeType(bool, bool) => bool - -endmodule diff --git a/src/old/java/shared-syntax.k b/src/old/java/shared-syntax.k deleted file mode 100644 index dddcb08..0000000 --- a/src/old/java/shared-syntax.k +++ /dev/null @@ -1,9 +0,0 @@ -module SHARED-SYNTAX -/*previously defined elsewhere for ltl-support, now these syntax are also used for java, -although we don't incorporate ltl for now, let's keep this independent like this -*/ -syntax Exp ::= Exp "<=" Exp [seqstrict, klabel('LtEq)] - | Exp "==" Exp [seqstrict, klabel('Eq)] - | Exp "!=" Exp [klabel('NotEq)] - -endmodule diff --git a/src/old/java/stmt-syntax.k b/src/old/java/stmt-syntax.k deleted file mode 100644 index 9365bb5..0000000 --- a/src/old/java/stmt-syntax.k +++ /dev/null @@ -1,71 +0,0 @@ -module STMT-SYNTAX - imports CLASS-SYNTAX - -//@ \subsection{Blocks.sdf} -syntax BlockStmt ::= Stmt | LocalVarDecStmt | ClassDec [klabel('ClassDecStm)] -syntax Block ::= "{" BlockStmList "}" [klabel('Block)] - - -//@ \subsection{LocalVariableDeclaraions.sdf} -syntax LocalVarDecStmt ::= LocalVarDec ";" [prefer, klabel('LocalVarDecStm)] -syntax LocalVarDec ::= AnnoVarModList Type VarDecList [prefer, klabel('LocalVarDec)] - - -//@ \subsection{Statements.sdf} -syntax Stmt ::= StmtWithoutTrailing - | LabeledStmt - | IfThenElseStmt - | IfThenStmt - | WhileStmt - | ForStmt - -syntax StmtWithoutTrailing ::= Block - | EmptyStmt - | ExprStmt - | AssertStmt - | SwitchStmt - | DoStmt - | TryStmt - | StackConsumerStmt - | SynchronizedStmt - -syntax StackConsumerStmt ::= ThrowStmt | ContinueStmt | BreakStmt | ReturnStmt - -syntax IfThenElseStmt ::= "if" "(" Exp ")" Stmt "else" Stmt [strict(1), klabel('If)] -syntax IfThenStmt ::= "if" "(" Exp ")" Stmt [prefer, strict(1), klabel('If)] - -syntax WhileStmt ::= "while" "(" Exp ")" Stmt [strict(1),klabel('While)] - -syntax ForStmt ::= "for" "(" LocalVarDec ";" OptionalExp ";" Exps ")" Stmt [klabel('For)] -syntax ForStmt ::= "for" "(" Exps ";" OptionalExp ";" Exps ")" Stmt [klabel('For)] -syntax ForStmt ::= "for" "(" Param ":" Exp ")" Stmt [klabel('ForEach)] - -syntax LabeledStmt ::= Id ":" Stmt [klabel('Labeled)] - -syntax EmptyStmt ::= ";" [klabel('Empty)] - -syntax ExprStmt ::= Exp ";" [strict, klabel('ExprStm)] - -syntax AssertStmt ::= "assert" Exp ";" [strict, klabel('AssertStm)] - | "assert" Exp ":" Exp ";" [strict(1), klabel('AssertStm)] - -syntax SwitchStmt ::= "switch" "(" Exp ")" SwitchBlock [strict(1), klabel('Switch)] -syntax SwitchBlock ::= "{" SwitchGroupList SwitchLabelList "}" [klabel('SwitchBlock)] -syntax SwitchGroup ::= SwitchLabelList BlockStmList [klabel('SwitchGroup)] -syntax SwitchLabel ::= "case" Exp ":" [klabel('Case)] - | "default" ":" [klabel('Default)] - -syntax DoStmt ::= "do" Stmt "while" "(" Exp ")" ";" [strict(2), klabel('DoWhile)] - -syntax CatchClause ::= "catch" "(" Param ")" Block [klabel('Catch)] -syntax TryStmt ::= "try" Block CatchClauses "finally" Block [klabel('Try)] - | "try" Block CatchClauses [klabel('Try)] - -syntax ThrowStmt ::= "throw" Exp ";" [strict, klabel('Throw)] -syntax ContinueStmt ::= "continue" OptionalId ";" [klabel('Continue)] -syntax BreakStmt ::= "break" OptionalId ";" [klabel('Break)] -syntax ReturnStmt ::= "return" OptionalExp ";" [klabel('Return)] - -syntax SynchronizedStmt ::= "synchronized" "(" Exp ")" Block [strict(1), klabel('Synchronized)] - -endmodule diff --git a/src/old/java/subtyping.k b/src/old/java/subtyping.k deleted file mode 100644 index 791defe..0000000 --- a/src/old/java/subtyping.k +++ /dev/null @@ -1,161 +0,0 @@ -module SUBTYPING - imports CORE-CLASSES - -//@ Checks whether first type is a subtype of the second -syntax Exp ::= subtype ( - Type, - Type - ) - [strict] - -/*@ Checks whether the each type in the first list of types is a subtype -of the type at the same position in the second list. -If lists have different size, the function will evaluate to false. -Used in method call overloading resolution. -*/ -syntax KItem ::= subtypeList ( Types, Types ) - -rule [subtype-same-type-True]: - subtype( T:Type, T ) => true - [structural] - -/*@ \subsection{Subtyping among primitive types} */ - -rule subtype( byte, T:Type ) => (T ==K short) orBool (T ==K int) orBool (T ==K long) orBool (isFloatType(T) ==K true) -when T =/=K byte [structural] - -rule subtype( short, T:Type ) => (T ==K int) orBool (T ==K long) orBool (isFloatType(T) ==K true) - -when T =/=K short [structural] - -rule subtype( int, T:Type ) => (T ==K long orBool isFloatType(T) ==K true) -when T =/=K int [structural] - -rule subtype( long, T:Type ) => isFloatType(T) ==K true -when T =/=K long [structural] - -rule subtype( char, T:Type ) => (T ==K int) orBool (T ==K long) orBool (isFloatType(T) ==K true) -when T =/=K char [structural] - -rule subtype( float, T:Type ) => (T ==K double) -when T =/=K float [structural] - -rule subtype( double, T:Type ) => false -when T =/=K double [structural] - -rule subtype( bool, T:Type ) => false -when T =/=K bool [structural] - -/*@ \subsection{Subtyping among reference types} -The subclass relation introduces a subtyping relation. */ - -rule [subtype-ClassOfClassRed]: - subtype( Class1:ClassType, Class:ClassType ) - => subtype( Class2:ClassType, Class ) ... - - Class1 - Class2 - classCMT - ... - - - Class - classCMT - ... - -when - Class1 =/=K Class - [structural] - -rule [subtype-NoClassOfAnyFalse]: - subtype( noClass, _ ) => false - -//The case subtype (noClass, noClass) should never be encountered -//used by the rule [findQualifierOfType] -rule [subtype-AnyOfNoClassFalse]: - subtype( _, noClass ) => true - -rule [subtype-IInterfaceOfClass]: - subtype( Class1:ClassType, Class:ClassType ) => Class ==K classObject ... - - Class1 - interfaceCMT - ... - - - Class - classCMT - ... - -/* -K Limitation: This way don't seem to work: - Class1 - interfaceMetaT - Class - classMetaT -*/ - -rule [subtype-OfInterface]: - subtype( Class1:ClassType, Class2:ClassType ) => Class2 in ISet ... - - Class1 - ISet:Set - ... - - - Class2 - interfaceCMT - ... - - -rule [subType-ClassOfOtherFalse]: - subtype( _:ClassType, T:Type ) => false -when - notBool (isClassType(T) ==K true) - -rule [subtype-ArrayOfClass]: - subtype( arrayOf _, Class:ClassType ) => Class ==K classObject - -rule [subtype-ArrayOfOtherFalse]: - subtype( arrayOf _, T:Type ) => false -when - (getKLabel(T) =/=KLabel 'arrayOf_) - andBool notBool (isClassType(T) ==K true) - -rule [subtype-Null]: - subtype( nullType, T:Type ) => (isRefType(T) ==K true) - [structural] - -//@ Subtype -rule [subtype-ArrayOfArrayPrimitive]: - subtype( arrayOf T1:Type, arrayOf T2:Type ) => (T1 ==K T2) -when - notBool (isRefType(T1) ==K true) orBool notBool (isRefType(T2) ==K true) - -rule [subtype-ArrayOfArrayRef]: - subtype( arrayOf RefT1:RefType, arrayOf RefT2:RefType ) => subtype( RefT1, RefT2 ) - -//used by lookupQThis, when QThis is an inferred qualifier for unqualified new instance creation. -rule [subtype-OfNoClass]: - subtype( _, noClass ) => false - -/*@ \subsection{Subtyping lists of types}*/ - -rule [subtypeList]: - subtypeList(types(T1:Type,,Ts:KList), types(Tp1:Type,,Tps:KList)) - => andAux( subtype(T1,Tp1), subtypeList(types(Ts), types(Tps)) ) - [structural] - -rule [subtypeList-EmptyLeft]: - subtypeList(types(.KList), types(_:Type,,_)) => false - [structural] - -rule [subtypeList-EmptyRight]: - subtypeList(types(_:Type,,_) , types(.KList)) => false - [structural] - -rule [subtypeList-EmptyBoth]: - subtypeList(types(.KList), types(.KList)) => true - [structural] - -endmodule diff --git a/src/old/java/type-syntax.k b/src/old/java/type-syntax.k deleted file mode 100644 index 3c8542d..0000000 --- a/src/old/java/type-syntax.k +++ /dev/null @@ -1,62 +0,0 @@ -module TYPE-SYNTAX - imports NAME-SYNTAX - imports OPTIONAL-SYNTAX - -//@ \subsection{Main.sdf} -syntax Type ::= PrimType - | RefType -/*Denis' syntax: actually in sdf "void" together with Type compose ResultType, -since now "void" is Type, there is no need for another syntax of ResultType.*/ - | "void" [klabel('Void)] - -//@ \subsection{ParameterizedTypes.sdf} -syntax TypeArgs ::= "<" ActualTypeArgList ">" [klabel('TypeArgs)] - -syntax ActualTypeArg ::= Type - | "?" OptionalWildcardBound [klabel('Wildcard)] - -syntax WildcardBound ::= "extends" RefType [klabel('WildcardUpperBound)] - | "super" RefType [klabel('WildcardLowerBound)] - - -//@ \subsection{PrimitiveTypes.sdf} -syntax IntOrLongType ::= "int" [klabel('Int)] - | "long" [klabel('Long)] -syntax IntType ::= "byte" [klabel('Byte)] - | "short" [klabel('Short)] - | "char" [klabel('Char)] - | IntOrLongType - -syntax FloatType ::= "float" [klabel('Float)] - | "double" [klabel('Double)] -//sdf NumType -syntax NumericType ::= IntType | FloatType -syntax PrimType ::= NumericType | "bool" [klabel('Boolean)] //sdf "boolean" - - -//@ \subsection{ReferenceTypes.sdf} - /*@ A fully qualified class name, or noClass where no valid class could be computed.*/ -syntax ClassOrInterfaceType ::= TypeDecSpec OptionalTypeArgs [klabel('ClassOrInterfaceType)] - -syntax InterfaceType ::= TypeDecSpec OptionalTypeArgs [klabel('InterfaceType)] -//sdf ClassType, use another name JavaClassType to avoid conflict with Denis' ClassType syntax -syntax JavaClassType ::= TypeDecSpec OptionalTypeArgs [klabel('ClassType)] - -syntax TypeDecSpec ::= TypeName | TypeDecSpec TypeArgs "." Id [klabel('Member)] - -syntax TypeVar ::= TypeVarId [klabel('TypeVar)] - -syntax ArrayType ::= Type "[" "]" [strict, klabel('ArrayType)] - -syntax RefType ::= ClassOrInterfaceType | ArrayType - - -//@ \subsection{TypeVariables.sdf} -syntax TypeVarId ::= Id - -syntax TypeBound ::= "extends" ClassOrInterfaceTypeList [klabel('TypeBound)] - -syntax TypeParam ::= TypeVarId OptionalTypeBound [klabel('TypeParam)] -syntax TypeParams ::= "<" TypeParamList ">" [klabel('TypeParams)] - -endmodule \ No newline at end of file diff --git a/src/old/rvm-syntax.k b/src/old/rvm-syntax.k deleted file mode 100644 index 4dcc89e..0000000 --- a/src/old/rvm-syntax.k +++ /dev/null @@ -1,45 +0,0 @@ - -require "java/java-syntax.k" - -require "logic/ere-syntax.k" - -module RVM-SYNTAX - imports JAVA-SYNTAX - - imports ERE-SYNTAX - - syntax CompilationUnit ::= OptionalPackageDec ImportDecList SpecDec [klabel('CompilationUnit)] - - syntax SpecDec ::= SpecDecHead SpecBody - - syntax SpecDecHead ::= Id OptionalParams - - - syntax OptionalParams ::= Params [prefer, klabel('Some)] | None - - syntax SpecBody ::= "{" SpecBodyDecList "}" - - syntax SpecBodyDec ::= EventDec | PropertyDec - - syntax EventDec ::= EventDecHead EventBody [klabel('EventDec)] - - syntax EventBody ::= Block [klabel('EventBody)] - - syntax EventDecHead ::= "event" Id "(" Params ")" - - syntax PropertyDec ::= Property HandlerDecList - - syntax Property ::= LogicName ":" LogicFormula - - syntax HandlerDec ::= HandlerDecHead HandlerBody - - syntax HandlerDecHead ::= "@" LogicState - - syntax HandlerBody ::= Block - - - -syntax SpecBodyDecList ::= List{SpecBodyDec, ""} -syntax HandlerDecList ::= List{HandlerDec, ""} - -endmodule \ No newline at end of file diff --git a/src/rvm/logic-plugins-shell.k b/src/rvm/logic-plugins-shell.k new file mode 100644 index 0000000..7995140 --- /dev/null +++ b/src/rvm/logic-plugins-shell.k @@ -0,0 +1,7 @@ +require "../logic/semantics/fsm.k" + +module LOGIC-PLUGINS-SHELL + imports FSM + + +endmodule \ No newline at end of file diff --git a/src/rvm/rvc.k b/src/rvm/rvc.k new file mode 100644 index 0000000..e638b7c --- /dev/null +++ b/src/rvm/rvc.k @@ -0,0 +1,20 @@ +require "rvm-syntax.k" +require "rvm-compiler.k" +require "logic-plugins-shell.k" +require "../c-monitor-code-template/c-monitor-template.k" + +module RVC-SYNTAX + imports RVM-COMPILER-SYNTAX + +endmodule + +module RVC + imports RVC-SYNTAX + imports RVM-COMPILER-CORE + + imports RVM-COMPILER + + imports LOGIC-PLUGINS-SHELL + imports C-MONITOR-TEMPLATE + +endmodule diff --git a/src/rvm/rvm-compiler-core.k b/src/rvm/rvm-compiler-core.k new file mode 100644 index 0000000..c925135 --- /dev/null +++ b/src/rvm/rvm-compiler-core.k @@ -0,0 +1,122 @@ +require "rvm-syntax.k" + +module RVM-COMPILER-SYNTAX + imports RVM-SYNTAX + imports DOMAINS-SYNTAX + + + syntax NoBracket ::= r"[^<{}][^{}]*" [token, klabel('NoBracket)] + syntax ParamsBubble ::= r"\\([^\\)]*\\)" [token, avoid, klabel('ParamsBubble)] + syntax VarInitBubble ::= r"[^<;][^;]*" [token, avoid, klabel('VarInitBubble)] + syntax NoParentheses ::= r"[^()<][^()]*" [token, klabel('NoParentheses)] + + syntax BoolExpBubble ::= BalancedParentheses [token, klabel('BoolExpBubble)] //TODO:removed prefer (for MOP production), check amb + + syntax DecBubbleList ::= List{DecBubble, ""} [token, klabel(DecBubbleListCons)] + + syntax DecBubble ::= ClassDecBubble [token, klabel('DecBubbleClass)] + | MethodDecBubble [token, klabel('DecBubbleMethod)] + | FieldDecBubble [token, klabel('DecBubbleField)] + + syntax BlockBubble ::= "{" BalancedBracket "}" [prefer, token, klabel(BlockBubbleLabel)] + | EmptyBlock + + + + syntax IdPattern ::= //id with * and .. wildcards (it can start with * but not with .. , same about end) + // r"(? + 0 + + $PGM:RVM + + "" + + "" + + .List //list of event name strings + //the params of each event, indexed by event id + .List + //the list of event action code, indexed by event id. + .List + + "" + .Params + .K + + -1 //the property rank + 0 //the number of properties + +/////////////////////////////Logic Plugin cells starts//////////////////////////////////////////// + + .K + .K + + false + +//map a state name(string) to its integer rank, temporary working cell + .Map + +// Each ListItem is a map from states name to state rank (string -> int), +//indexed by property rank + .List + + 0 + + //the raw transition defined in the rvm spec, indexed by states + .K + + 0 + + //the state transformation function, indexed by events + + + .K + + + -1 + .Map + .List + + + + + + //we may need to traverse formula to get state numbers + //in the first scan, use this tmp cell for saving state transitions + //which will be restored in the second scan. + .K + 0 + + .K + +///////////////////////Specific for FSM////////////////////////////////////////////////////// + +/////////////////////////////////Logic Plugin cells ends/////////////////////////////////////////// + //the map element maps state name to handler code string + .Map + + .HandlerDecList + + .List + +///////////////////////////////Code Generation////////////////////////////////////////////////// + "c" //the default target language for the generated monitor code + .List + .List //temporary cell for manipulation. + .K + .K //additional computation cell + + ///////specific for monitor code in language C +
.List
+ + +endmodule diff --git a/src/rvm/rvm-compiler.k b/src/rvm/rvm-compiler.k new file mode 100644 index 0000000..5b3acf9 --- /dev/null +++ b/src/rvm/rvm-compiler.k @@ -0,0 +1,132 @@ +require "rvm-syntax.k" +require "domains.k" +require "rvm-compiler-core.k" +require "../helper/print-ast.k" +require "../../src/helper/util.k" + +//// +module RVM-COMPILER + imports RVM-SYNTAX + imports RVM-COMPILER-CORE + imports PRINT-AST + imports UTIL + + syntax KResult ::= "error" + +/** +* Store the package info and import list. +*/ +rule X:OptionalPackageDec Y:ImportDecList Z:SpecDec => Z + "" => PackageDec2String(X) + "" => importList2String(Y) + +/** +* Store the spec name and params. +*/ +rule X:Id (Ps:Params) SB:SpecBody => SB + "" => Id2String(X) + .Params => Ps + +/** +* Store the declarations info. +*/ +rule {(Decls:DecBubbleList => .K) Events:EventDecList +Props:PropertyDecList} + .K => Decls + I:Int => sizeOf(Props) + + + + +/** +* Extract and store the first event in the event list if we haven't encountered it before. +*/ +rule + 0 + {.K ((EM:EventModifier event (X:Id) (Ps:Params) Body:BlockBubble) + Events:EventDecList => Events) Props:PropertyDecList} + L:List (.List => ListItem(Id2String(X))) + EA:List (.List => ListItem(Block2Str(Body))) + +//the params of each event, indexed by event id + EP:List (.List => ListItem(Params2Str(Ps))) + + + ... + + (.Bag => + + X:Id + + + PS -Int 1 + .Map + .List + + + + ) + + PS:Int + .K => PS -Int 1 + +when notBool (Id2String(X) in L) + +//construct initial props cells +rule + L:List + + ... + + + X:Id + + (.Bag => + PS -Int 1 + .Map + .List + ) + ... + + + + ... + + PS:Int => PS -Int 1 +when PS >Int 0 andBool isLastItem(L, X) + +rule 0 => .K + + +/** +* Report error if an event is defined multiple times. +* In case of error, the execution will be terminated and the error info +* will be stored in cell. +*/ +rule {.K ((EM:EventModifier event (X:Id) (Ps:Params) Body:BlockBubble) + Events:EventDecList) Props:PropertyDecList} => .K + EL:List + (.List => ListItem("Duplicate event " +String Id2String(X))) ErrList:List +when (Id2String(X) in EL) + +//No events left +rule + {.K (.EventDecList) Props:PropertyDecList} => Props + 0 => 1 + + +//add the property formula and corresponding handlers +rule Prop:PropertyDec Props:PropertyDecList => Props + I:Int => I +Int 1 + .K => getLogicName(Prop) + .K => getFormula(Prop) + .K => getFormula(Prop) + .HandlerDecList => getHandlers(Prop) + false => true + +//No properties left +rule .PropertyDecList => . + false + M:Map => .Map + +endmodule diff --git a/src/rvm/rvm-syntax.k b/src/rvm/rvm-syntax.k index 25d3afa..14c5fc1 100644 --- a/src/rvm/rvm-syntax.k +++ b/src/rvm/rvm-syntax.k @@ -7,7 +7,7 @@ module RVM-SYNTAX //top level sort (aka CompilationUnit) - syntax RVM ::= OptionalPackageDec ImportDecList SpecDec + syntax RVM ::= OptionalPackageDec ImportDecList SpecDec [prefer, klabel('RVM)] syntax SpecDec ::= SpecDecHead SpecBody @@ -24,6 +24,6 @@ module RVM-SYNTAX //syntax SpecBodyDecList ::= List{SpecBodyDec, ""} -syntax EventDecList ::= List{EventDec, ""} +syntax EventDecList ::= List{EventDec, ""} [klabel('EventsDecList)] endmodule diff --git a/test/cmop/rvc/Test.rvm b/test/cmop/rvc/Test.rvm new file mode 100644 index 0000000..2f19a29 --- /dev/null +++ b/test/cmop/rvc/Test.rvm @@ -0,0 +1,31 @@ +package rvm; + +import java.io.*; +Test (int o){ + + event hasnext(Iterator i) {} // {1, 1, 1, 3} + event next(Iterator i) {} // {2, 0, 2, 3} + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + // alias match = unsafe, start + + @match { + int j; + } + + + +} diff --git a/test/cmop/test.in b/test/cmop/test.in new file mode 100644 index 0000000..573541a --- /dev/null +++ b/test/cmop/test.in @@ -0,0 +1 @@ +0 diff --git a/test/cmop/test.k b/test/cmop/test.k new file mode 100644 index 0000000..752065c --- /dev/null +++ b/test/cmop/test.k @@ -0,0 +1,59 @@ +require "../../src/c-monitor-code-template/c-monitor-template-syntax.k" +require "../../src/helper/util.k" +require "../../src/helper/print-ast.k" + + +module TEST +imports C-MONITOR-TEMPLATE-SYNTAX +imports UTIL +imports PRINT-AST + +configuration + $PGM:Int + false + .List + .Map + .List //temporary cell for manipulation. + + "HasNext" + + + +rule false => true + _:K => $CMonitor 2 3 + .Map => (("Safe" |-> 0) ("Unsafe" |-> 1) + ("good" |-> 2) ("bad" |-> 3)) + +//generate the include part. +//TODO: incorporate the user provided includes +rule $incl M:MainBody => M + L:List (.List => ListItem("#include \n" + +String "#include \n") ) + + +//rewrite the global var declarations. +rule G:GlobalVarDecls M:MainBody1 => M + + L:List (.List => ListItem("static int __RVC_state = 0;\n")) + + +rule ($localInit(0) M:MainBody2) => + M + +rule ($localInit(I:Int) M:MainBody2) => + (($sVar(I -Int 1), $localInit(I -Int 1)) M) + +when I >=Int 1 + +rule (($sVar(I:Int), $localInit(J:Int)) M:MainBody2) => + (($localInit(J:Int)) M) + + StateMap:Map + (.List => ListItem(getStrKey(StateMap, I))) L:List + +rule $reset M:MainBody3 => M + SN:String + L:List => .List //the local state vars are stored in tmp cell + Code:List (.List => L) (.List => ListItem(printResetFunc(SN))) + +endmodule \ No newline at end of file diff --git a/test/helper/a.test b/test/helper/a.test new file mode 100644 index 0000000..573541a --- /dev/null +++ b/test/helper/a.test @@ -0,0 +1 @@ +0 diff --git a/test/helper/test.k b/test/helper/test.k new file mode 100644 index 0000000..8f5f09c --- /dev/null +++ b/test/helper/test.k @@ -0,0 +1,22 @@ +require "../../src/helper/util.k" + +module TEST +imports UTIL + + +configuration + + $PGM:Int + false + .Map + .List + + +rule false => true + .Map => (((1 |-> 2):Map (2 |-> 0):Map) (0 |-> 1):Map):Map + +rule true + M:Map + .List => toIntArray(M) + +endmodule \ No newline at end of file diff --git a/test/mop/test.mop b/test/mop/test.mop index 518589f..2279185 100644 --- a/test/mop/test.mop +++ b/test/mop/test.mop @@ -22,6 +22,8 @@ PipedOutputStream_UnconnectedWrite(PipedOutputStream o) { write -> yes ] +//alias match = yes + @fail { } diff --git a/test/rvm/Test-dupEvent.rvm b/test/rvm/Test-dupEvent.rvm new file mode 100644 index 0000000..c2574ac --- /dev/null +++ b/test/rvm/Test-dupEvent.rvm @@ -0,0 +1,24 @@ +package rvm; + +import java.io.*; +Test (int o){ + event create(){ + int i; + } + event close(){ + int i; + } + + event create(){ + int k; + } + + ere: x & x + + @match { + int j; + } + + + +} diff --git a/test/rvm/Test-partialFunction.rvm b/test/rvm/Test-partialFunction.rvm new file mode 100644 index 0000000..e4bbbbf --- /dev/null +++ b/test/rvm/Test-partialFunction.rvm @@ -0,0 +1,29 @@ +package rvm; + +import java.io.*; +Test (int o){ + + event hasnext(Iterator i) {} // {3, 1, 3, 3} + event next(Iterator i) {} // {2, 0, 2, 3} + + fsm : + start [ + next -> unsafe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + ] + + // alias match = unsafe, start + + @match { + int j; + } + + + +} diff --git a/test/rvm/Test-undefinedEvent.rvm b/test/rvm/Test-undefinedEvent.rvm new file mode 100644 index 0000000..6ab691e --- /dev/null +++ b/test/rvm/Test-undefinedEvent.rvm @@ -0,0 +1,24 @@ +package rvm; + +import java.io.*; +Test (int o){ + + event hasnext(Iterator i) {} // after + event next(Iterator i) {} // before + + fsm : + start [ + foo -> safe //event foo is undefined, should report error. + + next -> unsafe + hasnext -> safe + ] + + + @match { + int j; + } + + + +} diff --git a/test/rvm/Test-undefinedState.rvm b/test/rvm/Test-undefinedState.rvm new file mode 100644 index 0000000..39e1144 --- /dev/null +++ b/test/rvm/Test-undefinedState.rvm @@ -0,0 +1,31 @@ +package rvm; + +import java.io.*; +Test (int o){ + + event hasnext(Iterator i) {} // after + event next(Iterator i) {} // before + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> bar //state bar is undefined, should report error. + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + // alias match = unsafe, start + + @match { + int j; + } + + + +} diff --git a/test/rvm/fsm/rvc/HasNext/HasNext.rvm b/test/rvm/fsm/rvc/HasNext/HasNext.rvm new file mode 100644 index 0000000..35efe4f --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/HasNext.rvm @@ -0,0 +1,36 @@ +package rvm; + + +HasNext(Iterator i) { + event hasnext(Iterator i) {} + event next(Iterator i) {} + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + + @unsafe { +fprintf(stderr, "next called without hasNext!\n"); + } + +} + + + + + + + + + diff --git a/test/rvm/fsm/rvc/HasNext/Makefile b/test/rvm/fsm/rvc/HasNext/Makefile new file mode 100644 index 0000000..bb4c71f --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/Makefile @@ -0,0 +1,5 @@ +all: clean + +clean: + rm __RVC_*_Monitor* + diff --git a/test/rvm/fsm/rvc/HasNext/Test.rvm b/test/rvm/fsm/rvc/HasNext/Test.rvm new file mode 100644 index 0000000..5da5e06 --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/Test.rvm @@ -0,0 +1,59 @@ +package rvm; + +#include +#include "string.h" +#include + +Test (int o){ + int foo = 2; + + + event hasnext(Iterator i) {} // {1, 1, 1, 3} + event next(Iterator i) { int i = 0; {i--;} int j=i+ 2 ; +{{{}}} } // {2, 0, 2, 3} + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + @start { + int j; +fprintf(stderr, "Start!\n"); + } + + @unsafe { + fprintf(stderr, "It's not safe.\n"); + } + + + fsm : + start2 [ + next -> unsafe2 + hasnext -> safe2 + ] + safe2 [ + next -> start2 + hasnext -> safe2 + ] + unsafe2 [ + next -> unsafe2 + hasnext -> safe2 + ] + + @unsafe2 { + int k; +fprintf(stderr, "It's in state unsafe2.\n"); + } + + +} diff --git a/test/rvm/fsm/rvc/HasNext/runHasNext.sh b/test/rvm/fsm/rvc/HasNext/runHasNext.sh new file mode 100755 index 0000000..3ea0e9e --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/runHasNext.sh @@ -0,0 +1,3 @@ +kompile -d . ../../../../src/rvm/rvc.k + +krun HasNext.rvm diff --git a/test/rvm/fsm/rvc/HasNext/runTest.sh b/test/rvm/fsm/rvc/HasNext/runTest.sh new file mode 100755 index 0000000..60f0242 --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/runTest.sh @@ -0,0 +1,3 @@ +kompile -d . ../../../../src/rvm/rvc.k + +krun Test.rvm diff --git a/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.c b/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.c new file mode 100644 index 0000000..6693696 --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.c @@ -0,0 +1,47 @@ +package rvm; + + + +#include +static int __RVC_state = 0; + + + +int __RVC_HasNext_unsafe = 0; + +void +__RVC_HasNext_reset(void) +{ + __RVC_state = 0; + } + +static int __RVC_HASNEXT_NEXT[] = {2, 0, 2, }; +static int __RVC_HASNEXT_HASNEXT[] = {1, 1, 1, }; + +void +__RVC_HasNext_next(Iterator i) +{ +{} +__RVC_state = __RVC_HASNEXT_NEXT[__RVC_state]; + __RVC_HasNext_unsafe = __RVC_state == 2; +if(__RVC_HasNext_unsafe) +{ +{ +fprintf(stderr, "next called without hasNext!\n"); + }} +} + +void +__RVC_HasNext_hasnext(Iterator i) +{ +{} +__RVC_state = __RVC_HASNEXT_HASNEXT[__RVC_state]; + __RVC_HasNext_unsafe = __RVC_state == 2; +if(__RVC_HasNext_unsafe) +{ +{ +fprintf(stderr, "next called without hasNext!\n"); + }} +} + + diff --git a/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.h b/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.h new file mode 100644 index 0000000..9dcb49c --- /dev/null +++ b/test/rvm/fsm/rvc/HasNext/rv-monitor-output/__RVC_HasNext_Monitor.h @@ -0,0 +1,10 @@ +#ifndef __RVC_HASNEXT_MONITOR_H +#define __RVC_HASNEXT_MONITOR_H +void +__RVC_HasNext_reset(void); +void +__RVC_HasNext_next(Iterator i); +void +__RVC_HasNext_hasnext(Iterator i); + +#endif diff --git a/test/rvm/fsm/rvc/SeatBelt/Makefile b/test/rvm/fsm/rvc/SeatBelt/Makefile new file mode 100644 index 0000000..836d9d9 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/Makefile @@ -0,0 +1,22 @@ +all: compile test1 test2 + +compile: ../../../../../src/rvm/rvc.k + kompile -d . ../../../../../src/rvm/rvc.k + +__RVC_SeatBelt_Monitor.c: seatbelt.rvm + krun seatbelt.rvm + +test1: __RVC_SeatBelt_Monitor.c + gcc test_1/seatbelt.c __RVC_SeatBelt_Monitor.c -o test1_k + +test2: __RVC_SeatBelt_Monitor.c + gcc test_2/seatbelt.c __RVC_SeatBelt_Monitor.c -o test2_k + +clean: + rm -f test1_k test2_k __RVC_* actualOut actualErr + +test: test1_k test2_k + -@./test1_k 1> actualOut 2> actualErr + -@./test2_k 1>> actualOut 2>> actualErr + diff tests/test.expected.out actualOut + diff tests/test.expected.err actualErr diff --git a/test/rvm/fsm/rvc/SeatBelt/Makefile_rvc_java_backend b/test/rvm/fsm/rvc/SeatBelt/Makefile_rvc_java_backend new file mode 100644 index 0000000..96fcfe3 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/Makefile_rvc_java_backend @@ -0,0 +1,17 @@ +all: test1 test2 + +__RVC_SeatBelt_Monitor.c: seatbelt.rvm + ../../../../bin/rv-monitor -c seatbelt.rvm + +test1: __RVC_SeatBelt_Monitor.c + gcc test_1/seatbelt.c __RVC_SeatBelt_Monitor.c -o test1 + +test2: __RVC_SeatBelt_Monitor.c + gcc test_2/seatbelt.c __RVC_SeatBelt_Monitor.c -o test2 + +clean: + rm -f test1 test2 __RVC_* + +test: all + -@./test1 + -@./test2 diff --git a/test/rvm/fsm/rvc/SeatBelt/README b/test/rvm/fsm/rvc/SeatBelt/README new file mode 100644 index 0000000..c102019 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/README @@ -0,0 +1,33 @@ +Linux: +To run test_1 +../../../../bin/rv-monitor -c seatbelt.rvm + +gcc test_1/seatbelt.c __RVC_SeatBelt_Monitor.c -o seatbelt + +./seatbelt + + +To run test_2 +../../../../bin/rv-monitor -c seatbelt.rvm + +gcc test_2/seatbelt.c __RVC_SeatBelt_Monitor.c -o seatbelt + +./seatbelt + + + +Windows: +To run test_1 +../../../../bin/rv-monitor -c seatbelt.rvm + +gcc test_1/seatbelt.c __RVC_SeatBelt_Monitor.c -o seatbelt.exe + +seatbelt.exe + + +To run test_2 +../../../../bin/rv-monitor -c seatbelt.rvm + +gcc test_2/seatbelt.c __RVC_SeatBelt_Monitor.c -o seatbelt.exe + +seatbelt.exe diff --git a/test/rvm/fsm/rvc/SeatBelt/expectedOutput b/test/rvm/fsm/rvc/SeatBelt/expectedOutput new file mode 100644 index 0000000..b8a4e4e --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/expectedOutput @@ -0,0 +1,12 @@ +Test 1 +Test 1 +Seat belt attached. +set max speed to user input. +Seat belt removed. +set max speed to 10 mph. +Seat belt attached. +set max speed to user input. +Test 2 +Test 2 +Seat belt attached. +set max speed to user input. diff --git a/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.c b/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.c new file mode 100644 index 0000000..4342d48 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.c @@ -0,0 +1,58 @@ +#include + +#include +static int __RVC_state = 0; + + + +int __RVC_SeatBelt_safe = 0; +int __RVC_SeatBelt_unsafe = 0; + +void +__RVC_SeatBelt_reset(void) +{ + __RVC_state = 0; + } + +static int __RVC_SEATBELT_SEATBELTREMOVED[] = {-1,0, }; +static int __RVC_SEATBELT_SEATBELTATTACHED[] = {1, -1,}; + +void +__RVC_SeatBelt_seatBeltRemoved() +{ +{fprintf(stderr, "Seat belt removed.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTREMOVED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + +void +__RVC_SeatBelt_seatBeltAttached() +{ +{fprintf(stderr, "Seat belt attached.\n");} +__RVC_state = __RVC_SEATBELT_SEATBELTATTACHED[__RVC_state]; + __RVC_SeatBelt_safe = __RVC_state == 1; + __RVC_SeatBelt_unsafe = __RVC_state == 0; +if(__RVC_SeatBelt_safe) +{ +{ + fprintf(stderr, "set max speed to user input.\n"); + }} +if(__RVC_SeatBelt_unsafe) +{ +{ + fprintf(stderr, "set max speed to 10 mph.\n"); + }} +} + + diff --git a/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.h b/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.h new file mode 100644 index 0000000..8c1dc40 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/rv-monitor-generated-monitor-code/__RVC_SeatBelt_Monitor.h @@ -0,0 +1,10 @@ +#ifndef __RVC_SEATBELT_MONITOR_H +#define __RVC_SEATBELT_MONITOR_H +void +__RVC_SeatBelt_reset(void); +void +__RVC_SeatBelt_seatBeltRemoved(); +void +__RVC_SeatBelt_seatBeltAttached(); + +#endif diff --git a/test/rvm/fsm/rvc/SeatBelt/seatbelt.rvm b/test/rvm/fsm/rvc/SeatBelt/seatbelt.rvm new file mode 100644 index 0000000..bd07116 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/seatbelt.rvm @@ -0,0 +1,23 @@ +#include + +SeatBelt() { + event seatBeltRemoved(){fprintf(stderr, "Seat belt removed.\n");} + + event seatBeltAttached() {fprintf(stderr, "Seat belt attached.\n");} + + fsm : unsafe [ + seatBeltAttached -> safe + ] + safe [ + seatBeltRemoved -> unsafe + ] + + @safe { + fprintf(stderr, "set max speed to user input.\n"); + } + + @unsafe { + fprintf(stderr, "set max speed to 10 mph.\n"); + } + +} diff --git a/test/rvm/fsm/rvc/SeatBelt/test1 b/test/rvm/fsm/rvc/SeatBelt/test1 new file mode 100755 index 0000000..9ba74a2 Binary files /dev/null and b/test/rvm/fsm/rvc/SeatBelt/test1 differ diff --git a/test/rvm/fsm/rvc/SeatBelt/test2 b/test/rvm/fsm/rvc/SeatBelt/test2 new file mode 100755 index 0000000..7ccc48f Binary files /dev/null and b/test/rvm/fsm/rvc/SeatBelt/test2 differ diff --git a/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.c b/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.c new file mode 100644 index 0000000..cef6242 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.c @@ -0,0 +1,10 @@ +#include "../__RVC_SeatBelt_Monitor.h" +#include + +int main() { + fprintf(stdout, "Test 1\n"); + fprintf(stderr, "Test 1\n"); + __RVC_SeatBelt_seatBeltAttached(); + __RVC_SeatBelt_seatBeltRemoved(); + __RVC_SeatBelt_seatBeltAttached(); +} diff --git a/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.output b/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.output new file mode 100644 index 0000000..ca9b3c7 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/test_1/seatbelt.output @@ -0,0 +1,6 @@ +Seat belt atatched. +Seat belt removed. +Seat belt atatched. +set max speed to user input. +set max speed to 10 mph. +set max speed to user input. diff --git a/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.c b/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.c new file mode 100644 index 0000000..19cb2c6 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.c @@ -0,0 +1,8 @@ +#include "../__RVC_SeatBelt_Monitor.h" +#include + +int main() { + fprintf(stdout, "Test 2\n"); + fprintf(stderr, "Test 2\n"); + __RVC_SeatBelt_seatBeltAttached(); +} diff --git a/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.output b/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.output new file mode 100644 index 0000000..d696f85 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/test_2/seatbelt.output @@ -0,0 +1,2 @@ +Seat belt attached. +set max speed to user input. diff --git a/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.err b/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.err new file mode 100644 index 0000000..0851f11 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.err @@ -0,0 +1,10 @@ +Test 1 +Seat belt attached. +set max speed to user input. +Seat belt removed. +set max speed to 10 mph. +Seat belt attached. +set max speed to user input. +Test 2 +Seat belt attached. +set max speed to user input. diff --git a/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.out b/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.out new file mode 100644 index 0000000..998c014 --- /dev/null +++ b/test/rvm/fsm/rvc/SeatBelt/tests/test.expected.out @@ -0,0 +1,2 @@ +Test 1 +Test 2 diff --git a/test/rvm/fsm/rvj/HasNext.rvm b/test/rvm/fsm/rvj/HasNext.rvm new file mode 100644 index 0000000..96bce67 --- /dev/null +++ b/test/rvm/fsm/rvj/HasNext.rvm @@ -0,0 +1,48 @@ +package rvm; +import java.io.*; +import java.util.*; + +// This property specifies that a program does +// not call the hasnext method before the next +// method of an iterator. +// This property is borrowed from tracematches +// (see ECOOP'07 http://abc.comlab.ox.ac.uk/papers) + +HasNext(Iterator i) { + event hasnext(Iterator i) {} // after + event next(Iterator i) {} // before + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + // alias match = unsafe + // alias unmatch = safe + + @match { + System.out.println("next called without hasNext!"); + } + + @unmatch { + System.out.println("safe"); + } +} + + + + + + + + + diff --git a/test/rvm/fsm/rvj/HasNextRuntimeMonitor.java b/test/rvm/fsm/rvj/HasNextRuntimeMonitor.java new file mode 100644 index 0000000..7580cb7 --- /dev/null +++ b/test/rvm/fsm/rvj/HasNextRuntimeMonitor.java @@ -0,0 +1,334 @@ +package rvm; +import java.io.*; +import java.util.*; +import java.util.concurrent.*; +import java.util.concurrent.locks.*; +import java.lang.ref.*; +import com.runtimeverification.rvmonitor.java.rt.*; +import com.runtimeverification.rvmonitor.java.rt.ref.*; +import com.runtimeverification.rvmonitor.java.rt.table.*; +import com.runtimeverification.rvmonitor.java.rt.tablebase.AbstractIndexingTree; +import com.runtimeverification.rvmonitor.java.rt.tablebase.SetEventDelegator; +import com.runtimeverification.rvmonitor.java.rt.tablebase.TableAdopter.Tuple2; +import com.runtimeverification.rvmonitor.java.rt.tablebase.TableAdopter.Tuple3; +import com.runtimeverification.rvmonitor.java.rt.tablebase.IDisableHolder; +import com.runtimeverification.rvmonitor.java.rt.tablebase.IMonitor; +import com.runtimeverification.rvmonitor.java.rt.tablebase.DisableHolder; +import com.runtimeverification.rvmonitor.java.rt.tablebase.TerminatedMonitorCleaner; +import java.util.concurrent.atomic.AtomicInteger; + +final class HasNextMonitor_Set extends com.runtimeverification.rvmonitor.java.rt.tablebase.AbstractMonitorSet { + + HasNextMonitor_Set(){ + this.size = 0; + this.elements = new HasNextMonitor[4]; + } + final void event_hasnext(Iterator i) { + int numAlive = 0 ; + for(int i_1 = 0; i_1 < this.size; i_1++){ + HasNextMonitor monitor = this.elements[i_1]; + if(!monitor.isTerminated()){ + elements[numAlive] = monitor; + numAlive++; + + final HasNextMonitor monitorfinalMonitor = monitor; + monitor.Prop_1_event_hasnext(i); + if(monitorfinalMonitor.Prop_1_Category_match) { + monitorfinalMonitor.Prop_1_handler_match(); + } + } + } + for(int i_1 = numAlive; i_1 < this.size; i_1++){ + this.elements[i_1] = null; + } + size = numAlive; + } + final void event_next(Iterator i) { + int numAlive = 0 ; + for(int i_1 = 0; i_1 < this.size; i_1++){ + HasNextMonitor monitor = this.elements[i_1]; + if(!monitor.isTerminated()){ + elements[numAlive] = monitor; + numAlive++; + + final HasNextMonitor monitorfinalMonitor = monitor; + monitor.Prop_1_event_next(i); + if(monitorfinalMonitor.Prop_1_Category_match) { + monitorfinalMonitor.Prop_1_handler_match(); + } + } + } + for(int i_1 = numAlive; i_1 < this.size; i_1++){ + this.elements[i_1] = null; + } + size = numAlive; + } +} + +class HasNextMonitor extends com.runtimeverification.rvmonitor.java.rt.tablebase.AbstractAtomicMonitor implements Cloneable, com.runtimeverification.rvmonitor.java.rt.RVMObject { + protected Object clone() { + try { + HasNextMonitor ret = (HasNextMonitor) super.clone(); + ret.pairValue = new AtomicInteger(pairValue.get()); + return ret; + } + catch (CloneNotSupportedException e) { + throw new InternalError(e.toString()); + } + } + + static final int Prop_1_transition_hasnext[] = {2, 2, 2, 3};; + static final int Prop_1_transition_next[] = {1, 1, 0, 3};; + + volatile boolean Prop_1_Category_match = false; + + private AtomicInteger pairValue; + + HasNextMonitor() { + this.pairValue = new AtomicInteger(this.calculatePairValue(-1, 0) ) ; + + } + + @Override public final int getState() { + return this.getState(this.pairValue.get() ) ; + } + @Override public final int getLastEvent() { + return this.getLastEvent(this.pairValue.get() ) ; + } + private final int getState(int pairValue) { + return (pairValue & 3) ; + } + private final int getLastEvent(int pairValue) { + return (pairValue >> 2) ; + } + private final int calculatePairValue(int lastEvent, int state) { + return (((lastEvent + 1) << 2) | state) ; + } + + private final int handleEvent(int eventId, int[] table) { + int nextstate; + while (true) { + int oldpairvalue = this.pairValue.get() ; + int oldstate = this.getState(oldpairvalue) ; + nextstate = table [ oldstate ]; + int nextpairvalue = this.calculatePairValue(eventId, nextstate) ; + if (this.pairValue.compareAndSet(oldpairvalue, nextpairvalue) ) { + break; + } + } + return nextstate; + } + + final boolean Prop_1_event_hasnext(Iterator i) { + {} + + int nextstate = this.handleEvent(0, Prop_1_transition_hasnext) ; + this.Prop_1_Category_match = nextstate == 1; + + return true; + } + + final boolean Prop_1_event_next(Iterator i) { + {} + + int nextstate = this.handleEvent(1, Prop_1_transition_next) ; + this.Prop_1_Category_match = nextstate == 1; + + return true; + } + + final void Prop_1_handler_match (){ + { + System.out.println("next called without hasNext!"); + } + + } + + final void reset() { + this.pairValue.set(this.calculatePairValue(-1, 0) ) ; + + Prop_1_Category_match = false; + } + + // RVMRef_i was suppressed to reduce memory overhead + + //alive_parameters_0 = [Iterator i] + boolean alive_parameters_0 = true; + + @Override + protected final void terminateInternal(int idnum) { + int lastEvent = this.getLastEvent(); + + switch(idnum){ + case 0: + alive_parameters_0 = false; + break; + } + switch(lastEvent) { + case -1: + return; + case 0: + //hasnext + //alive_i + if(!(alive_parameters_0)){ + RVM_terminated = true; + return; + } + break; + + case 1: + //next + //alive_i + if(!(alive_parameters_0)){ + RVM_terminated = true; + return; + } + break; + + } + return; + } + + public static int getNumberOfEvents() { + return 2; + } + + public static int getNumberOfStates() { + return 4; + } + +} + +public final class HasNextRuntimeMonitor implements com.runtimeverification.rvmonitor.java.rt.RVMObject { + private static com.runtimeverification.rvmonitor.java.rt.map.RVMMapManager HasNextMapManager; + static { + HasNextMapManager = new com.runtimeverification.rvmonitor.java.rt.map.RVMMapManager(); + HasNextMapManager.start(); + } + + // Declarations for the Lock + static final ReentrantLock HasNext_RVMLock = new ReentrantLock(); + static final Condition HasNext_RVMLock_cond = HasNext_RVMLock.newCondition(); + + private static boolean HasNext_activated = false; + + // Declarations for Indexing Trees + private static Object HasNext_i_Map_cachekey_i; + private static HasNextMonitor HasNext_i_Map_cachevalue; + private static final MapOfMonitor HasNext_i_Map = new MapOfMonitor(0) ; + + public static int cleanUp() { + int collected = 0; + // indexing trees + collected += HasNext_i_Map.cleanUpUnnecessaryMappings(); + return collected; + } + + // Removing terminated monitors from partitioned sets + static { + TerminatedMonitorCleaner.start() ; + } + // Setting the behavior of the runtime library according to the compile-time option + static { + RuntimeOption.enableFineGrainedLock(false) ; + } + + public static final void hasnextEvent(Iterator i) { + HasNext_activated = true; + while (!HasNext_RVMLock.tryLock()) { + Thread.yield(); + } + + CachedWeakReference wr_i = null; + MapOfMonitor matchedLastMap = null; + HasNextMonitor matchedEntry = null; + boolean cachehit = false; + if ((i == HasNext_i_Map_cachekey_i) ) { + matchedEntry = HasNext_i_Map_cachevalue; + cachehit = true; + } + else { + wr_i = new CachedWeakReference(i) ; + { + // FindOrCreateEntry + MapOfMonitor itmdMap = HasNext_i_Map; + matchedLastMap = itmdMap; + HasNextMonitor node_i = HasNext_i_Map.getNodeEquivalent(wr_i) ; + matchedEntry = node_i; + } + } + // D(X) main:1 + if ((matchedEntry == null) ) { + if ((wr_i == null) ) { + wr_i = new CachedWeakReference(i) ; + } + // D(X) main:4 + HasNextMonitor created = new HasNextMonitor() ; + matchedEntry = created; + matchedLastMap.putNode(wr_i, created) ; + } + // D(X) main:8--9 + final HasNextMonitor matchedEntryfinalMonitor = matchedEntry; + matchedEntry.Prop_1_event_hasnext(i); + if(matchedEntryfinalMonitor.Prop_1_Category_match) { + matchedEntryfinalMonitor.Prop_1_handler_match(); + } + + if ((cachehit == false) ) { + HasNext_i_Map_cachekey_i = i; + HasNext_i_Map_cachevalue = matchedEntry; + } + + HasNext_RVMLock.unlock(); + } + + public static final void nextEvent(Iterator i) { + HasNext_activated = true; + while (!HasNext_RVMLock.tryLock()) { + Thread.yield(); + } + + CachedWeakReference wr_i = null; + MapOfMonitor matchedLastMap = null; + HasNextMonitor matchedEntry = null; + boolean cachehit = false; + if ((i == HasNext_i_Map_cachekey_i) ) { + matchedEntry = HasNext_i_Map_cachevalue; + cachehit = true; + } + else { + wr_i = new CachedWeakReference(i) ; + { + // FindOrCreateEntry + MapOfMonitor itmdMap = HasNext_i_Map; + matchedLastMap = itmdMap; + HasNextMonitor node_i = HasNext_i_Map.getNodeEquivalent(wr_i) ; + matchedEntry = node_i; + } + } + // D(X) main:1 + if ((matchedEntry == null) ) { + if ((wr_i == null) ) { + wr_i = new CachedWeakReference(i) ; + } + // D(X) main:4 + HasNextMonitor created = new HasNextMonitor() ; + matchedEntry = created; + matchedLastMap.putNode(wr_i, created) ; + } + // D(X) main:8--9 + final HasNextMonitor matchedEntryfinalMonitor = matchedEntry; + matchedEntry.Prop_1_event_next(i); + if(matchedEntryfinalMonitor.Prop_1_Category_match) { + matchedEntryfinalMonitor.Prop_1_handler_match(); + } + + if ((cachehit == false) ) { + HasNext_i_Map_cachekey_i = i; + HasNext_i_Map_cachevalue = matchedEntry; + } + + HasNext_RVMLock.unlock(); + } + +} diff --git a/test/rvm/fsm/rvj/Test.rvm b/test/rvm/fsm/rvj/Test.rvm new file mode 100644 index 0000000..eb60775 --- /dev/null +++ b/test/rvm/fsm/rvj/Test.rvm @@ -0,0 +1,31 @@ +package rvm; + +import java.io.*; +Test (int o){ + + event hasnext(Iterator i) {} // {1, 1, 1, 3} + event next(Iterator i) {} // {2, 0, 2, 3} + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + // alias match = unsafe, start + + @safe { + int j; + } + + + +} diff --git a/test/rvm/Test2.rvm b/test/rvm/fsm/rvj/Test2.rvm similarity index 100% rename from test/rvm/Test2.rvm rename to test/rvm/fsm/rvj/Test2.rvm diff --git a/test/rvm/Test.rvm b/test/rvm/fsm/rvj/Test3.rvm similarity index 81% rename from test/rvm/Test.rvm rename to test/rvm/fsm/rvj/Test3.rvm index 9ba5a1b..d4a5fc8 100644 --- a/test/rvm/Test.rvm +++ b/test/rvm/fsm/rvj/Test3.rvm @@ -2,6 +2,10 @@ package rvm; import java.io.*; Test (int o){ + x=2; + c { int z = 10 ; } + y=1; + event create(){ int i; } diff --git a/test/rvm/fsm/rvj/Test4.rvm b/test/rvm/fsm/rvj/Test4.rvm new file mode 100644 index 0000000..bb08c27 --- /dev/null +++ b/test/rvm/fsm/rvj/Test4.rvm @@ -0,0 +1,56 @@ +package rvm; + +import java.io.*; +Test (int o){ + String x = "foo"; + class bar { + private int foo() { return 1; } + } + + event hasnext(Iterator i) {} // {1, 1, 1, 3} + event next(Iterator i) { int i = 0; {i--;} int j=i+ 2 ; +{{{}}} } // {2, 0, 2, 3} + + fsm : + start [ + next -> unsafe + hasnext -> safe + ] + safe [ + next -> start + hasnext -> safe + ] + unsafe [ + next -> unsafe + hasnext -> safe + ] + + @start { + int j; + } + + @unsafe { + System.err.println("It is not safe"); + } + + + fsm : + start2 [ + next -> unsafe2 + hasnext -> safe2 + ] + safe2 [ + next -> start2 + hasnext -> safe2 + ] + unsafe2 [ + next -> unsafe2 + hasnext -> safe2 + ] + + @unsafe2 { + int k; + } + + +} diff --git a/test/rvm/fsm/rvj/info-from-formula b/test/rvm/fsm/rvj/info-from-formula new file mode 100644 index 0000000..7f4b8ce --- /dev/null +++ b/test/rvm/fsm/rvj/info-from-formula @@ -0,0 +1,22 @@ +events: hasnext next + +categories: unmatch match + +logic: fsm + +formula: +start[ + next -> unsafe + hasnext -> safe +] +safe[ + next -> start + hasnext -> safe +] +unsafe[ + next -> unsafe + hasnext -> safe +] +alias unmatch = safe +alias match = unsafe + diff --git a/test/rvm/fsm/rvj/rv-monitor-shell-result b/test/rvm/fsm/rvj/rv-monitor-shell-result new file mode 100644 index 0000000..5d88e98 --- /dev/null +++ b/test/rvm/fsm/rvj/rv-monitor-shell-result @@ -0,0 +1,28 @@ +properties={safe condition=$state$ == 2, match condition=$state$ == 1, state declaration=int $state$; +static final int $transition_hasnext$[] = {2, 2, 2, 3};; +static final int $transition_next$[] = {1, 1, 0, 3};; +, monitoring body=, monitored events for set=hasnext:{ + $monitor$.$state$ = $transition_hasnext$[$monitor$.$state$]; +} + +next:{ + $monitor$.$state$ = $transition_next$[$monitor$.$state$]; +} + +, match coenables={next=[[next], [next, hasnext]], hasnext=[[next], [next, hasnext]]} +, unsafe condition=$state$ == 1, monitored events=hasnext:{ + $state$ = $transition_hasnext$[$state$]; +} + +next:{ + $state$ = $transition_next$[$state$]; +} + +, match enables={next=[[], [next], [hasnext], [next, hasnext]], hasnext=[[], [next], [hasnext], [next, hasnext]]}, reset=$state$ = 0; +, start condition=$state$ == 0, fail condition=$state$ == 3 +, initialization=$state$ = 0; +, nonfail condition=$state$ != 3 +, state declaration for set=static final int $transition_hasnext$[] = {2, 2, 2, 3};; +static final int $transition_next$[] = {1, 1, 0, 3};; +} +startEvents=[next, hasnext] diff --git a/version.txt b/version.txt new file mode 100644 index 0000000..453c3ae --- /dev/null +++ b/version.txt @@ -0,0 +1,4 @@ +K: [github](https://github.com/kframework/k) +ee3bdc2066c29d7a0c7f29ab85c7bcaf1332b173 + +Mar 31: stable