diff --git a/cil-semantics/cil-decl.k b/cil-semantics/cil-decl.k index 4e9b9b89c..8f88d59a7 100644 --- a/cil-semantics/cil-decl.k +++ b/cil-semantics/cil-decl.k @@ -112,10 +112,8 @@ module CIL-DECL defineFun(F:Ptr, T:Type, Ps:Params, FB:FunBody) => lower-break-continue-to-goto-control(F) - ~> make-goto-table-control(F) //~> propagate-constants(F) ... - // _ => F ... .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 - make-goto-table-control(F:Ptr) ... - ... - F - { _:VarDecls { Ss:Stmts } } - ... - - false => true - - (.Bag => - - Ss - .Stmts - - ) - - - [structural] - rule - ... - ... - .Stmts - ... - => .Bag - ... - [structural] - rule - make-goto-table-control(_:Ptr) => . ... - true => false - .Bag - [structural] - - rule - make-goto-table-control(F:Ptr) ... - ... - F - ... .Map => L |-> (S Ss1) @Stmts Cont ... - ... - - - L:Label : S:Stmt Ss1:Stmts => S Ss1 - - - Cont:Stmts - - - [structural] - - rule - ... - - - (if ( _ ) S1:Stmt else S2:Stmt) Ss:Stmts => Ss - - - Cont:Stmts - - - (.Bag => - - S1 (.Stmts) - Ss @Stmts Cont - - - S2 (.Stmts) - Ss @Stmts Cont - - ) - ... - [structural] - rule - ... - - - while (E:Exp) S:Stmt Ss:Stmts => Ss - - - Cont:Stmts - - - (.Bag => - - S (.Stmts) - - (while (E) S Ss) @Stmts Cont - - - ) - ... - [structural] - rule - - { Ss1:Stmts } Ss2:Stmts => Ss1 @Stmts Ss2 - - [structural] - rule - - KLabel:KLabel(KList:KList) Ss:Stmts => Ss - - 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 index f0555034f..9c432c701 100644 --- 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 index d66a43973..0d1f8806f 100644 --- a/cil-semantics/cil-stmt.k +++ b/cil-semantics/cil-stmt.k @@ -13,18 +13,15 @@ module CIL-STMT rule goto L:Label; ~> _ => Ss F:Ptr - ... - F - ... L |-> Ss:Stmts ... - ... + F + ... L |-> Ss:Stmts ... [computational] - rule (. => eval-case-labels) - ~> goto $caseLabel(_, _) ; - ... + rule + (. => make-goto-table ~> eval-case-labels) ~> goto _:Label ; ... F:Ptr F - false + false => true [structural] rule goto $caseLabel(I:Int, V:TypedValue) ; @@ -32,25 +29,127 @@ module CIL-STMT F:Ptr F Lbls:Map - true + true 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 + make-goto-table ... + F:Ptr + F + { _:VarDecls { Ss:Stmts } } + false => true + + (.Bag => + + Ss + .Stmts + + ) + + [structural] + rule + ... + ... + .Stmts + ... + => .Bag + ... + [structural] + rule + make-goto-table => . ... + true => false + .Bag + [structural] + + rule + F:Ptr + F + ... .Map => L |-> (S Ss1) @Stmts Cont ... + + + L:Label : S:Stmt Ss1:Stmts => S Ss1 + + + Cont:Stmts + + + [structural] + + rule + ... + + + (if ( _ ) S1:Stmt else S2:Stmt) Ss:Stmts => Ss + + + Cont:Stmts + + + (.Bag => + + S1 (.Stmts) + Ss @Stmts Cont + + + S2 (.Stmts) + Ss @Stmts Cont + + ) + ... + [structural] + rule + ... + + + while (E:Exp) S:Stmt Ss:Stmts => Ss + + + Cont:Stmts + + + (.Bag => + + S (.Stmts) + + (while (E) S Ss) @Stmts Cont + + + ) + ... + [structural] + rule + + { Ss1:Stmts } Ss2:Stmts => Ss1 @Stmts Ss2 + + [structural] + rule + + KLabel:KLabel(KList:KList) Ss:Stmts => Ss + + 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 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), @@ -70,7 +169,6 @@ module CIL-STMT F:Ptr F _ => Lbls - false => true [structural] syntax K ::= "$exp2bool" "(" Exp ")" [strict] diff --git a/cil-semantics/cil-syntax.k b/cil-semantics/cil-syntax.k index 3301e3c06..cf2f88dad 100644 --- 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 index 96cce3f4e..3a7c24d93 100644 --- a/cil-semantics/cil.k +++ b/cil-semantics/cil.k @@ -34,8 +34,8 @@ module CIL .Params .K // FunBody .Map // Map{Label, Stmt} - // For lazy evaluation of constant expressions in case labels. - false + // For lazy label generation. + false .Map // Map{CId, Ptr}