Lazy generation of the lable table and some enum stuff.

kframework · Aug 21, 2013 · 656d459 · 656d459
1 parent 1903c1f
commit 656d459
Show file tree

Hide file tree

Showing 5 changed files with 122 additions and 129 deletions.
diff --git a/cil-semantics/cil-decl.k b/cil-semantics/cil-decl.k
@@ -112,10 +112,8 @@ module CIL-DECL
     <k>
       defineFun(F:Ptr, T:Type, Ps:Params, FB:FunBody)
     => lower-break-continue-to-goto-control(F) 
-      ~> make-goto-table-control(F)
       //~> propagate-constants(F)
     ...</k>
-    // <frame-fun-id> _ => F </frame-fun-id>
     <funs>...
       .Bag
     =>
@@ -285,116 +283,6 @@ module CIL-DECL
   rule normLabels(FB:FunBody)
     => #visit(FB, 'normLabelsVisitor, 0, 'needsLabelNorm)::FunBody
 
-  /*
-   * Compute the goto table (Map{Label, Stmt})
-   */
-  syntax K ::= "make-goto-table-control" "(" Ptr ")"
-  rule
-    <k> make-goto-table-control(F:Ptr) ...</k>
-    <fun>...
-      <fun-id> F </fun-id>
-      <body> { _:VarDecls { Ss:Stmts } } </body>
-    ...</fun>
-    <make-goto-table>
-      <make-goto-table-enabled> false => true </make-goto-table-enabled>
-      <make-goto-table-tasks>
-        (.Bag => 
-          <make-goto-table-task>
-            <make-goto-table-stmts> Ss </make-goto-table-stmts>
-            <make-goto-table-cont> .Stmts </make-goto-table-cont>
-          </make-goto-table-task>
-        )
-      </make-goto-table-tasks>
-    </make-goto-table>
-  [structural]
-  rule
-    <make-goto-table-tasks>...
-      <make-goto-table-task>...
-        <make-goto-table-stmts> .Stmts </make-goto-table-stmts>
-      ...</make-goto-table-task>
-      => .Bag
-    ...</make-goto-table-tasks>
-  [structural]
-  rule
-    <k> make-goto-table-control(_:Ptr) => . ...</k>
-    <make-goto-table-enabled> true => false </make-goto-table-enabled>
-    <make-goto-table-tasks> .Bag </make-goto-table-tasks>
-  [structural]
-
-  rule
-    <k> make-goto-table-control(F:Ptr) ...</k>
-    <fun>...
-      <fun-id> F </fun-id>
-      <labels>... .Map => L |-> (S Ss1) @Stmts Cont ...</labels>
-    ...</fun>
-    <make-goto-table-task>
-      <make-goto-table-stmts>
-        L:Label : S:Stmt Ss1:Stmts => S Ss1
-      </make-goto-table-stmts>
-      <make-goto-table-cont>
-        Cont:Stmts
-      </make-goto-table-cont>
-    </make-goto-table-task>
-  [structural]
-
-  rule
-    <make-goto-table-tasks>...
-      <make-goto-table-task>
-        <make-goto-table-stmts>
-          (if ( _ ) S1:Stmt else S2:Stmt) Ss:Stmts => Ss
-        </make-goto-table-stmts>
-        <make-goto-table-cont> 
-          Cont:Stmts
-        </make-goto-table-cont>
-      </make-goto-table-task>
-      (.Bag =>
-        <make-goto-table-task>
-          <make-goto-table-stmts> S1 (.Stmts) </make-goto-table-stmts>
-          <make-goto-table-cont> Ss @Stmts Cont </make-goto-table-cont>
-        </make-goto-table-task>
-        <make-goto-table-task>
-          <make-goto-table-stmts> S2 (.Stmts) </make-goto-table-stmts>
-          <make-goto-table-cont> Ss @Stmts Cont </make-goto-table-cont>
-        </make-goto-table-task>
-      )
-    ...</make-goto-table-tasks>
-  [structural]
-  rule
-    <make-goto-table-tasks>...
-      <make-goto-table-task>
-        <make-goto-table-stmts>
-          while (E:Exp) S:Stmt Ss:Stmts => Ss
-        </make-goto-table-stmts>
-        <make-goto-table-cont>
-          Cont:Stmts
-        </make-goto-table-cont>
-      </make-goto-table-task>
-      (.Bag =>
-        <make-goto-table-task>
-          <make-goto-table-stmts> S (.Stmts) </make-goto-table-stmts>
-          <make-goto-table-cont>
-            (while (E) S Ss) @Stmts Cont
-          </make-goto-table-cont>
-        </make-goto-table-task>
-      )
-    ...</make-goto-table-tasks>
-  [structural]
-  rule
-    <make-goto-table-stmts>
-      { Ss1:Stmts } Ss2:Stmts => Ss1 @Stmts Ss2
-    </make-goto-table-stmts>
-  [structural]
-  rule
-    <make-goto-table-stmts>
-      KLabel:KLabel(KList:KList) Ss:Stmts => Ss
-    </make-goto-table-stmts>
-  when isStmt(KLabel:KLabel(KList:KList)) 
-    andBool KLabel =/=KLabel '_:_ 
-    andBool KLabel =/=KLabel 'if`(_`)_else_ 
-    andBool KLabel =/=KLabel 'while`(_`)_ 
-    andBool KLabel =/=KLabel '`{_`}
-  [structural]
-
   /*
    * Local variable declarations (without initializers).
    */

