Skip to content

Instantly share code, notes, and snippets.

@bmmoore

bmmoore/diff

Last active December 26, 2015 19:19
Show Gist options
  • Save bmmoore/7201048 to your computer and use it in GitHub Desktop.
Save bmmoore/7201048 to your computer and use it in GitHub Desktop.
Download ZIP
error_kool-untyped.k
Raw
diff
diff no-error_kool-untyped.k error_kool-untyped.k
534c534
< /* */
---
>
Raw
error_kool-untyped.k
module KOOL-UNTYPED-SYNTAX
imports BUILTIN-SYNTAX-HOOKS
syntax Id ::= "Object" | "Main"
syntax Decl ::= "var" Exps ";"
| "private" "var" Exps ";" [prefer]
| "method" Id "(" Ids ")" Block
| "private" "method" Id "(" Ids ")" Block [prefer]
| "class" Id Block
| "class" Id "extends" Id Block
syntax Exp ::= Int | Bool | String | Id
| "this"
| "super"
| "(" Exp ")" [bracket]
| "++" Exp
| Exp "instanceOf" Id [strict(1)]
| "(" Id ")" Exp [strict(2)]
| "new" Id "(" Exps ")" [strict(2)]
| Exp "." Id
> Exp "[" Exps "]" [strict]
> Exp "(" Exps ")" [strict(2)]
| "-" Exp [strict]
| "sizeOf" "(" Exp ")" [strict]
| "read" "(" ")"
> left:
Exp "*" Exp [strict, left]
| Exp "/" Exp [strict, left]
| Exp "%" Exp [strict, left]
> left:
Exp "+" Exp [strict, left]
| Exp "-" Exp [strict, left]
> non-assoc:
Exp "<" Exp [strict, non-assoc]
| Exp "<=" Exp [strict, non-assoc]
| Exp ">" Exp [strict, non-assoc]
| Exp ">=" Exp [strict, non-assoc]
| Exp "==" Exp [strict, non-assoc]
| Exp "!=" Exp [strict, non-assoc]
> "!" Exp [strict]
> left:
Exp "&&" Exp [strict(1), left]
| Exp "||" Exp [strict(1), left]
> "spawn" Block
> Exp "=" Exp [strict(2), right]
syntax Ids ::= List{Id,","}
syntax Exps ::= List{Exp,","} [strict]
syntax Block ::= "{" "}"
| "{" Stmts "}"
syntax Stmt ::= Decl | Block
| Exp ";" [strict]
| "if" "(" Exp ")" Block "else" Block [avoid, strict(1)]
| "if" "(" Exp ")" Block
| "while" "(" Exp ")" Block
| "for" "(" Stmt Exp ";" Exp ")" Block
| "return" Exp ";" [strict]
| "return" ";"
| "print" "(" Exps ")" ";" [strict]
| "try" Block "catch" "(" Id ")" Block
| "throw" Exp ";" [strict]
| "join" Exp ";" [strict]
| "acquire" Exp ";" [strict]
| "release" Exp ";" [strict]
| "rendezvous" Exp ";" [strict]
syntax Stmts ::= Stmt
| Stmts Stmts [right]
rule if (E) S => if (E) S else {} [macro]
rule for(Start Cond; Step) {S} => {Start while (Cond) {S Step;}} [macro]
rule var E1:Exp, E2:Exp, Es:Exps; => var E1; var E2, Es; [macro]
rule private var E1:Exp, E2:Exp, Es:Exps; => private var E1; private var E2, Es; [macro]
rule var X:Id = E; => var X; X = E; [macro]
rule private var X:Id = E; => private var X; X = E; [macro]
rule class C:Id S => class C extends Object S
endmodule
module KOOL-UNTYPED
imports KOOL-UNTYPED-SYNTAX
configuration <T color="red">
<threads color="orange">
<thread multiplicity="*" color="yellow">
<k color="green"> ($PGM:Stmts ~> execute) </k>
<br/>
<control color="cyan">
<fstack color="blue"> .List </fstack>
<xstack color="purple"> .List </xstack>
<br/>
<crntObj color="Fuchsia"> <crntClass> Object </crntClass>
<envStack> .List </envStack>
<location multiplicity="?"> .K </location>
</crntObj>
</control>
<br/>
<env color="violet"> .Map </env>
<penv> .Map </penv>
<holds color="black"> .Map </holds>
<id color="pink"> 0 </id>
</thread>
</threads>
<br/>
<store color="white"> .Map </store>
<busy color="cyan">.Set </busy>
<terminated color="red"> .Set </terminated>
<in color="magenta" stream="stdin"> .List </in>
<out color="brown" stream="stdout"> .List </out>
<nextLoc color="gray"> 0 </nextLoc>
<br/>
<classes color="Fuchsia"> <class multiplicity="*" color="Fuchsia">
<className color="Fuchsia"> Main </className>
<extends color="Fuchsia"> Object </extends>
<declarations color="Fuchsia"> .K </declarations>
</class>
</classes>
</T>
syntax Val ::= Int | Bool | String
| array(Int,Int)
syntax Vals ::= List{Val,","}
syntax Exp ::= Val
syntax KResult ::= Val
syntax K ::= "undefined" [latex(\bot)]
/****** private variable declaration *********/
rule <k> private var X:Id; => . ...</k>
<penv> Penv => Penv[L/X] </penv>
<store> ... . => L |-> undefined ... </store>
<nextLoc> L:Int => L +Int 1 </nextLoc>
rule <k> var X:Id; => . ...</k>
<env> Env => Env[L/X] </env>
<store>... . => L |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 </nextLoc>
/****** private array declaration *********/
context private var _:Id[HOLE];
rule <k> private var X:Id[N:Int]; => . ...</k>
<penv> Penv => Penv[L/X] </penv>
<store>... . => L |-> array(L +Int 1, N)
(L +Int 1) ... (L +Int N) |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
when N >=Int 0
context var _:Id[HOLE];
rule <k> var X:Id[N:Int]; => . ...</k>
<env> Env => Env[L/X] </env>
<store>... . => L |-> array(L +Int 1, N)
(L +Int 1) ... (L +Int N) |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
when N >=Int 0
syntax Id ::= "$1" | "$2"
rule var X:Id[N1:Int, N2:Int, Vs:Vals];
=> var X[N1];
{
var $1=X;
for(var $2=0; $2 <= N1 - 1; ++$2) {
var X[N2,Vs];
$1[$2] = X;
}
}
[structural]
rule <k> X:Id => V ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
context ++(HOLE => lvalue(HOLE))
rule <k> ++loc(L) => I +Int 1 ...</k>
<store>... L |-> (I:Int => I +Int 1) ...</store> [increment]
rule I1:Int + I2:Int => I1 +Int I2
rule Str1:String + Str2:String => Str1 +String Str2
rule I1:Int - I2:Int => I1 -Int I2
rule I1:Int * I2:Int => I1 *Int I2
rule I1:Int / I2:Int => I1 /Int I2 when I2 =/=K 0
rule I1:Int % I2:Int => I1 %Int I2 when I2 =/=K 0
rule - I:Int => 0 -Int I
rule I1:Int < I2:Int => I1 <Int I2
rule I1:Int <= I2:Int => I1 <=Int I2
rule I1:Int > I2:Int => I1 >Int I2
rule I1:Int >= I2:Int => I1 >=Int I2
rule V1:Val == V2:Val => V1 ==K V2
rule V1:Val != V2:Val => V1 =/=K V2
rule ! T:Bool => notBool(T)
rule true && E => E
rule false && _ => false
rule true || _ => true
rule false || E => E
rule V:Val[N1:Int, N2:Int, Vs:Vals] => V[N1][N2, Vs]
[structural, anywhere]
rule array(L,_)[N:Int] => lookup(L +Int N)
[structural, anywhere]
rule sizeOf(array(_,N)) => N
rule <k> return(V:Val); ~> _ => V ~> K </k>
<control>
<fstack> ListItem((Env,K,C)) => . ...</fstack>
(_ => C)
</control>
<env> _ => Env </env>
syntax Val ::= "nothing"
rule return; => return nothing; [macro]
rule <k> read() => I ...</k> <in> ListItem(I:Int) => . ...</in> [read]
context (HOLE => lvalue(HOLE)) = _
rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (_ => V) ...</store>
[assignment]
rule {} => . [structural]
rule <k> { S } => S ~> env(Env) ...</k> <env> Env </env> [structural]
rule S1 S2 => S1 ~> S2 [structural]
rule _:Val; => .
rule if ( true) S else _ => S
rule if (false) _ else S => S
rule while (E) S => if (E) {S while(E)S} [structural]
rule <k> print(V:Val, Es => Es); ...</k> <out>... . => ListItem(V) </out>
[print]
rule print(.Vals); => . [structural]
syntax K ::= (Id,Stmt,K,Map,ControlCellFragment)
syntax K ::= "popx"
rule <k> (try S1 catch(X) {S2} => S1 ~> popx) ~> K </k>
<control>
<xstack> . => ListItem((X, S2, K, Env, C)) ...</xstack>
C
</control>
<env> Env </env>
rule <k> popx => . ...</k>
<xstack> _:ListItem => . ...</xstack>
rule <k> throw V:Val; ~> _ => { var X = V; S2 } ~> K </k>
<control>
<xstack> ListItem((X, S2, K, Env, C)) => . ...</xstack>
(_ => C)
</control>
<env> _ => Env </env>
rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .)
<busy> Busy => Busy -Set keys(H) </busy>
<terminated>... . => SetItem(T) ...</terminated>
rule <k> join T:Int; => . ...</k>
<terminated>... SetItem(T) ...</terminated>
rule <k> acquire V:Val; => . ...</k>
<holds>... . => V |-> 0 ...</holds>
<busy> Busy (. => SetItem(V)) </busy>
when (notBool(V in Busy:Set)) [acquire]
rule <k> acquire V; => . ...</k>
<holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
rule <k> release V:Val; => . ...</k>
<holds>... V |-> (N => N:Int -Int 1) ...</holds>
when N >Int 0
rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => . ...</holds>
<busy>... SetItem(V) => . ...</busy>
rule <k> rendezvous V:Val; => . ...</k>
<k> rendezvous V; => . ...</k> [rendezvous]
syntax Decl ::= mkDecls(Ids,Vals) [function]
rule mkDecls((X:Id, Xs:Ids), (V:Val, Vs:Vals)) => var X=V; mkDecls(Xs,Vs)
rule mkDecls(.Ids,.Vals) => {}
syntax K ::= lookup(Int)
rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [lookup]
syntax K ::= env(Map)
rule <k> env(Env) => . ...</k> <env> _ => Env </env> [structural]
rule (env(_) => .) ~> env(_) [structural]
syntax Exp ::= lvalue(K)
syntax Val ::= loc(Int)
rule <k> lvalue(X:Id => loc(L)) ...</k> <env>... X |-> L:Int ...</env>
[structural]
/****** added this *******/
rule <k> lvalue(X:Id => loc(L)) ...</k> <env> Env </env> <penv>... X |-> L:Int ...</penv>
when notBool (X in keys(Env))
[structural]
context lvalue(_[HOLE])
context lvalue(HOLE[_])
rule lvalue(lookup(L:Int) => loc(L)) [structural]
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
rule N...M |-> _ => .Map when N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M
syntax K ::= "execute"
rule <k> execute => new Main(.Exps); </k> <env> . </env> [structural]
syntax Val ::= objectClosure(CrntObjCellFragment)
| methodClosure(Id,Int,Ids,Stmt)
syntax K ::= (Map,K,ControlCellFragment)
rule <k> methodClosure(Class,OL,Xs,S)(Vs:Vals) ~> K
=> mkDecls(Xs,Vs) S return; </k>
<env> Env => . </env>
<store>... OL |-> objectClosure(<crntClass>_</crntClass> Obj)...</store>
<br/>
<control>
C
<fstack> . => ListItem((Env, K, C <crntObj> Obj' </crntObj>))
...</fstack>
<crntObj> Obj' => <crntClass> Class </crntClass> Obj </crntObj>
</control>
rule <thread>...
<k> spawn S => T ...</k>
<env> Env </env>
<crntObj> Obj </crntObj>
...</thread>
(. => <thread>...
<k> S </k>
<env> Env </env>
<id> T </id>
<crntObj> Obj </crntObj>
...</thread>)
when fresh(T:Int)
rule <k> class Class1 extends Class2 { S } => . ...</k>
<classes>... (. => <class>
<className> Class1 </className>
<extends> Class2 </extends>
<declarations> S </declarations>
</class>)
...</classes> [structural]
rule <k> method F:Id(Xs:Ids) S => . ...</k>
<crntClass> Class:Id </crntClass>
<location> OL:Int </location>
<env> Env => Env[L/F] </env>
<store>... . => L |-> methodClosure(Class,OL,Xs,S) ...</store>
<nextLoc> L => L +Int 1 </nextLoc>
/******** private method declaration **********/
/*
rule <k> private method F:Id(Xs:Ids) S => . ...</k>
<crntClass> Class:Id </crntClass>
<location> OL:Int </location>
<penv> Penv => Penv[L/F] </penv>
<store>... . => L |-> methodClosure(Class,OL,Xs,S) ...</store>
<nextLoc> L => L +Int 1 </nextLoc>
*/
syntax ListItem ::= (Id,BagItem)
rule <k> new Class:Id(Vs:Vals) ~> K
=> create(Class) ~> storeObj ~> Class(Vs); return this; </k>
<env> Env => . </env>
<nextLoc> L:Int => L +Int 1 </nextLoc>
<br/>
<control> C
<crntObj> Obj
=> <crntClass> Object </crntClass>
<envStack> (Object, <env>.Map</env>) </envStack>
<location> L </location>
</crntObj>
<fstack> . => ListItem((Env, K, C <crntObj> Obj </crntObj>)) ...</fstack>
</control>
syntax K ::= create(Id)
rule <k> create(Class:Id)
=> create(Class1) ~> setCrntClass(Class) ~> S ~> addEnvLayer ...</k>
<className> Class </className>
<extends> Class1:Id </extends>
<declarations> S </declarations> [structural]
rule <k> create(Object) => . ...</k> [structural]
syntax K ::= setCrntClass(Id)
rule <k> setCrntClass(C) => . ...</k>
<crntClass> _ => C </crntClass> [structural]
syntax K ::= "addEnvLayer"
rule <k> addEnvLayer => . ...</k>
<env> Env => . </env>
<crntClass> Class:Id </crntClass>
<envStack> . => (Class, <env>Env</env>) ...</envStack>
[structural]
syntax K ::= "storeObj"
rule <k> storeObj => . ...</k>
<crntObj> Obj (<location> L:Int </location> => .) </crntObj>
<store>... . => L |-> objectClosure(Obj) ...</store>
rule <k> this => objectClosure(Obj) ...</k>
<crntObj> Obj </crntObj>
/***** private member access ********/
/*
rule <k>X:Id => V ... </k> <env> Env:Map </env> <penv> ... X |-> L ... </penv> <store> L |-> V </store>
when notBool(X in keys(Env))
*/
rule <k> X:Id => this . X ...</k> <env> Env:Map </env> <penv> Penv:Map </penv>
when notBool(X in keys(Env)) && notBool (X in keys(Penv)) [structural]
context HOLE . _ when (HOLE =/=K super)
rule objectClosure(<crntClass> Class:Id </crntClass>
<envStack>... (Class,EnvC) EStack </envStack>)
. X:Id
=> lookupMember(<envStack> (Class,EnvC) EStack </envStack>, X)
[structural]
rule <k> super . X => lookupMember(<envStack>EStack</envStack>, X) ...</k>
<crntClass> Class </crntClass>
<envStack>... (Class,EnvC) EStack </envStack>
[structural]
rule <k> (X:Id => V)(_:Exps) ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
/***** added this ****/
rule <k> (X:Id => V)(_:Exps) ...</k>
<env> Env </env>
<penv>... X |-> L ...</penv>
<store>... L |-> V:Val ...</store>
when notBool ( X in keys(Env) ) [lookup]
/*
rule <k> (X:Id => this . X)(_:Exps) ...</k>
<env> Env </env>
when notBool(X in keys(Env)) [structural]
*/
/***** added this ****/
rule <k> (X:Id => this . X)(_:Exps) ...</k>
<env> Env </env> <penv> Penv </penv>
when notBool (X in keys(Penv)) [structural]
context HOLE._::Id(_) when HOLE =/=K super
rule (objectClosure(Obj:Bag <envStack> EStack </envStack>) . X
=> lookupMember(<envStack> EStack </envStack>, X:Id))(_:Exps) [structural]
rule <k> (super . X
=> lookupMember(<envStack>EStack</envStack>,X))(_:Exps)...</k>
<crntClass> Class </crntClass>
<envStack>... (Class,_) EStack </envStack>
[structural]
context HOLE(_:Exps)
when getKLabel HOLE ==KLabel '_`(_`) orBool getKLabel HOLE ==KLabel '_`[_`]
rule <k> (lookup(L) => V)(_:Exps) ...</k> <store>... L |-> V:Val ...</store>
[lookup]
rule objectClosure(<envStack> (C,_) ...</envStack> _)
instanceOf C => true
rule objectClosure(<envStack> (C,_) => . ...</envStack> _)
instanceOf C' when C =/=K C' [structural]
rule objectClosure(<envStack> . </envStack> _) instanceOf _ => false
rule (C) objectClosure(<crntClass> _ </crntClass> Obj)
=> objectClosure(<crntClass> C </crntClass> Obj)
rule <k> lvalue(X:Id => this . X) ...</k> <env> Env </env> <penv> Penv </penv>
when notBool(X in keys(Env)) && notBool (X in keys(Penv)) [structural]
context lvalue(HOLE . _)
rule lvalue(objectClosure(<crntClass> C </crntClass>
<envStack>... (C,EnvC) EStack </envStack>)
. X
=> lookupMember(<envStack> (C,EnvC) EStack </envStack>,
X)) [structural]
syntax K ::= lookupMember(BagItem,Id) [function]
rule lookupMember(<envStack> (_, <env>... X|->L ...</env>) ...</envStack>, X)
=> lookup(L)
rule lookupMember(<envStack> (_, <env> Env </env>) => . ...</envStack>, X)
when notBool(X in keys(Env))
endmodule
Raw
no-error_kool-untyped.k
module KOOL-UNTYPED-SYNTAX
imports BUILTIN-SYNTAX-HOOKS
syntax Id ::= "Object" | "Main"
syntax Decl ::= "var" Exps ";"
| "private" "var" Exps ";" [prefer]
| "method" Id "(" Ids ")" Block
| "private" "method" Id "(" Ids ")" Block [prefer]
| "class" Id Block
| "class" Id "extends" Id Block
syntax Exp ::= Int | Bool | String | Id
| "this"
| "super"
| "(" Exp ")" [bracket]
| "++" Exp
| Exp "instanceOf" Id [strict(1)]
| "(" Id ")" Exp [strict(2)]
| "new" Id "(" Exps ")" [strict(2)]
| Exp "." Id
> Exp "[" Exps "]" [strict]
> Exp "(" Exps ")" [strict(2)]
| "-" Exp [strict]
| "sizeOf" "(" Exp ")" [strict]
| "read" "(" ")"
> left:
Exp "*" Exp [strict, left]
| Exp "/" Exp [strict, left]
| Exp "%" Exp [strict, left]
> left:
Exp "+" Exp [strict, left]
| Exp "-" Exp [strict, left]
> non-assoc:
Exp "<" Exp [strict, non-assoc]
| Exp "<=" Exp [strict, non-assoc]
| Exp ">" Exp [strict, non-assoc]
| Exp ">=" Exp [strict, non-assoc]
| Exp "==" Exp [strict, non-assoc]
| Exp "!=" Exp [strict, non-assoc]
> "!" Exp [strict]
> left:
Exp "&&" Exp [strict(1), left]
| Exp "||" Exp [strict(1), left]
> "spawn" Block
> Exp "=" Exp [strict(2), right]
syntax Ids ::= List{Id,","}
syntax Exps ::= List{Exp,","} [strict]
syntax Block ::= "{" "}"
| "{" Stmts "}"
syntax Stmt ::= Decl | Block
| Exp ";" [strict]
| "if" "(" Exp ")" Block "else" Block [avoid, strict(1)]
| "if" "(" Exp ")" Block
| "while" "(" Exp ")" Block
| "for" "(" Stmt Exp ";" Exp ")" Block
| "return" Exp ";" [strict]
| "return" ";"
| "print" "(" Exps ")" ";" [strict]
| "try" Block "catch" "(" Id ")" Block
| "throw" Exp ";" [strict]
| "join" Exp ";" [strict]
| "acquire" Exp ";" [strict]
| "release" Exp ";" [strict]
| "rendezvous" Exp ";" [strict]
syntax Stmts ::= Stmt
| Stmts Stmts [right]
rule if (E) S => if (E) S else {} [macro]
rule for(Start Cond; Step) {S} => {Start while (Cond) {S Step;}} [macro]
rule var E1:Exp, E2:Exp, Es:Exps; => var E1; var E2, Es; [macro]
rule private var E1:Exp, E2:Exp, Es:Exps; => private var E1; private var E2, Es; [macro]
rule var X:Id = E; => var X; X = E; [macro]
rule private var X:Id = E; => private var X; X = E; [macro]
rule class C:Id S => class C extends Object S
endmodule
module KOOL-UNTYPED
imports KOOL-UNTYPED-SYNTAX
configuration <T color="red">
<threads color="orange">
<thread multiplicity="*" color="yellow">
<k color="green"> ($PGM:Stmts ~> execute) </k>
<br/>
<control color="cyan">
<fstack color="blue"> .List </fstack>
<xstack color="purple"> .List </xstack>
<br/>
<crntObj color="Fuchsia"> <crntClass> Object </crntClass>
<envStack> .List </envStack>
<location multiplicity="?"> .K </location>
</crntObj>
</control>
<br/>
<env color="violet"> .Map </env>
<penv> .Map </penv>
<holds color="black"> .Map </holds>
<id color="pink"> 0 </id>
</thread>
</threads>
<br/>
<store color="white"> .Map </store>
<busy color="cyan">.Set </busy>
<terminated color="red"> .Set </terminated>
<in color="magenta" stream="stdin"> .List </in>
<out color="brown" stream="stdout"> .List </out>
<nextLoc color="gray"> 0 </nextLoc>
<br/>
<classes color="Fuchsia"> <class multiplicity="*" color="Fuchsia">
<className color="Fuchsia"> Main </className>
<extends color="Fuchsia"> Object </extends>
<declarations color="Fuchsia"> .K </declarations>
</class>
</classes>
</T>
syntax Val ::= Int | Bool | String
| array(Int,Int)
syntax Vals ::= List{Val,","}
syntax Exp ::= Val
syntax KResult ::= Val
syntax K ::= "undefined" [latex(\bot)]
/****** private variable declaration *********/
rule <k> private var X:Id; => . ...</k>
<penv> Penv => Penv[L/X] </penv>
<store> ... . => L |-> undefined ... </store>
<nextLoc> L:Int => L +Int 1 </nextLoc>
rule <k> var X:Id; => . ...</k>
<env> Env => Env[L/X] </env>
<store>... . => L |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 </nextLoc>
/****** private array declaration *********/
context private var _:Id[HOLE];
rule <k> private var X:Id[N:Int]; => . ...</k>
<penv> Penv => Penv[L/X] </penv>
<store>... . => L |-> array(L +Int 1, N)
(L +Int 1) ... (L +Int N) |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
when N >=Int 0
context var _:Id[HOLE];
rule <k> var X:Id[N:Int]; => . ...</k>
<env> Env => Env[L/X] </env>
<store>... . => L |-> array(L +Int 1, N)
(L +Int 1) ... (L +Int N) |-> undefined ...</store>
<nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
when N >=Int 0
syntax Id ::= "$1" | "$2"
rule var X:Id[N1:Int, N2:Int, Vs:Vals];
=> var X[N1];
{
var $1=X;
for(var $2=0; $2 <= N1 - 1; ++$2) {
var X[N2,Vs];
$1[$2] = X;
}
}
[structural]
rule <k> X:Id => V ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
context ++(HOLE => lvalue(HOLE))
rule <k> ++loc(L) => I +Int 1 ...</k>
<store>... L |-> (I:Int => I +Int 1) ...</store> [increment]
rule I1:Int + I2:Int => I1 +Int I2
rule Str1:String + Str2:String => Str1 +String Str2
rule I1:Int - I2:Int => I1 -Int I2
rule I1:Int * I2:Int => I1 *Int I2
rule I1:Int / I2:Int => I1 /Int I2 when I2 =/=K 0
rule I1:Int % I2:Int => I1 %Int I2 when I2 =/=K 0
rule - I:Int => 0 -Int I
rule I1:Int < I2:Int => I1 <Int I2
rule I1:Int <= I2:Int => I1 <=Int I2
rule I1:Int > I2:Int => I1 >Int I2
rule I1:Int >= I2:Int => I1 >=Int I2
rule V1:Val == V2:Val => V1 ==K V2
rule V1:Val != V2:Val => V1 =/=K V2
rule ! T:Bool => notBool(T)
rule true && E => E
rule false && _ => false
rule true || _ => true
rule false || E => E
rule V:Val[N1:Int, N2:Int, Vs:Vals] => V[N1][N2, Vs]
[structural, anywhere]
rule array(L,_)[N:Int] => lookup(L +Int N)
[structural, anywhere]
rule sizeOf(array(_,N)) => N
rule <k> return(V:Val); ~> _ => V ~> K </k>
<control>
<fstack> ListItem((Env,K,C)) => . ...</fstack>
(_ => C)
</control>
<env> _ => Env </env>
syntax Val ::= "nothing"
rule return; => return nothing; [macro]
rule <k> read() => I ...</k> <in> ListItem(I:Int) => . ...</in> [read]
context (HOLE => lvalue(HOLE)) = _
rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (_ => V) ...</store>
[assignment]
rule {} => . [structural]
rule <k> { S } => S ~> env(Env) ...</k> <env> Env </env> [structural]
rule S1 S2 => S1 ~> S2 [structural]
rule _:Val; => .
rule if ( true) S else _ => S
rule if (false) _ else S => S
rule while (E) S => if (E) {S while(E)S} [structural]
rule <k> print(V:Val, Es => Es); ...</k> <out>... . => ListItem(V) </out>
[print]
rule print(.Vals); => . [structural]
syntax K ::= (Id,Stmt,K,Map,ControlCellFragment)
syntax K ::= "popx"
rule <k> (try S1 catch(X) {S2} => S1 ~> popx) ~> K </k>
<control>
<xstack> . => ListItem((X, S2, K, Env, C)) ...</xstack>
C
</control>
<env> Env </env>
rule <k> popx => . ...</k>
<xstack> _:ListItem => . ...</xstack>
rule <k> throw V:Val; ~> _ => { var X = V; S2 } ~> K </k>
<control>
<xstack> ListItem((X, S2, K, Env, C)) => . ...</xstack>
(_ => C)
</control>
<env> _ => Env </env>
rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .)
<busy> Busy => Busy -Set keys(H) </busy>
<terminated>... . => SetItem(T) ...</terminated>
rule <k> join T:Int; => . ...</k>
<terminated>... SetItem(T) ...</terminated>
rule <k> acquire V:Val; => . ...</k>
<holds>... . => V |-> 0 ...</holds>
<busy> Busy (. => SetItem(V)) </busy>
when (notBool(V in Busy:Set)) [acquire]
rule <k> acquire V; => . ...</k>
<holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
rule <k> release V:Val; => . ...</k>
<holds>... V |-> (N => N:Int -Int 1) ...</holds>
when N >Int 0
rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => . ...</holds>
<busy>... SetItem(V) => . ...</busy>
rule <k> rendezvous V:Val; => . ...</k>
<k> rendezvous V; => . ...</k> [rendezvous]
syntax Decl ::= mkDecls(Ids,Vals) [function]
rule mkDecls((X:Id, Xs:Ids), (V:Val, Vs:Vals)) => var X=V; mkDecls(Xs,Vs)
rule mkDecls(.Ids,.Vals) => {}
syntax K ::= lookup(Int)
rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store> [lookup]
syntax K ::= env(Map)
rule <k> env(Env) => . ...</k> <env> _ => Env </env> [structural]
rule (env(_) => .) ~> env(_) [structural]
syntax Exp ::= lvalue(K)
syntax Val ::= loc(Int)
rule <k> lvalue(X:Id => loc(L)) ...</k> <env>... X |-> L:Int ...</env>
[structural]
/****** added this *******/
rule <k> lvalue(X:Id => loc(L)) ...</k> <env> Env </env> <penv>... X |-> L:Int ...</penv>
when notBool (X in keys(Env))
[structural]
context lvalue(_[HOLE])
context lvalue(HOLE[_])
rule lvalue(lookup(L:Int) => loc(L)) [structural]
syntax Map ::= Int "..." Int "|->" K
[function, latex({#1}\ldots{#2}\mapsto{#3})]
rule N...M |-> _ => .Map when N >Int M
rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M
syntax K ::= "execute"
rule <k> execute => new Main(.Exps); </k> <env> . </env> [structural]
syntax Val ::= objectClosure(CrntObjCellFragment)
| methodClosure(Id,Int,Ids,Stmt)
syntax K ::= (Map,K,ControlCellFragment)
rule <k> methodClosure(Class,OL,Xs,S)(Vs:Vals) ~> K
=> mkDecls(Xs,Vs) S return; </k>
<env> Env => . </env>
<store>... OL |-> objectClosure(<crntClass>_</crntClass> Obj)...</store>
<br/>
<control>
C
<fstack> . => ListItem((Env, K, C <crntObj> Obj' </crntObj>))
...</fstack>
<crntObj> Obj' => <crntClass> Class </crntClass> Obj </crntObj>
</control>
rule <thread>...
<k> spawn S => T ...</k>
<env> Env </env>
<crntObj> Obj </crntObj>
...</thread>
(. => <thread>...
<k> S </k>
<env> Env </env>
<id> T </id>
<crntObj> Obj </crntObj>
...</thread>)
when fresh(T:Int)
rule <k> class Class1 extends Class2 { S } => . ...</k>
<classes>... (. => <class>
<className> Class1 </className>
<extends> Class2 </extends>
<declarations> S </declarations>
</class>)
...</classes> [structural]
rule <k> method F:Id(Xs:Ids) S => . ...</k>
<crntClass> Class:Id </crntClass>
<location> OL:Int </location>
<env> Env => Env[L/F] </env>
<store>... . => L |-> methodClosure(Class,OL,Xs,S) ...</store>
<nextLoc> L => L +Int 1 </nextLoc>
/******** private method declaration **********/
/*
rule <k> private method F:Id(Xs:Ids) S => . ...</k>
<crntClass> Class:Id </crntClass>
<location> OL:Int </location>
<penv> Penv => Penv[L/F] </penv>
<store>... . => L |-> methodClosure(Class,OL,Xs,S) ...</store>
<nextLoc> L => L +Int 1 </nextLoc>
*/
syntax ListItem ::= (Id,BagItem)
rule <k> new Class:Id(Vs:Vals) ~> K
=> create(Class) ~> storeObj ~> Class(Vs); return this; </k>
<env> Env => . </env>
<nextLoc> L:Int => L +Int 1 </nextLoc>
<br/>
<control> C
<crntObj> Obj
=> <crntClass> Object </crntClass>
<envStack> (Object, <env>.Map</env>) </envStack>
<location> L </location>
</crntObj>
<fstack> . => ListItem((Env, K, C <crntObj> Obj </crntObj>)) ...</fstack>
</control>
syntax K ::= create(Id)
rule <k> create(Class:Id)
=> create(Class1) ~> setCrntClass(Class) ~> S ~> addEnvLayer ...</k>
<className> Class </className>
<extends> Class1:Id </extends>
<declarations> S </declarations> [structural]
rule <k> create(Object) => . ...</k> [structural]
syntax K ::= setCrntClass(Id)
rule <k> setCrntClass(C) => . ...</k>
<crntClass> _ => C </crntClass> [structural]
syntax K ::= "addEnvLayer"
rule <k> addEnvLayer => . ...</k>
<env> Env => . </env>
<crntClass> Class:Id </crntClass>
<envStack> . => (Class, <env>Env</env>) ...</envStack>
[structural]
syntax K ::= "storeObj"
rule <k> storeObj => . ...</k>
<crntObj> Obj (<location> L:Int </location> => .) </crntObj>
<store>... . => L |-> objectClosure(Obj) ...</store>
rule <k> this => objectClosure(Obj) ...</k>
<crntObj> Obj </crntObj>
/***** private member access ********/
/*
rule <k>X:Id => V ... </k> <env> Env:Map </env> <penv> ... X |-> L ... </penv> <store> L |-> V </store>
when notBool(X in keys(Env))
*/
rule <k> X:Id => this . X ...</k> <env> Env:Map </env> <penv> Penv:Map </penv>
when notBool(X in keys(Env)) && notBool (X in keys(Penv)) [structural]
context HOLE . _ when (HOLE =/=K super)
rule objectClosure(<crntClass> Class:Id </crntClass>
<envStack>... (Class,EnvC) EStack </envStack>)
. X:Id
=> lookupMember(<envStack> (Class,EnvC) EStack </envStack>, X)
[structural]
rule <k> super . X => lookupMember(<envStack>EStack</envStack>, X) ...</k>
<crntClass> Class </crntClass>
<envStack>... (Class,EnvC) EStack </envStack>
[structural]
rule <k> (X:Id => V)(_:Exps) ...</k>
<env>... X |-> L ...</env>
<store>... L |-> V:Val ...</store> [lookup]
/***** added this ****/
rule <k> (X:Id => V)(_:Exps) ...</k>
<env> Env </env>
<penv>... X |-> L ...</penv>
<store>... L |-> V:Val ...</store>
when notBool ( X in keys(Env) ) [lookup]
/*
rule <k> (X:Id => this . X)(_:Exps) ...</k>
<env> Env </env>
when notBool(X in keys(Env)) [structural]
*/
/***** added this ****/
rule <k> (X:Id => this . X)(_:Exps) ...</k>
<env> Env </env> <penv> Penv </penv>
when notBool (X in keys(Penv)) [structural]
context HOLE._::Id(_) when HOLE =/=K super
rule (objectClosure(Obj:Bag <envStack> EStack </envStack>) . X
=> lookupMember(<envStack> EStack </envStack>, X:Id))(_:Exps) [structural]
rule <k> (super . X
=> lookupMember(<envStack>EStack</envStack>,X))(_:Exps)...</k>
<crntClass> Class </crntClass>
<envStack>... (Class,_) EStack </envStack>
[structural]
context HOLE(_:Exps)
when getKLabel HOLE ==KLabel '_`(_`) orBool getKLabel HOLE ==KLabel '_`[_`]
rule <k> (lookup(L) => V)(_:Exps) ...</k> <store>... L |-> V:Val ...</store>
[lookup]
rule objectClosure(<envStack> (C,_) ...</envStack> _)
instanceOf C => true
rule objectClosure(<envStack> (C,_) => . ...</envStack> _)
instanceOf C' when C =/=K C' [structural]
rule objectClosure(<envStack> . </envStack> _) instanceOf _ => false
rule (C) objectClosure(<crntClass> _ </crntClass> Obj)
=> objectClosure(<crntClass> C </crntClass> Obj)
rule <k> lvalue(X:Id => this . X) ...</k> <env> Env </env> <penv> Penv </penv>
when notBool(X in keys(Env)) && notBool (X in keys(Penv)) [structural]
context lvalue(HOLE . _)
rule lvalue(objectClosure(<crntClass> C </crntClass>
<envStack>... (C,EnvC) EStack </envStack>)
. X
=> lookupMember(<envStack> (C,EnvC) EStack </envStack>,
X)) [structural]
syntax K ::= lookupMember(BagItem,Id) [function]
rule lookupMember(<envStack> (_, <env>... X|->L ...</env>) ...</envStack>, X)
=> lookup(L)
rule lookupMember(<envStack> (_, <env> Env </env>) => . ...</envStack>, X)
when notBool(X in keys(Env))
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment