forked from kframework/c-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
/
syntax.k
128 lines (117 loc) · 6.82 KB
/
syntax.k
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
module C-ABSTRACT-SYNTAX
imports C-SYNTAX
syntax K ::= "AnonymousName" // new, argument is type
rule AnonymousName => #NoName [macro, structural]
syntax C ::= Definition
syntax Definition ::= "DefinitionLoc" "(" K "," K ")"
[klabel('DefinitionLoc)]
syntax Definition ::= "DefinitionLocRange" "(" K "," K "," K ")"
[klabel('DefinitionLocRange)]
// this wraps all statements with their location in the original file
syntax Statement ::= "StatementLoc" "(" K "," K ")"
[klabel('StatementLoc)] // new
rule DefinitionLoc(K:K, L:K) => CodeLoc(K:K, L:K) [macro, structural]
rule StatementLoc(K:K, L:K) => CodeLoc(K:K, L:K) [macro, structural]
rule DefinitionLocRange(K:K, _, L:K) => CodeLoc(K:K, L:K) [macro, structural]
syntax Expression ::= Conditional(K, K, K)
[klabel('Conditional)]
rule Conditional(K1:K, K2:K, K3:K) => K1:K ? K2:K : K3:K [macro, structural]
syntax Expression ::= ArrayIndex(K, K) [klabel('ArrayIndex)]
rule ArrayIndex(K1:K, K2:K) => K1:K[K2:K] [macro, structural]
syntax Expression ::= Negative(K) [klabel('Negative)]
rule Negative(K:K) => - K:K [macro, structural]
syntax Expression ::= Positive(K) [klabel('Positive)]
rule Positive(K:K) => + K:K [macro, structural]
syntax Expression ::= LogicalNot(K) [klabel('LogicalNot)]
rule LogicalNot(K:K) => ! K:K [macro, structural]
syntax Expression ::= BitwiseNot(K) [klabel('BitwiseNot)]
rule BitwiseNot(K:K) => ~ K:K [macro, structural]
syntax Expression ::= Dereference(K) [klabel('Dereference)]
rule Dereference(K:K) => * K:K [macro, structural]
syntax Expression ::= Reference(K) [klabel('Reference)]
rule Reference(K:K) => & K:K [macro, structural]
syntax Expression ::= PreIncrement(K) [klabel('PreIncrement)]
rule PreIncrement(K:K) => ++ K:K [macro, structural]
syntax Expression ::= PreDecrement(K) [klabel('PreDecrement)]
rule PreDecrement(K:K) => -- K:K [macro, structural]
syntax Expression ::= PostIncrement(K) [klabel('PostIncrement)]
rule PostIncrement(K:K) => K:K ++ [macro, structural]
syntax Expression ::= PostDecrement(K) [klabel('PostDecrement)]
rule PostDecrement(K:K) => K:K -- [macro, structural]
syntax Expression ::= Multiply(K, K) [klabel('Multiply)]
rule Multiply(K1:K, K2:K) => K1:K * K2:K [macro, structural]
syntax Expression ::= Divide(K, K) [klabel('Divide)]
rule Divide(K1:K, K2:K) => K1:K / K2:K [macro, structural]
syntax Expression ::= Modulo(K, K) [klabel('Modulo)]
rule Modulo(K1:K, K2:K) => K1:K % K2:K [macro, structural]
syntax Expression ::= Plus(K, K) [klabel('Plus)]
rule Plus(K1:K, K2:K) => K1:K + K2:K [macro, structural]
syntax Expression ::= Minus(K, K) [klabel('Minus)]
rule Minus(K1:K, K2:K) => K1:K - K2:K [macro, structural]
syntax Expression ::= LeftShift(K, K) [klabel('LeftShift)]
rule LeftShift(K1:K, K2:K) => K1:K << K2:K [macro, structural]
syntax Expression ::= RightShift(K, K) [klabel('RightShift)]
rule RightShift(K1:K, K2:K) => K1:K >> K2:K [macro, structural]
syntax Expression ::= LessThan(K, K) [klabel('LessThan)]
rule LessThan(K1:K, K2:K) => K1:K < K2:K [macro, structural]
syntax Expression ::= LessThanOrEqual(K, K) [klabel('LessThanOrEqual)]
rule LessThanOrEqual(K1:K, K2:K) => K1:K <= K2:K [macro, structural]
syntax Expression ::= GreaterThan(K, K) [klabel('GreaterThan)]
rule GreaterThan(K1:K, K2:K) => K1:K > K2:K [macro, structural]
syntax Expression ::= GreaterThanOrEqual(K, K) [klabel('GreaterThanOrEqual)]
rule GreaterThanOrEqual(K1:K, K2:K) => K1:K >= K2:K [macro, structural]
syntax Expression ::= Equality(K, K) [klabel('Equality)]
rule Equality(K1:K, K2:K) => K1:K == K2:K [macro, structural]
syntax Expression ::= NotEquality(K, K) [klabel('NotEquality)]
rule NotEquality(K1:K, K2:K) => K1:K != K2:K [macro, structural]
syntax Expression ::= BitwiseAnd(K, K) [klabel('BitwiseAnd)]
rule BitwiseAnd(K1:K, K2:K) => K1:K & K2:K [macro, structural]
syntax Expression ::= BitwiseXor(K, K) [klabel('BitwiseXor)]
rule BitwiseXor(K1:K, K2:K) => K1:K ^ K2:K [macro, structural]
syntax Expression ::= BitwiseOr(K, K) [klabel('BitwiseOr)]
rule BitwiseOr(K1:K, K2:K) => K1:K | K2:K [macro, structural]
syntax Expression ::= LogicalAnd(K, K) [klabel('LogicalAnd)]
rule LogicalAnd(K1:K, K2:K) => K1:K && K2:K [macro, structural]
syntax Expression ::= LogicalOr(K, K) [klabel('LogicalOr)]
rule LogicalOr(K1:K, K2:K) => K1:K || K2:K [macro, structural]
syntax Expression ::= "Assign" "(" K "," K ")" [klabel('Assign)]
rule Assign(K1:K, K2:K) => K1:K := K2:K [macro, structural]
syntax Expression ::= "AssignMultiply" "(" K "," K ")"
[klabel('AssignMultiply)]
rule AssignMultiply(K1:K, K2:K) => K1:K *= K2:K [macro, structural]
syntax Expression ::= "AssignDivide" "(" K "," K ")"
[klabel('AssignDivide)]
rule AssignDivide(K1:K, K2:K) => K1:K /= K2:K [macro, structural]
syntax Expression ::= "AssignModulo" "(" K "," K ")"
[klabel('AssignModulo)]
rule AssignModulo(K1:K, K2:K) => K1:K %= K2:K [macro, structural]
syntax Expression ::= "AssignPlus" "(" K "," K ")"
[klabel('AssignPlus)]
rule AssignPlus(K1:K, K2:K) => K1:K += K2:K [macro, structural]
syntax Expression ::= "AssignMinus" "(" K "," K ")"
[klabel('AssignMinus)]
rule AssignMinus(K1:K, K2:K) => K1:K -= K2:K [macro, structural]
syntax Expression ::= "AssignBitwiseAnd" "(" K "," K ")"
[klabel('AssignBitwiseAnd)]
rule AssignBitwiseAnd(K1:K, K2:K) => K1:K &= K2:K [macro, structural]
syntax Expression ::= "AssignBitwiseXor" "(" K "," K ")"
[klabel('AssignBitwiseXor)]
rule AssignBitwiseXor(K1:K, K2:K) => K1:K ^= K2:K [macro, structural]
syntax Expression ::= "AssignBitwiseOr" "(" K "," K ")"
[klabel('AssignBitwiseOr)]
rule AssignBitwiseOr(K1:K, K2:K) => K1:K |= K2:K [macro, structural]
syntax Expression ::= "AssignLeftShift" "(" K "," K ")"
[klabel('AssignLeftShift)]
rule AssignLeftShift(K1:K, K2:K) => K1:K <<= K2:K [macro, structural]
syntax Expression ::= "AssignRightShift" "(" K "," K ")"
[klabel('AssignRightShift)]
rule AssignRightShift(K1:K, K2:K) => K1:K >>= K2:K [macro, structural]
syntax Expression ::= Dot(K, CId) [klabel('Dot)]
rule Dot(K:K, X:CId) => K:K . X:CId [macro, structural]
syntax Expression ::= Arrow(K, CId) [klabel('Arrow)]
rule Arrow(K:K, X:CId) => K:K -> X:CId [macro, structural]
/*@ This macro defines an important identity from
\source[n1570]{\para{6.5.3.2}{3}}. As a syntactic macro, it should run
on programs before they even start to reduce. */
rule &(*(K:K)) => K:K [macro, structural]
endmodule