diff --git a/cil-semantics/cil-implementation.k b/cil-semantics/cil-implementation.k
@@ -10,6 +10,10 @@ require "cil-common.k"
 module CIL-IMPLEMENTATION
   imports CIL-COMMON
 
+  // "each enumerated type shall be compatible with char, a signed integer
+  // type, or an unsigned integer type"
+  rule enum X:CId => int [macro]
+
   /*
    * FIXME: it would be faster to treat each basic type individually, rather
    * that us byteWidthMacro

diff --git a/cil-semantics/cil-stmt.k b/cil-semantics/cil-stmt.k
@@ -13,44 +13,143 @@ module CIL-STMT
   rule
     <k> goto L:Label; ~> _ => Ss </k>
     <frame-fun-id> F:Ptr </frame-fun-id>
-    <fun>...
-      <fun-id> F </fun-id>
-      <labels>... L |-> Ss:Stmts ...</labels>
-    ...</fun>
+    <fun-id> F </fun-id>
+    <labels>... L |-> Ss:Stmts ...</labels>
   [computational]
 
-  rule <k> (. => eval-case-labels)
-    ~> goto $caseLabel(_, _) ; 
-    ...</k>
+  rule 
+    <k> (. => make-goto-table ~> eval-case-labels) ~> goto _:Label ; ...</k>
     <frame-fun-id> F:Ptr </frame-fun-id>
     <fun-id> F </fun-id>
-    <labels-evaluated> false </labels-evaluated>
+    <labels-generated> false => true </labels-generated>
   [structural]
 
   rule <k> goto $caseLabel(I:Int, V:TypedValue) ;
     => goto $defaultLabel(I) ; ...</k>
     <frame-fun-id> F:Ptr </frame-fun-id>
     <fun-id> F </fun-id>
     <labels> Lbls:Map </labels>
-    <labels-evaluated> true </labels-evaluated>
+    <labels-generated> true </labels-generated>
     when notBool ($caseLabel(I, V) in keys Lbls)
   [structural]
 
+  /*
+   * Compute the goto table (Map{Label, Stmt}). We do this at "runtime" to
+   * improve the performance of the interpreter.
+   */
+  syntax K ::= "make-goto-table"
+  rule
+    <k> make-goto-table ...</k>
+    <frame-fun-id> F:Ptr </frame-fun-id>
+    <fun-id> F </fun-id>
+    <body> { _:VarDecls { Ss:Stmts } } </body>
+    <make-goto-table-enabled> false => true </make-goto-table-enabled>
+    <make-goto-table-tasks>
+      (.Bag => 
+        <make-goto-table-task>
+          <make-goto-table-stmts> Ss </make-goto-table-stmts>
+          <make-goto-table-cont> .Stmts </make-goto-table-cont>
+        </make-goto-table-task>
+      )
+    </make-goto-table-tasks>
+  [structural]
+  rule
+    <make-goto-table-tasks>...
+      <make-goto-table-task>...
+        <make-goto-table-stmts> .Stmts </make-goto-table-stmts>
+      ...</make-goto-table-task>
+      => .Bag
+    ...</make-goto-table-tasks>
+  [structural]
+  rule
+    <k> make-goto-table => . ...</k>
+    <make-goto-table-enabled> true => false </make-goto-table-enabled>
+    <make-goto-table-tasks> .Bag </make-goto-table-tasks>
+  [structural]
+
+  rule
+    <frame-fun-id> F:Ptr </frame-fun-id>
+    <fun-id> F </fun-id>
+    <labels>... .Map => L |-> (S Ss1) @Stmts Cont ...</labels>
+    <make-goto-table-task>
+      <make-goto-table-stmts>
+        L:Label : S:Stmt Ss1:Stmts => S Ss1
+      </make-goto-table-stmts>
+      <make-goto-table-cont>
+        Cont:Stmts
+      </make-goto-table-cont>
+    </make-goto-table-task>
+  [structural]
+
+  rule
+    <make-goto-table-tasks>...
+      <make-goto-table-task>
+        <make-goto-table-stmts>
+          (if ( _ ) S1:Stmt else S2:Stmt) Ss:Stmts => Ss
+        </make-goto-table-stmts>
+        <make-goto-table-cont> 
+          Cont:Stmts
+        </make-goto-table-cont>
+      </make-goto-table-task>
+      (.Bag =>
+        <make-goto-table-task>
+          <make-goto-table-stmts> S1 (.Stmts) </make-goto-table-stmts>
+          <make-goto-table-cont> Ss @Stmts Cont </make-goto-table-cont>
+        </make-goto-table-task>
+        <make-goto-table-task>
+          <make-goto-table-stmts> S2 (.Stmts) </make-goto-table-stmts>
+          <make-goto-table-cont> Ss @Stmts Cont </make-goto-table-cont>
+        </make-goto-table-task>
+      )
+    ...</make-goto-table-tasks>
+  [structural]
+  rule
+    <make-goto-table-tasks>...
+      <make-goto-table-task>
+        <make-goto-table-stmts>
+          while (E:Exp) S:Stmt Ss:Stmts => Ss
+        </make-goto-table-stmts>
+        <make-goto-table-cont>
+          Cont:Stmts
+        </make-goto-table-cont>
+      </make-goto-table-task>
+      (.Bag =>
+        <make-goto-table-task>
+          <make-goto-table-stmts> S (.Stmts) </make-goto-table-stmts>
+          <make-goto-table-cont>
+            (while (E) S Ss) @Stmts Cont
+          </make-goto-table-cont>
+        </make-goto-table-task>
+      )
+    ...</make-goto-table-tasks>
+  [structural]
+  rule
+    <make-goto-table-stmts>
+      { Ss1:Stmts } Ss2:Stmts => Ss1 @Stmts Ss2
+    </make-goto-table-stmts>
+  [structural]
+  rule
+    <make-goto-table-stmts>
+      KLabel:KLabel(KList:KList) Ss:Stmts => Ss
+    </make-goto-table-stmts>
+  when isStmt(KLabel:KLabel(KList:KList)) 
+    andBool KLabel =/=KLabel '_:_ 
+    andBool KLabel =/=KLabel 'if`(_`)_else_ 
+    andBool KLabel =/=KLabel 'while`(_`)_ 
+    andBool KLabel =/=KLabel '`{_`}
+  [structural]
+
   // This is a somewhat hackish method for evaluating the constant expressions
   // in the case labels of switch statements. It seems to slow things down
   // quite a bit too.
   syntax K ::= "eval-case-labels"
              | "eval-case-labels" "(" Map "," Map ")"
              | "case-label-freezer" "(" Int "," Stmts ")"
