From 7327ce3b713e9e6cac8e7fe94988699bc6c32d0f Mon Sep 17 00:00:00 2001 From: chathhorn Date: Mon, 19 Aug 2013 17:32:09 -0500 Subject: [PATCH] Lazy evaluation of constants in case labels in an attempt to improve performance slightly. --- cil-semantics/cil-decl.k | 30 +------------------------- cil-semantics/cil-exp.k | 3 +++ cil-semantics/cil-stmt.k | 46 ++++++++++++++++++++++++++++++++++++++++ cil-semantics/cil.k | 2 ++ 4 files changed, 52 insertions(+), 29 deletions(-) diff --git a/cil-semantics/cil-decl.k b/cil-semantics/cil-decl.k index 30665b019..4e9b9b89c 100644 --- 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) ... // _ => F @@ -125,37 +124,10 @@ module CIL-DECL T Ps FB - .Map - + ... ... [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 eval-case-labels(F:Ptr) - => eval-case-labels'(F, Lbls, .Map) ... - F - Lbls:Map - - 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 eval-case-labels'(F:Ptr, .Map, Lbls:Map) => . ... - F - _ => Lbls - /* * Function declarations (without initializers). */ diff --git a/cil-semantics/cil-exp.k b/cil-semantics/cil-exp.k index 64563dc91..21cac0a6b 100644 --- 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 index 0998c0e8a..d66a43973 100644 --- a/cil-semantics/cil-stmt.k +++ b/cil-semantics/cil-stmt.k @@ -19,14 +19,60 @@ module CIL-STMT ... [computational] + rule (. => eval-case-labels) + ~> goto $caseLabel(_, _) ; + ... + F:Ptr + F + false + [structural] + rule goto $caseLabel(I:Int, V:TypedValue) ; => goto $defaultLabel(I) ; ... F:Ptr F Lbls:Map + true 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 eval-case-labels => . ... + F:Ptr + F + true + rule eval-case-labels => eval-case-labels(Lbls, .Map) ... + F:Ptr + F + Lbls:Map + false + + 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 eval-case-labels(.Map, Lbls:Map) => . ... + F:Ptr + F + _ => Lbls + false => true + [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 index becf6972e..96cce3f4e 100644 --- a/cil-semantics/cil.k +++ b/cil-semantics/cil.k @@ -34,6 +34,8 @@ module CIL .Params .K // FunBody .Map // Map{Label, Stmt} + // For lazy evaluation of constant expressions in case labels. + false .Map // Map{CId, Ptr}