forked from runtimeverification/python-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpython-semantics-attribute-ref.k
More file actions
125 lines (102 loc) · 7.39 KB
/
Copy pathpython-semantics-attribute-ref.k
File metadata and controls
125 lines (102 loc) · 7.39 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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
require "python-semantics-common.k"
module PYTHON-SEMANTICS-ATTRIBUTE-REF
imports PYTHON-SEMANTICS-COMMON
syntax ObjRef ::= mapLookup(Expression, Expression) [strict]
| mapInsert(Expression, Expression, Expression) [strict]
| basesLookup(Expression, Expression) [strict]
| basesLookup(List, Expression) [strict(2), klabel('basesLookup2)]
| descriptor(Expression, Expression, Expression, Test) [strict]
| checkData(Expression, Expression) [strict]
| checkDataSet(Expression, Expression, Expression) [strict]
rule [attribute]: O:Object . X:Id => ref("getattr")(O, Id2String(X), .Arguments)
rule invokeBuiltin("getattr", _) => try:
(try:
return getmember(String2Id("object"), "__getattribute__", true, false, true)(String2Id("name"))
except ref("AttributeError") :
(if hasmember(String2Id("object"), "__getattr__") :
return getmember(String2Id("object"), "__getattr__", true, false, true) (String2Id("name"))
else:
raise))
except ref("AttributeError") :
(if String2Id("default") ==Obj .Obj :
raise
else:
return String2Id("default"))
//rule invokeBuiltin(obj("hasattr",_), ListItem(O) ListItem(S), .) => try: (ref("getattr")(O, S, .Arguments) ; ~> ref("True")) except ref("AttributeError") : ref("False") else: pass
rule invokeBuiltin("object.__getattribute__",_) => (if hasmember(String2Id("self"), String2Id("name")) :
String2Id("data"), .Expressions := getmember(String2Id("self"), String2Id("name"), false, false, true) newline
(if hasmember(String2Id("data"), "__set__") or hasmember(String2Id("data"), "__delete__") :
return descriptor(String2Id("data"), String2Id("self"), gettype(String2Id("self")), false)
else: pass)
else: pass) newline
String2Id("val"), .Expressions := mapLookup(String2Id("self"), String2Id("name")) newline
(if String2Id("val") =/=Obj .Obj :
return String2Id("val")
else: pass) newline
return getmember(String2Id("self"), String2Id("name"), true, false, true)
rule invokeBuiltin("type.__getattribute__",_) => (if hasmember(String2Id("self"), String2Id("name")) :
String2Id("data"), .Expressions := getmember(String2Id("self"), String2Id("name"), false, false, true) newline
(if hasmember(String2Id("data"), "__set__") or hasmember(String2Id("data"), "__delete__") :
return descriptor(String2Id("data"), String2Id("self"), gettype(String2Id("self")), false)
else: pass)
else: pass) newline
return getmember(String2Id("self"), String2Id("name"), true, true, true)
syntax Test ::= checkMember(Expression) [strict]
rule hasmember(O:Object, O2:Object) => checkMember(getmember(O, O2, false, false, false)) -> false
rule checkMember(.Obj) => .Obj
rule checkMember(O:Object) => true
rule getmember(O:Object, O2:Object, T:Bool, T2:Bool, true) => getmember(O, O2, T, T2, false) -> raiseInternal("AttributeError", "object has no attribute '" +String strvalue(O2) +String "'")
rule getmember(O:Object, O2:Object, true, false, false) => descriptor(getmember(O, O2, false, false, false), O, gettype(O), false)
rule getmember(O:Object, O2:Object, false, true, false) => basesLookup(getref(O, "__mro__"), O2) -> getmember(O, O2, false, false, false)
rule getmember(O:Object, O2:Object, true, true, false) => descriptor(basesLookup(getref(O, "__mro__"), O2), O, gettype(O), true) -> getmember(O, O2, true, false, false)
rule getmember(O:Object, O2:Object, false, false, false) => basesLookup(getref2(gettype(O), "__mro__"), O2)
rule <k> mapLookup(obj(B,_), O) => try: K[O] except ref("KeyError") : .Obj else: pass ...</k>
<object>
<id>B</id>
<oattrs>... "__dict__" |-> K ...</oattrs>
</object>
rule <k> mapLookup(obj(B,_), O:Object) => .Obj ...</k>
<object>
<id>B</id>
<oattrs>Attrs:Map</oattrs>
</object> when notBool("__dict__" in keys(Attrs))
rule <k> mapLookup(obj(B,_), O:Object) => K ...</k>
<object>...
<id>B</id>
<oenv>... S |-> K ...</oenv>
...</object> when S ==String strvalue(O)
rule <k> mapLookup(obj(B,_), O:Object) => .Obj ...</k>
<object>...
<id>B</id>
<oenv> Env:Map </oenv>
...</object> when notBool(strvalue(O) in keys(Env))
rule basesLookup(O:Object, O2:Object) => basesLookup(listvalue(O), O2)
rule basesLookup(ListItem(B) L:List, O) => mapLookup(B, O) -> basesLookup(L, O)
rule basesLookup(., _) => .Obj
rule descriptor(.Obj,_,_,_) => .Obj
//TODO: add super
rule descriptor(O:Object, O2:Object, _, true) => (getmember(O, "__get__", false, false, false) ( O , ref("None") , O2, .Arguments)) -> O
rule <k> descriptor(O:Object, O2:Object, Type:Object, false) => (getmember(O, "__get__", false, false, false) ( O , O2 , Type, .Arguments )) -> O ...</k>
<symbols>... "None" |-> NoneId ...</symbols> when id(O2) =/=K NoneId
rule <k> descriptor(O:Object, O2:Object, Type:Object, false) => (getmember(O, "__get__", false, false, false) (O, O2, O2, .Arguments)) -> O ...</k>
<symbols>... "None" |-> NoneId ...</symbols> when id(O2) ==K NoneId
rule setmember(O:Object, Name:Object, Value:Object) => checkDataSet(getmember(O, Name, false, false, false), O, Value) -> mapInsert(O, Name, Value) -> raiseInternal("AttributeError", "object has no attribute '" +String strvalue(Name) +String "'")
rule checkDataSet(O:Object, Instance, Value) => getmember(O, "__set__", false, false, false) (O, Instance, Value, .Arguments) -> .Obj
rule checkDataSet(.Obj, _, _) => .Obj
rule <k> mapInsert(obj(B,_), Name, Value) => Dict [Name] , .Expressions := Value ~> ref("None") ...</k>
<object>
<id> B </id>
<oattrs>... "__dict__" |-> Dict ...</oattrs>
</object>
rule <k> mapInsert(obj(B,_), _, _) => .Obj ...</k>
<object>...
<id> B </id>
<oattrs> Env:Map </oattrs>
...</object> when notBool("__dict__" in keys(Env))
rule <k> mapInsert(obj(B,_), _, _) => raiseInternal("TypeError", "can't set attributes of built-in/extension type") ...</k>
<object>...
<id> B </id>
<oattrs>... "__dict__" |-> _ ...</oattrs>
<oenv> _ </oenv>
...</object>
endmodule