-
Notifications
You must be signed in to change notification settings - Fork 0
/
PrimOp-STM.dl
139 lines (129 loc) · 4.4 KB
/
PrimOp-STM.dl
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
/*
HINT: is interpreted -/+
primop effectful
+ "atomically#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}
- "retry#" :: {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}
+ "catchRetry#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}
+ "catchSTM#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> (%b -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}
+ "newTVar#" :: %a -> {"State#" %s} -> {"GHC.Prim.Unit#" {"TVar#" %s %a}}
+ "readTVar#" :: {"TVar#" %s %a} -> {"State#" %s} -> {"GHC.Prim.Unit#" %a}
+ "readTVarIO#" :: {"TVar#" %s %a} -> {"State#" %s} -> {"GHC.Prim.Unit#" %a}
+ "writeTVar#" :: {"TVar#" %s %a} -> %a -> {"State#" %s} -> {"GHC.Prim.(##)"}
primop pure
- "sameTVar#" :: {"TVar#" %s %a} -> {"TVar#" %s %a} -> T_Int64
*/
.decl TVar(ext_result:Variable, ty_node:Variable, item:Variable)
.output TVar
// "atomically#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}) -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a}
USED("PrimOp-STM-01")
RaisedEx("Control.Exception.Base.nestedAtomically"), // hardwired closure for GHC RTS
//Called(r, op),
CallPNode1("atomically#", r, v0, v1_state) :-
op = "atomically#",
Call(r, op, _),
// pass argument to the wrapped function
CallArgument(r, 0, v0),
CallArgument(r, 1, v1_state),
NEW_REACHABLE(r)
.
// CHECKED
// "catchRetry#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a})
// -> ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a})
// -> {"State#" {RealWorld}}
// -> {"GHC.Prim.Unit#" %a}
USED("PrimOp-STM-02")
//Called(r, op),
CallPNode1("catchRetry#-wrapped", r, v0, v2_state),
CallPNode1("catchRetry#-handler", r, v1, v2_state) :-
op = "catchRetry#",
Call(r, op, _),
// pass argument to the wrapped function
// first function
CallArgument(r, 0, v0),
// second function
CallArgument(r, 1, v1),
// state
CallArgument(r, 2, v2_state),
NEW_REACHABLE(r)
.
// CHECKED
// "catchSTM#" :: ({"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a})
// -> (%b -> {"State#" {RealWorld}} -> {"GHC.Prim.Unit#" %a})
// -> {"State#" {RealWorld}}
// -> {"GHC.Prim.Unit#" %a}
// handle the wrapped function
USED("PrimOp-STM-03")
//Called(r, op),
CallPNode1("catchSTM#-wrapped", r, v0, v2_state) :-
op = "catchSTM#",
Call(r, op, _),
// pass argument to the wrapped function
CallArgument(r, 0, v0),
CallArgument(r, 2, v2_state),
NEW_REACHABLE(r)
.
// TODO: check STM implementation, check what exception it can throw
// CHECKED
// NOTE: the handler has its own rule, because it fires only when there are exceptions, while the wrapped function is always called
// handle ex-handler
USED("PrimOp-STM-04")
//Called(r, op),
CallPNode2("catchSTM#-handler", r, v1, ex, v2_state) :-
op = "catchSTM#",
Call(r, op, _),
// pass argument to the handler function
CallArgument(r, 1, v1),
CallArgument(r, 2, v2_state),
RaisedEx(ex),
NEW_REACHABLE(r)
.
// CHECKED
// "newTVar#" :: %a -> {"State#" %s} -> {"GHC.Prim.Unit#" {"TVar#" %s %a}}
// new tvar
USED("PrimOp-STM-05")
//Called(r, op),
TVar(r, ty_node, item) :-
op = "newTVar#",
Call(r, op, _),
// initial item
CallArgument(r, 0, item),
// extract result node
RetTup1Node0(op, ty_node),
NEW_REACHABLE(r)
.
// CHECKED
// "readTVar#" :: {"TVar#" %s %a} -> {"State#" %s} -> {"GHC.Prim.Unit#" %a}
// "readTVarIO#" :: {"TVar#" %s %a} -> {"State#" %s} -> {"GHC.Prim.Unit#" %a}
USED("PrimOp-STM-06")
//Called(r, op),
TypeVarPointsTo(r, ty_node, item) :-
( op = "readTVar#"
; op = "readTVarIO#"
),
Call(r, op, _),
// lookup tvar items
CallArgument(r, 0, arr),
ExternalOrigin(arr, ext_result, arr_node),
TVar(ext_result, arr_node, item),
// lookup result node
RetTup1Node0(op, ty_node),
NEW_REACHABLE(r)
.
// CHECKED
// "writeTVar#" :: {"TVar#" %s %a} -> %a -> {"State#" %s} -> {"GHC.Prim.(##)"}
// extend tvar
USED("PrimOp-STM-07")
//Called(r, op),
TVar(ext_result, ty_node, item) :-
op = "writeTVar#",
Call(r, op, _),
// item to write
CallArgument(r, 1, item),
// lookup tvar
CallArgument(r, 0, arr),
ExternalOrigin(arr, ext_result, ty_node),
// validation
TVar(ext_result, ty_node, _),
NEW_REACHABLE(r)
.
// CHECKED