Skip to content

Instantly share code, notes, and snippets.

@chrisshroba chrisshroba/-
Created Oct 27, 2016

Embed
What would you like to do?
/* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.