|
|
@@ -0,0 +1,158 @@ |
|
|
/* File: simp3.k */ |
|
|
|
|
|
requires "arithbool.k" |
|
|
|
|
|
module SIMP3-SYNTAX |
|
|
imports ARITHBOOL-SYNTAX |
|
|
imports ARITHBOOL-SEMANTICS |
|
|
|
|
|
/* |
|
|
ARITHBOOL-SYNTAX introduces (variable free) arithmetic and boolean |
|
|
expressions. We wish to extend it with references, which encompass |
|
|
variables, and arrays. References will be represented by identifiers |
|
|
naming locations, or nil when a location has not yet been assigned. |
|
|
These need to be values, to be the value of reference variables. |
|
|
*/ |
|
|
|
|
|
syntax Ref ::= "ref" Id |
|
|
syntax Loc ::= "nil" | Ref |
|
|
// syntax Array ::= "array" Map // Int -> Val |
|
|
syntax Val ::= Int | Loc // | Array |
|
|
|
|
|
syntax E ::= Val // Why do I need this for the rule on line 91 |
|
|
syntax KResult ::= Loc |
|
|
|
|
|
/* |
|
|
We extend our syntax with variables represented by identifiers naming |
|
|
them, repeated dereferencing, and array elements. These will be |
|
|
syntactic elements to which we may assign. They may also occur as |
|
|
expressions inside an arithmentic expression. |
|
|
*/ |
|
|
|
|
|
syntax Mutable ::= Id // Id as variable |
|
|
| Ref |
|
|
| "(" Mutable ")" [bracket] |
|
|
| "*" Mutable [strict] |
|
|
> Mutable "[" E "]" [strict(2,1)] |
|
|
|
|
|
syntax E ::= Mutable |
|
|
|
|
|
/* |
|
|
Our syntax for commands needs to be expanded to allow assignment to |
|
|
mutable terms, not just identifiers. We will also incorporate the |
|
|
alias command from simp2.k. |
|
|
*/ |
|
|
|
|
|
syntax CFinal ::= "skip" |
|
|
|
|
|
syntax C ::= CFinal |
|
|
| C ";" C [right, strict(1)] |
|
|
| "alias" Id "=" Id |
|
|
| Mutable ":=" E [strict(2)] |
|
|
| "if" B "then" C "else" C "fi" [strict(1)] |
|
|
| "{" C "}" |
|
|
| "while" B "do" C "od" |
|
|
|
|
|
|
|
|
/* |
|
|
S is the syntactic catogory of "syntax", allowing us to incrementally |
|
|
test each new construct. It already contains E and B. |
|
|
*/ |
|
|
|
|
|
syntax S ::= C |
|
|
|
|
|
|
|
|
syntax KResult ::= CFinal |
|
|
|
|
|
syntax LVal ::= Ref | "lvalue" Mutable | "(" LVal ")" [bracket] |
|
|
| "forcervalue" Mutable // so that we can cause assignment to also allocate |
|
|
| "star" LVal [strict] |
|
|
syntax Cint ::= C | "assign" LVal Val [strict(1)] |
|
|
syntax MutCalc ::= Mutable |
|
|
|
|
|
endmodule |
|
|
|
|
|
module SIMP3 |
|
|
imports SIMP3-SYNTAX |
|
|
imports ARITHBOOL-SEMANTICS |
|
|
|
|
|
configuration |
|
|
<T> |
|
|
<k> $PGM:S </k> |
|
|
<loc> .Map </loc> |
|
|
<mem> .Map </mem> |
|
|
</T> |
|
|
|
|
|
rule skip ; C2 => C2 |
|
|
rule if true then C1 else C2 fi => C1 |
|
|
rule if false then C1 else C2 fi => C2 |
|
|
rule {C} => C [structrual] |
|
|
rule while B do C od => if B then {C ; while B do C od} else skip fi |
|
|
rule M := (V:Val) => assign (lvalue M) V |
|
|
|
|
|
rule <k> I:Id => V ... </k> |
|
|
<loc> ... (I |-> L) ... </loc> |
|
|
<mem> ... (L |-> V) ... </mem> |
|
|
|
|
|
rule <k> (* (ref (L:Id))) => V ...</k> |
|
|
<mem> ... (L |-> V) ...</mem> |
|
|
|
|
|
/* |
|
|
// Use this if you can't alias a declared variable |
|
|
rule <k> alias I1:Id = I2:Id => skip ... </k> |
|
|
<loc>Loc:Map (.Map => I1 |-> Loc[I2]) </loc> |
|
|
requires (notBool(I1 in keys(Loc))) |
|
|
*/ |
|
|
|
|
|
// Use this if we are allowing aliasing already declared variables. |
|
|
rule <k> alias I1:Id = I2:Id => skip ... </k> |
|
|
<loc> Loc => Loc[ I1 <- Loc[I2] ] </loc> |
|
|
|
|
|
rule <k> assign (ref (L)) V => skip ... </k> |
|
|
<mem> Mem:Map => Mem[L <- V] </mem> |
|
|
|
|
|
rule <k> lvalue Id => ref(L) ...</k> |
|
|
<loc> ... (Id|-> L) ... </loc> |
|
|
|
|
|
/* |
|
|
Use if we want assigning to a variable to allocate space for it even |
|
|
if it hasn't been previously declared. |
|
|
*/ |
|
|
rule <k> lvalue (Id:Id) => ref(!L) ...</k> |
|
|
<loc> Loc:Map (.Map => Id |-> !L) </loc> |
|
|
requires (notBool(Id in keys(Loc))) |
|
|
|
|
|
rule lvalue (ref(L)) => ref(L) |
|
|
|
|
|
// rule lvalue (* M) => M |
|
|
|
|
|
rule lvalue (* M) => forcervalue M // This must be a ref |
|
|
|
|
|
rule <k> forcervalue (Id:Id) => ref L2 ... </k> |
|
|
<loc> ... Id |-> L1 ...</loc> |
|
|
<mem> ... L1 |-> ref L2 ... </mem> |
|
|
|
|
|
rule <k> forcervalue (Id:Id) => ref !L2 ... </k> |
|
|
<loc> ... Id |-> L1 ...</loc> |
|
|
<mem> Mem:Map(.Map => L1 |-> ref !L2) </mem> |
|
|
|
|
|
rule <k> forcervalue (Id:Id) => ref (!L2:Id) ... </k> |
|
|
<loc> Loc:Map (.Map => Id |-> (!L1:Id)) </loc> |
|
|
<mem> Mem:Map (.Map => !L1 |-> ref !L2) </mem> |
|
|
requires (notBool(Id in keys(Loc))) |
|
|
|
|
|
// forcervalue of an Int is an error |
|
|
|
|
|
rule forcervalue (ref L) => ref L |
|
|
|
|
|
rule forcervalue (* M) => star (forcervalue M) |
|
|
|
|
|
|
|
|
rule <k> star (ref L1) => ref L2 ... </k> |
|
|
<mem> ... L1 |-> ref L2 ... </mem> |
|
|
|
|
|
rule <k> star (ref L1) => ref !L2 ... </k> |
|
|
<mem> Mem:Map (.Map => L1 |-> ref !L2) </mem> |
|
|
requires notBool(L1 in keys(Mem)) |
|
|
|
|
|
endmodule |
chrisshroba created this gist