Code gen

.gitignore

@@ -3,3 +3,4 @@
 test/rvm/property-db
 test/mop/property-db
 *-kompiled/
+*.bak

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.

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.

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 <k> $main4 => $eventFuncs(size(EL)) </k>
+        <events> EL:List </events>
+        <states> _:Map => .Map </states>
+        <code> CL:List (.List => ListItem("\n")) </code>
+
+    rule <k> $eventFuncs(I:Int) => ($eFunc(0), $eventFuncs(I)) </k>
+    when I >Int 0
+
+    rule <k> $eventFuncs(I:Int) => .K </k>
+    when I <=Int 0
+
+    rule <k> $eFunc(I:Int), $eventFuncs(0) => .K </k>
+    <methodBody> .K </methodBody>
+    <k2> .K </k2>
+
+    rule <k> $eFunc(I:Int), $eventFuncs(J:Int) => $eFunc(I +Int 1), $eventFuncs(J -Int 1) </k>
+    <methodBody> .K => $eFunc(I) </methodBody>
+    <tmpList> _ => .List </tmpList>
+            <code> CL:List (.List => ListItem("\n")) </code>
+    when J >Int 0
+
+    rule     <methodBody> $eFunc(I:Int) => $methHeader(I) {$mbody} </methodBody>
+
+    //print method header
+    rule <methodBody> $methHeader(I:Int) {$mbody} => $mbody2 </methodBody>
+    <events> EL:List </events>
+                          <specName> SN:String </specName>
+                      //the params of each event, indexed by event id
+                      <eventParams> EPs:List </eventParams>
+                      //the list of event action code, indexed by event id.
+                      <eventAction> EAs:List </eventAction>
+    <code> 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
+    </code>
+
+    <header> HeaderCode:List (.List =>
+        ListItem(printMethodHeader(SN, getStringI(EL, I), getStringI(EPs, I)) +String ";"))
+    </header>
+
+    //store the current event name which will be used to infer event transition function.
+    <tmpList> .List => ListItem(getStringI(EL, I)) </tmpList>
+
+
+//////////////////////////////////////////////////////////////////////////////
+    //state updates
+   rule <methodBody> $mbody2 => ($stateUpdates(PS) ;; $handlers) </methodBody>
+        <propSize> PS:Int </propSize>
+
+   rule <methodBody> ($stateUpdates(PS:Int) ;; $handlers) =>
+        $sUpdate(0) ,, $stateUpdates(PS) ;; $handlers
+        </methodBody>
+
+   rule <methodBody>
+        ($sUpdate(I:Int) ,, $stateUpdates(PS:Int) ;; $handlers)
+        => $handlers
+        </methodBody>
+        when PS <=Int 0
+
+   rule <methodBody>
+            ($sUpdate(I:Int) ,, $stateUpdates(PS:Int) ;; $handlers) =>
+            ($sUpdate(I +Int 1) ,, $stateUpdates(PS -Int 1) ;; $handlers)
+            </methodBody>
+
+            <k2> .K => $gsUpdate(I), $lsUpdates(getSize(SML, I)) </k2>
+          <stateNameMap> SML:List </stateNameMap>
+
+            //cache the state map of property I
+            <states> .Map => getMapI(SML, I) </states>
+
+          <propNum> _:Int => I </propNum> //the cur property rank is I
+when PS >Int 0
+
+//finish the state updates code
+       rule <methodBody>
+            ($sUpdate(I:Int) ,, $stateUpdates(0) ;; $handlers) =>
+            $handlers
+            </methodBody>
+            <k2> .K </k2>
+
+//generate global state update code
+//when the property size > 1, the event transition function will have property rank as prefix
+rule <k2> $gsUpdate(I:Int), $lsUpdates(J:Int) => $lsUpdates(J) </k2>
+     <specName> SN:String </specName>
+     <tmpList> ListItem(EN:String) </tmpList> //the tmpList stores the current event name
+<code> C:List (.List => ListItem(
+globalStateUpdate(globalStateVarI(I), propXEventE(SN, I, EN))
+))
+</code>
+<propSize> PS:Int </propSize>
+when PS >Int 1
+
+//only a single property is defined
+rule <k2> $gsUpdate(I:Int), $lsUpdates(J:Int) => $lsUpdates(J) </k2>
+     <specName> SN:String </specName>
+     <tmpList> ListItem(EN:String) </tmpList> //the tmpList stores the current event name
+<code> C:List (.List => ListItem(
+globalStateUpdate(globalStateVarI(I), propXEventE(SN, EN))
+))
+</code>
+<propSize> PS:Int </propSize>
+when PS <=Int 1
+
+//update local states
+rule <k2> $lsUpdate(I:Int) $lsUpdates(0) => .K </k2>
+<states> M:Map => .Map </states>
+
+
+rule <k2> $lsUpdates(I:Int) => $lsUpdate(0) $lsUpdates(I) </k2>
+
+rule <k2> $lsUpdate(I:Int) $lsUpdates(J:Int) => $lsUpdate(I +Int 1) $lsUpdates(J -Int 1) </k2>
+<propNum> G:Int </propNum>
+<specName> SN:String </specName>
+<states> M:Map </states>
+//the three args are local state var, global state var, state rank
+//localStateVarI(spec name, property rank, state name)
+<code> C:List (.List => ListItem(localStateUpdate( localStateVarI(SN, G, getStrKey(M, I)),
+globalStateVarI(G), I)))
+</code>
+when J >Int 0
+
+//handler code and closing parenthesis
+rule <methodBody> $handlers => .K </methodBody>
+<k2> .K </k2>
+<handlersList> HDM:Map </handlersList>
+<code> C:List (.List => getHandlerCode(HDM)) (.List => ListItem("\n}\n")) </code>
+
+endmodule

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