Lazy evaluation of constants in case labels in an attempt to improve …

…performance slightly.
kframework · Aug 19, 2013 · 7327ce3 · 7327ce3
1 parent 28cb7da
commit 7327ce3
Show file tree

Hide file tree

Showing 4 changed files with 52 additions and 29 deletions.
diff --git a/cil-semantics/cil-decl.k b/cil-semantics/cil-decl.k
@@ -113,7 +113,6 @@ module CIL-DECL
       defineFun(F:Ptr, T:Type, Ps:Params, FB:FunBody)
     => lower-break-continue-to-goto-control(F) 
       ~> make-goto-table-control(F)
-      ~> eval-case-labels(F)
       //~> propagate-constants(F)
     ...</k>
     // <frame-fun-id> _ => F </frame-fun-id>
@@ -125,37 +124,10 @@ module CIL-DECL
         <fun-type> T </fun-type>
         <formals> Ps </formals>
         <body> FB </body>
-        <labels> .Map </labels>
-      </fun>
+      ...</fun>
     ...</funs>
   [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" "(" Ptr ")"
-             | "eval-case-labels'" "(" Ptr "," Map "," Map ")"
-             | "case-label-freezer" "(" Int "," Stmts ")"
-  rule <k> eval-case-labels(F:Ptr) 
-    => eval-case-labels'(F, Lbls, .Map) ...</k>
-    <fun-id> F </fun-id>
-    <labels> Lbls:Map </labels>
-
-  rule eval-case-labels'(_, 
-    _:Map (L:Label |-> Ss:Stmts => .Map), 
-    _:Map (.Map => L |-> Ss)) 
-    when getKLabel(L) =/=KLabel '$caseLabel
-  rule (. => E ~> case-label-freezer(I, Ss)) 
-    ~> eval-case-labels'(_, 
-    _:Map ($caseLabel(I:Int, E:Exp) |-> Ss:Stmts => .Map), _:Map) 
-  rule (E:KResult ~> case-label-freezer(I:Int, Ss:Stmts) => .)
-    ~> eval-case-labels'(_, 
-    _:Map, _:Map (.Map => $caseLabel(I, E) |-> Ss))
-
-  rule <k> eval-case-labels'(F:Ptr, .Map, Lbls:Map) => . ...</k>
-    <fun-id> F </fun-id>
-    <labels> _ => Lbls </labels>
-
   /*
    * Function declarations (without initializers).
    */

diff --git a/cil-semantics/cil-exp.k b/cil-semantics/cil-exp.k
@@ -60,7 +60,10 @@ module CIL-LITERAL
       andBool (S =/=String "")
   rule getNumericPart'(S:String, Num:String) => Num
     when isSuffixChar(carStr(S))
+      andBool (Num =/=String "")
   rule getNumericPart'("", Num:String) => Num
+    when Num =/=String ""
+  rule getNumericPart'("", "") => "0"
 
   syntax String ::= getSuffix(String) [function]
 

diff --git a/cil-semantics/cil-stmt.k b/cil-semantics/cil-stmt.k
@@ -19,14 +19,60 @@ module CIL-STMT
     ...</fun>
   [computational]
 
+  rule <k> (. => eval-case-labels)
+    ~> goto $caseLabel(_, _) ; 
+    ...</k>
+    <frame-fun-id> F:Ptr </frame-fun-id>
+    <fun-id> F </fun-id>
+    <labels-evaluated> false </labels-evaluated>
+  [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>
     when notBool ($caseLabel(I, V) in keys Lbls)
   [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), 
+    _:Map (.Map => L |-> Ss)) 
+    when getKLabel(L) =/=KLabel '$caseLabel
+    [structural]
+  rule (. => E ~> case-label-freezer(I, Ss)) 
+    ~> eval-case-labels(
+      _:Map ($caseLabel(I:Int, E:Exp) |-> Ss:Stmts => .Map), _:Map) 
+    [structural]
+  rule (E:KResult ~> case-label-freezer(I:Int, Ss:Stmts) => .)
+    ~> eval-case-labels(
+      _:Map, _:Map (.Map => $caseLabel(I, E) |-> Ss))
+    [structural]
+
+  rule <k> eval-case-labels(.Map, Lbls:Map) => . ...</k>
+    <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]
   rule if (E:Exp) S1:Stmt else S2:Stmt
     => $exp2bool(E) ~> if (HOLE) S1 else S2

diff --git a/cil-semantics/cil.k b/cil-semantics/cil.k
@@ -34,6 +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>
       </fun>
     </funs>
     <global-env> .Map </global-env> // Map{CId, Ptr}