-  rule <k> eval-case-labels => . ...</k>
-    <frame-fun-id> F:Ptr </frame-fun-id>
-    <fun-id> F </fun-id>
-    <labels-evaluated> true </labels-evaluated>
+
   rule <k> eval-case-labels => eval-case-labels(Lbls, .Map) ...</k>
     <frame-fun-id> F:Ptr </frame-fun-id>
     <fun-id> F </fun-id>
     <labels> Lbls:Map </labels>
-    <labels-evaluated> false </labels-evaluated>
 
   rule eval-case-labels(
     _:Map (L:Label |-> Ss:Stmts => .Map), 
@@ -70,7 +169,6 @@ module CIL-STMT
     <frame-fun-id> F:Ptr </frame-fun-id>
     <fun-id> F </fun-id>
     <labels> _ => Lbls </labels>
-    <labels-evaluated> false => true </labels-evaluated>
     [structural]
 
   syntax K ::= "$exp2bool" "(" Exp ")"    [strict]

diff --git a/cil-semantics/cil-syntax.k b/cil-semantics/cil-syntax.k
@@ -14,6 +14,7 @@ module CIL-SYNTAX
                    | "union" CId "{" VarDecls "}" ";"
                    | "struct" CId ";" // forward decls
                    | "union" CId ";"
+                   | "enum" CId ";"
 
   syntax TypedefDecl ::= "typedef" DeclSpecs Declarator ";"
 
@@ -24,6 +25,7 @@ module CIL-SYNTAX
   // It appears that CIL substitutes constants for the enum tags, but leaves
   // the declaration, so I think it can be safely elided.
   rule enum _:CId { _:EnumInits } ; => . [macro]
+  rule enum _:CId ; => . [macro]
 
   syntax Type ::= ParamDecl // TODO(chathhorn)
   // syntax Type ::= Void
@@ -386,6 +388,7 @@ module CIL-SYNTAX
   syntax AggTypeSpec ::=
       "struct" CId 
     | "union" CId 
+    | "enum" CId 
 
   // atomic-type-specifier
   //     _Atomic ( type-name )

diff --git a/cil-semantics/cil.k b/cil-semantics/cil.k
@@ -34,8 +34,8 @@ module CIL
         <formals> .Params </formals>
         <body> .K </body> // FunBody
         <labels> .Map </labels> // Map{Label, Stmt}
-        // For lazy evaluation of constant expressions in case labels.
-        <labels-evaluated> false </labels-evaluated>
+        // For lazy label generation.
+        <labels-generated> false </labels-generated>
       </fun>
     </funs>
     <global-env> .Map </global-env> // Map{CId, Ptr}