Skip to content

Commit 5c01b36

Browse files
chathhornchathhorn
committed
Some regressions.
1 parent 2dd2f48 commit 5c01b36

10 files changed

Lines changed: 79 additions & 47 deletions

File tree

‎scripts/program-runner‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,7 @@ sub parseRawResultLine {
242242
$parsed->{output} = $1;
243243
};
244244

245-
/< result-value > 'tv\(# (-?\d+)\(\.KList\),,'t\(Set2KLabel \.Set\(\.KList\),,'int\(\.KList\)\)\) <\/ result-value >/ && do {
245+
/< result-value > 'tv\(# (-?\d+)\(\.KList\),,/ && do {
246246
$parsed->{exitCode} = $1;
247247
};
248248
}
@@ -290,11 +290,11 @@ sub parseResult {
290290
$parsed->{output} = $1;
291291
};
292292

293-
/<result-value>\s*tv\s*\(\s*(-?\d+)\s*,\s*t\s*\(\s*\.Set\s*,\s*int\s*\)\s*\)\s*<\/result-value>/ && do {
293+
/<result-value>\s*tv\s*\(\s*(-?\d+)\s*,/ && do {
294294
$parsed->{exitCode} = $1;
295295
};
296296

297-
/<result-value>\s*tv\s*\(\s*NullPointer\s*,\s*t\s*\(\s*\.Set\s*,\s*int\s*\)\s*\)\s*<\/result-value>/ && do {
297+
/<result-value>\s*tv\s*\(\s*NullPointer\s*,/ && do {
298298
$parsed->{exitCode} = 0;
299299
};
300300
}

‎semantics/language/common/conversion.k‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ module C-CONVERSION
5050

5151
rule cast(T':Type, tv(V:CValue, T:Type)) => tv(V, cast(T', T))
5252
when stripQualifiers(T) ==Type stripQualifiers(T')
53+
andBool notBool isPointerType(T')
5354
[structural, anywhere]
5455

5556
/*@ \fromStandard{\source[n1570]{\para{6.3.1.2}{1}}}{
@@ -427,9 +428,9 @@ module C-CONVERSION
427428
syntax Type ::= cast(Type, Type) [function]
428429
429430
rule cast(T':Type, T:Type) => T'
430-
when notBool hasReadFromLoc(T)
431+
when notBool hasReadFrom(T)
431432
rule cast(T':Type, T:Type)
432-
=> addModifier(readFrom(getReadFromLoc(T)), T')
433-
when hasReadFromLoc(T)
433+
=> addModifier(readFrom(getReadFrom(T)), stripReadFrom(T'))
434+
when hasReadFrom(T)
434435
endmodule
435436

‎semantics/language/common/expr/assignment.k‎

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -63,9 +63,12 @@ module C-COMMON-EXPR-ASSIGNMENT
6363
rule nclv(_, t(Mods':Set, pointerType(T':Type)))
6464
:= (tv(V:CValue, t(Mods:Set, pointerType(T:Type)))
6565
=> cast(t(Mods', pointerType(T')), tv(V, t(Mods, pointerType(T)))))
66-
when areCompatible(stripQualifiers(T'), stripQualifiers(T))
67-
andBool (getQualifiers(T) <=Set getQualifiers(T'))
68-
andBool (t(Mods', pointerType(T')) =/=Type t(Mods, pointerType(T)))
66+
when areCompatible(
67+
stripQualifiers(stripAlignas(T')),
68+
stripQualifiers(stripAlignas(T)))
69+
andBool getQualifiers(T) <=Set getQualifiers(T')
70+
andBool t(Mods', pointerType(T')) =/=Type t(Mods, pointerType(T))
71+
andBool getAlignas(T') <=Int getAlignas(T)
6972
[structural]
7073
7174
rule nclv(_, t(Mods':Set, pointerType(T':Type)))
@@ -93,12 +96,17 @@ module C-COMMON-EXPR-ASSIGNMENT
9396
orBool (notBool isPointerType(T') andBool isPointerType(T))
9497
rule (. => ERROR("CEA2", "incompatible pointer types in assignment or function call arguments."))
9598
~> nclv(_, T':Type) := tv(_, T:Type)
99+
// TODO(chathhorn): split these out for better errors.
96100
when isPointerType(T') andBool isPointerType(T)
97101
andBool notBool isVoidType(innerType(T'))
98102
andBool notBool isVoidType(innerType(T))
99-
andBool notBool
100-
((getQualifiers(innerType(T)) <=Set getQualifiers(innerType(T')))
101-
andBool areCompatible(innerType(T'), innerType(T)))
103+
andBool (
104+
notBool areCompatible(
105+
stripQualifiers(stripAlignas(innerType(T'))),
106+
stripQualifiers(stripAlignas(innerType(T))))
107+
orBool notBool (getQualifiers(innerType(T)) <=Set getQualifiers(innerType(T')))
108+
orBool getAlignas(innerType(T')) >Int getAlignas(innerType(T))
109+
)
102110
rule (. => CV("CEA3", "lvalue required as left operand in assignment.", ""))
103111
~> tv(_, _) := tv(_, _)
104112

‎semantics/language/common/memory/reading.k‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,14 @@ module C-MEMORY-READING
3333
/*@ These rules figure out whether the read should be structural or
3434
computational, depending on what is being read */
3535
rule read(Loc:SymLoc, T:Type)
36-
=> readActual(Loc, addModifier(readFrom(stripProv(Loc)), T))
36+
=> readActual(Loc, addModifier(readFrom(stripProv(Loc)),
37+
stripReadFrom(T)))
3738
when isThreadDuration(Loc) orBool isAutoDuration(Loc)
3839
[structural]
3940
// read data of "allocated" duration
4041
rule read(Loc:SymLoc, T:Type)
41-
=> readActual(Loc, addModifier(readFrom(stripProv(Loc)), T))
42+
=> readActual(Loc, addModifier(readFrom(stripProv(Loc)),
43+
stripReadFrom(T)))
4244
when notBool isThreadDuration(Loc)
4345
andBool notBool isAutoDuration(Loc)
4446
andBool Loc =/=K NullPointer

‎semantics/language/common/typing.k‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,6 +159,7 @@ module C-TYPING-SYNTAX
159159
// Strips function and storage specifiers.
160160
syntax Type ::= stripSpecifiers(Type) [function]
161161
syntax Type ::= stripQualifiers(Type) [function]
162+
syntax Type ::= stripAlignas(Type) [function]
162163

163164
syntax Type ::= addQualifier(CVSpecifier, Type) [function]
164165
syntax Type ::= addQualifiers(Set, Type) [function]
@@ -182,15 +183,19 @@ module C-TYPING-SYNTAX
182183
syntax Bool ::= isNullPointerConstant(RValue) [function]
183184
syntax Bool ::= fromConstantExpr(Type) [function]
184185
185-
syntax Bool ::= hasReadFromLoc(Type) [function]
186-
syntax SymLoc ::= getReadFromLoc(Type) [function]
186+
syntax Bool ::= hasReadFrom(Type) [function]
187+
syntax SymLoc ::= getReadFrom(Type) [function]
188+
syntax Type ::= stripReadFrom(Type) [function]
187189
188190
syntax List ::= idsFromParams(List) [function]
189191
190192
syntax Type ::= tagRestrict(RestrictTag, Type) [function]
191193
syntax RestrictTag ::= getRestrictBlock(Type) [function]
192194
193195
syntax Int ::= arrayLength(Type) [function]
196+
197+
syntax Bool ::= hasAlignas(Type) [function]
198+
syntax Bool ::= hasAlignasMod(Set) [function]
194199
endmodule
195200
196201
module C-TYPING

‎semantics/language/common/typing/compatibility.k‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -192,20 +192,17 @@ module C-TYPING-COMPATIBILITY
192192
// It's more complicated than this, too, I think -- e.g.,
193193
// alignas on a definition implies no alignas should be on any
194194
// declaration.
195-
andBool ((#hasAlignas(Mods) =/=K true
196-
orBool #hasAlignas(Mods') =/=K true)
197-
orElseBool getAlignas(Mods) ==Int getAlignas(Mods'))
195+
andBool (((notBool hasAlignasMod(Mods))
196+
andBool (notBool hasAlignasMod(Mods')))
197+
orElseBool getAlignasMod(Mods) ==Int getAlignasMod(Mods'))
198198
199-
rule getAlignas(T:Type) => getAlignas(getModifiers(T))
200-
when #hasAlignas(getModifiers(T)) ==K true
199+
rule getAlignas(T:Type) => getAlignasMod(getModifiers(T))
200+
when hasAlignasMod(getModifiers(T))
201201
rule getAlignas(T:Type) => 1
202-
when #hasAlignas(getModifiers(T)) =/=K true
202+
when notBool hasAlignasMod(getModifiers(T))
203203
204-
syntax Int ::= getAlignas(Set) [function]
205-
rule getAlignas(SetItem(alignas(A:Int)) _) => A
206-
207-
syntax Bool ::= "#hasAlignas" "(" Set ")" [function]
208-
rule #hasAlignas(SetItem(alignas(_)) _) => true
204+
syntax Int ::= getAlignasMod(Set) [function]
205+
rule getAlignasMod(SetItem(alignas(A:Int)) _) => A
209206
210207
// We can assume the types are compatible.
211208
rule compositeType(T:Type, T:Type) => T

‎semantics/language/common/typing/misc.k‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,6 +194,16 @@ module C-TYPING-MISC
194194
rule stripSpecifiers(T:Type)
195195
=> stripStorageSpecifiers(stripFunctionSpecifiers(T))
196196

197+
rule stripAlignas(t(Mods:Set SetItem(alignas(_)), T:SimpleType))
198+
=> stripAlignas(t(Mods, T))
199+
rule stripAlignas(T:Type) => T
200+
when notBool hasAlignas(T)
201+
202+
rule stripReadFrom(t(Mods:Set SetItem(readFrom(_)), T:SimpleType))
203+
=> stripReadFrom(t(Mods, T))
204+
rule stripReadFrom(T:Type) => T
205+
when notBool hasReadFrom(T)
206+
197207
rule addQualifier(Q:CVSpecifier, T:Type)
198208
=> addQualifiers(SetItem(Q), T)
199209

@@ -391,7 +401,7 @@ module C-TYPING-MISC
391401
rule getRestrictBlock(t(SetItem(RestrictBlock(Tag:RestrictTag)) _, _))
392402
=> Tag
393403

394-
rule getReadFromLoc(t(_ SetItem(readFrom(Loc:SymLoc)), _)) => Loc
404+
rule getReadFrom(t(_ SetItem(readFrom(Loc:SymLoc)), _)) => Loc
395405

396406
rule arrayLength(t(_, arrayType(_, N:Int))) => N
397407
/*@ these large numbers are used instead of an infinity---the result of

‎semantics/language/common/typing/predicates.k‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -313,7 +313,13 @@ module C-TYPING-PREDICATES
313313
// TODO(chathhorn)
314314
rule fromConstantExpr(_) => true
315315
316-
rule hasReadFromLoc(t(Mods:Set, _)) => #hasReadFrom(Mods) ==K true
316+
rule hasAlignas(t(Mods:Set, _)) => #hasAlignas(Mods) ==K true
317+
rule hasAlignasMod(Mods:Set) => #hasAlignas(Mods) ==K true
318+
319+
syntax Bool ::= "#hasAlignas" "(" Set ")" [function]
320+
rule #hasAlignas(SetItem(alignas(_)) _) => true
321+
322+
rule hasReadFrom(t(Mods:Set, _)) => #hasReadFrom(Mods) ==K true
317323
318324
syntax Bool ::= "#hasReadFrom" "(" Set ")" [function]
319325
rule #hasReadFrom(_ SetItem(readFrom(_))) => true

‎semantics/language/execution/expr/assignment.k‎

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -12,16 +12,16 @@ module C-EXPR-ASSIGNMENT
1212
~> write(Loc, V, T)
1313
~> transferProv(Loc, tv(V, T))
1414
when notBool isRestrictType(T)
15-
andBool (#fromArrayStatic(T) =/=K true)
15+
andBool (#fromArrayStatic(T') =/=K true)
1616
andBool (T ==Type T')
1717
[structural]
1818
rule nclv(Loc:SymLoc, T':Type) := tv(V:CValue, T:Type)
1919
=> checkOverlap(stripProv(Loc), T)
20-
~> checkArrayStaticAssign(T, tv(V, T))
20+
~> checkArrayStaticAssign(T', tv(V, T))
2121
~> write(Loc, V, T)
2222
~> transferProv(Loc, tv(V, T))
2323
when notBool isRestrictType(T)
24-
andBool (#fromArrayStatic(T) ==K true)
24+
andBool (#fromArrayStatic(T') ==K true)
2525
andBool (T ==Type T')
2626
[structural]
2727
rule nclv(Loc:SymLoc, T':Type) := tv(V:SymLoc, T:Type)
@@ -30,43 +30,44 @@ module C-EXPR-ASSIGNMENT
3030
~> write(Loc, V, T)
3131
~> transferProv(Loc, tv(V, T))
3232
when isRestrictType(T)
33+
andBool (#fromArrayStatic(T') =/=K true)
3334
andBool (T ==Type T')
3435
[structural]
3536
rule nclv(Loc:SymLoc, T':Type) := tv(V:SymLoc, T:Type)
3637
=> checkOverlap(stripProv(Loc), T)
37-
~> checkArrayStaticAssign(T, tv(V, T))
38+
~> checkArrayStaticAssign(T', tv(V, T))
3839
~> checkRestrictAssign(getRestrictBlock(T), getRelevantTags(Loc, V))
3940
~> write(Loc, V, T)
4041
~> transferProv(Loc, tv(V, T))
4142
when isRestrictType(T)
42-
andBool (#fromArrayStatic(T) ==K true)
43+
andBool (#fromArrayStatic(T') ==K true)
4344
andBool (T ==Type T')
4445
[structural]
4546

4647
syntax K ::= checkOverlap(SymLoc, Type)
4748
rule checkOverlap(_, T:Type) => .K
48-
when notBool hasReadFromLoc(T)
49+
when notBool hasReadFrom(T)
4950
[structural]
5051
rule checkOverlap(Loc:SymLoc, T:Type) => .K
51-
when getReadFromLoc(T) ==K Loc
52+
when getReadFrom(T) ==K Loc
5253
[structural]
5354
rule checkOverlap(Loc:SymLoc, T:Type) => .K
54-
when notBool sameBase(getReadFromLoc(T), Loc)
55+
when notBool sameBase(getReadFrom(T), Loc)
5556
[structural]
5657
rule checkOverlap(Loc:SymLoc, T:Type) => .K
57-
when (getReadFromLoc(T) +bytes byteSizeofType(T)) <=bytes Loc
58+
when (getReadFrom(T) +bytes byteSizeofType(T)) <=bytes Loc
5859
[structural]
5960
rule checkOverlap(Loc:SymLoc, T:Type) => .K
60-
when (Loc +bytes byteSizeofType(T)) <=bytes getReadFromLoc(T)
61+
when (Loc +bytes byteSizeofType(T)) <=bytes getReadFrom(T)
6162
[structural]
6263
rule (. => UNDEF("EEA1",
6364
"assignment from non-exactly-overlapping overlapping read.",
6465
"6.5.16.2"))
6566
~> checkOverlap(Loc:SymLoc, T:Type)
66-
when sameBase(getReadFromLoc(T), Loc)
67-
andBool (getReadFromLoc(T) =/=K Loc)
68-
andBool (((getReadFromLoc(T) +bytes byteSizeofType(T)) >bytes Loc)
69-
orBool ((Loc +bytes byteSizeofType(T)) >bytes getReadFromLoc(T)))
67+
when sameBase(getReadFrom(T), Loc)
68+
andBool (getReadFrom(T) =/=K Loc)
69+
andBool (((getReadFrom(T) +bytes byteSizeofType(T)) >bytes Loc)
70+
orBool ((Loc +bytes byteSizeofType(T)) >bytes getReadFrom(T)))
7071
[structural]
7172

7273
syntax Set ::= getRelevantTags(SymLoc, SymLoc) [function]

‎semantics/language/execution/stmt/switch.k‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -75,13 +75,15 @@ module C-STMT-SWITCH
7575
rule tryCase(
7676
(tv(V:K, T':Type) => cast(T, tv(V, T'))),
7777
tv(_, T:Type), _)
78-
when T =/=K T'
78+
when T =/=Type T'
7979
[structural]
80-
rule tryCase(tv(V':K, T:Type), tv(V:K, T:Type), _) => .
81-
when V =/=K V'
80+
rule tryCase(tv(V':K, T':Type), tv(V:K, T:Type), _) => .
81+
when (V =/=K V') andBool (T ==Type T')
8282
[structural]
8383
// match found in value and type, goto it
8484
// don't need to erase the rest of K since we're GOTOing
85-
rule tryCase(V:RValue, V:RValue, CaseHelper:K) => Goto(CaseHelper)
85+
rule tryCase(tv(V:CValue, T':Type), tv(V:CValue, T:Type), CaseHelper:K)
86+
=> Goto(CaseHelper)
87+
when T ==Type T'
8688
[structural]
8789
endmodule

0 commit comments

Comments
 (0)