-
Notifications
You must be signed in to change notification settings - Fork 4
Expand file tree
/
Copy pathpython-semantics-generator.k
More file actions
99 lines (84 loc) · 6.81 KB
/
Copy pathpython-semantics-generator.k
File metadata and controls
99 lines (84 loc) · 6.81 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
require "python-semantics-calls.k"
module PYTHON-SEMANTICS-GENERATOR
imports PYTHON-SEMANTICS-CALLS
rule [invoke-generator-function]: <k> invoke(obj(_:Int,<oattrs>... "__closure__" |-> Closure "__code__" |-> ref(Code) "__globals__" |-> Globals ...</oattrs>), M) ~> K:K => makeFrame(N, ref(Code), ref("None"), makeLocals(ref(Code) . String2Id("co_freevars"), Closure), Globals, Globals["__builtins__"], makeCells(ref(Code) . String2Id("co_freevars"), ref(Code) . String2Id("co_cellvars"), Closure, N), M) ~> mutable("gi_code" |-> ref(Code) "gi_frame" |-> ref(N) "gi_running" |-> ref("False") "gi_state" |-> .K, ref("generator")) ...</k>
<nextLoc> N => N +Int 1 </nextLoc>
<object>...
<id>Code</id>
<oattrs>... "co_flags" |-> Flags ...</oattrs>
...</object> when Flags &Int 32 =/=Int 0 [allocation]
rule invokeBuiltin(obj("iter_generator",_), ListItem(O), .) => O
rule invokeBuiltin(obj("next_generator",_), ListItem(O), .) => runGenerator(ref(id(O)), ref("None"))
rule invokeBuiltin(obj("send_generator",_), ListItem(O) ListItem(O2), .) => runGenerator(ref(id(O)), O2)
rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type), .) => ref("throw_generator")(O, Type, ref("None"), ref("None"))
rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value), .) => ref("throw_generator")(O, Type, Value, ref("None"))
rule invokeBuiltin(obj("throw_generator",_), ListItem(O) ListItem(Type) ListItem(Value) ListItem(Traceback), .) => test(or(istype(Traceback, ref("NoneType")), istype(Traceback, ref("traceback"))), test(or(istype(Type, ref("BaseException")), hasbase(Type, ref("BaseException"))), test(and(istype(Type, ref("BaseException")), negate(istype(Value, ref("NoneType")))), raiseInternal("TypeError", "instance exception may not have a separate value"), createRaiseStatement(O, Type, .Obj if Value is ref("None") else Value, .Obj if Traceback is ref("None") else Traceback)), raiseInternal("TypeError", "exceptions must be classes or instances deriving from BaseException")), raiseInternal("TypeError", "throw() third argument must be a traceback object"))
syntax ObjRef ::= createRaiseStatement(Exp, Exp, Exp, Exp) [strict]
rule createRaiseStatement(O, Type, .Obj, .Obj) => throwGenerator(ref(id(O)), test(istype(Type, ref("BaseException")), Type, Type(.Arguments)))
rule createRaiseStatement(O, Type, Value:Object, .Obj) => throwGenerator(ref(id(O)), Type(Value))
rule createRaiseStatement(O, Type, .Obj, Traceback:Object) => test(istype(Type, ref("BaseException")), throwGenerator(ref(id(O)), Type . String2Id("with_traceback")(Traceback)), throwGenerator(ref(id(O)), Type(.Arguments) . String2Id("with_traceback")(Traceback)))
rule createRaiseStatement(O, Type, Value:Object, Traceback:Object) => throwGenerator(ref(id(O)), Type(Value) . String2Id("with_traceback")(Traceback))
rule invokeBuiltin(obj("close_generator",_), ListItem(O), .) => try: throwGenerator(ref(id(O)), ref("GeneratorExit")) ; except ref("GeneratorExit") : ref("None") except ref("StopIteration") : ref("None") else: raiseInternal("RuntimeError", "generator ignored GeneratorExit")
syntax ObjRef ::= runGenerator(Exp, Exp) [seqstrict(2, 1)]
| throwGenerator(Exp, Exp) [seqstrict(2, 1)]
| enterGenerator(Exp, K, K)
rule runGenerator(O:Object, Arg:Object) => if Arg is not ref("None") : raiseInternal("TypeError", "can't send non-None value to just-started generator") else: enterGenerator(O, .K, .K) when getattr(O, "gi_state") ==K .K
rule throwGenerator(O:Object, Ex:Object) => enterGenerator(O, raise Ex, getattr(O, "gi_state"))
rule runGenerator(O:Object, Arg:Object) => enterGenerator(O, Arg, getattr(O, "gi_state")) when getattr(O, "gi_state") =/=K .K
syntax K ::= beginRunningGenerator(Object)
rule beginRunningGenerator(O) => if getref(O, "gi_running"): raiseInternal("ValueError", "generator already executing") ~> setref(id(O), "gi_running", ref("True"))
rule [start-generator]: <k> enterGenerator(O, Val, .K) ~> K => beginRunningGenerator(O) ~> Val ~> getattr2(getref(O, "gi_code"), "co_code") ~> return </k>
<control>...
<currentFrame>
<frameObject> Frame => id(getattr(O, "gi_frame")) </frameObject>
<fstack> FL => . </fstack>
<xcontext> XC </xcontext>
(C:Bag => <xstack> .List </xstack> <lstack> .List </lstack>)
</currentFrame>
<cstack> . => ListItem(generator(Frame, C, FL, XC, K, ref(id(O)))) ...</cstack>
...</control>
syntax K ::= (K, CurrentFrameCellFragment, List, K)
rule [continue-generator]: <k> enterGenerator(O, Val, (RestoredK, RestoredC, RestoredFL, RestoredXC)) ~> K => beginRunningGenerator(O) ~> Val ~> RestoredK ~> return </k>
<control>...
<currentFrame>
<frameObject> Frame => id(getattr(O, "gi_frame")) </frameObject>
<fstack> FL => RestoredFL </fstack>
<xcontext> XC => RestoredXC </xcontext>
(C:Bag => RestoredC)
</currentFrame>
<cstack> . => ListItem(generator(Frame, C, FL, XC, K, ref(id(O)))) ...</cstack>
...</control>
syntax Arguments ::= "#if" Bool "#then" Arguments "#else" Arguments "#fi" [function]
rule <k> return O:Object ~> _ => setref(N, "gi_running", ref("False")) ~> setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), SavedC, .List, SavedXC)) ~> raise ref("StopIteration")(#if id(O) ==K NoneId #then .Arguments #else O #fi) ~> K </k>
<control>...
<cstack> ListItem(generator(Frame, C, FL, XC, K, ref(N))) => . ...</cstack>
<currentFrame>
<frameObject> _ => Frame </frameObject>
<fstack> . => FL </fstack>
<xcontext> SavedXC => XC </xcontext>
(SavedC => C)
</currentFrame>
...</control>
<symbols>... "None" |-> NoneId ...</symbols>
rule [yield]: <k> yield O ~> SavedK => setref(N, "gi_running", ref("False")) ~> setattr(N, "gi_state", (SavedK, SavedC, SavedFL, SavedXC)) ~> O ~> K </k>
<control>...
<cstack> ListItem(generator(Frame, C, FL, XC, K, ref(N))) => . ...</cstack>
<currentFrame>
<frameObject> _ => Frame </frameObject>
<fstack> SavedFL => FL </fstack>
<xcontext> SavedXC => XC </xcontext>
(SavedC => C)
</currentFrame>
</control>
rule [raise-out-of-generator]: <k> (. => setref(N, "gi_running", ref("False")) ~> setattr(N, "gi_state", (#freezer (HOLE ;)(.KList), <xstack> . </xstack> SavedC, .List, ref("None")))) ~> raise ...</k>
<control>...
<cstack> ListItem(generator(Frame, C, FL, _, _, ref(N))) => . ...</cstack>
<currentFrame>
(<xstack> . </xstack>
SavedC => C)
<frameObject> _ => Frame </frameObject>
<fstack> . => FL </fstack>
<xcontext> SavedXC </xcontext>
</currentFrame>
...</control>
endmodule