more fixes relating to provenance, pointers, and unspecified values (#…

…178)

* more fixes relating to provenance, pointers, and unspecified values

* more fixes for cerberus tests

* temp

* more cerberus tweaks

* add tests to test suite

* fix whitespace

* fix examples

* fix syntax error

* fix another bug

* fix tests

* fix one more test

* some minor bug fixes

* fix another issue with equality types

* another bug fix in a test

* add some exceptions for commonly used integer constants cast to pointers

* fix another broken test

* fix test failure

examples/error-codes/Error_Codes.csv

@@ -19,7 +19,6 @@ UB-CCV12,Floating-point overflow.,"6.5:5, J.2:1 item 36",Undefined Behavior,
 UB-CEA1,A pointer (or array subscript) outside the bounds of an object.,"6.5.6:8, J.2:1 item 46",Undefined Behavior,
 UB-CEA5,Computing pointer difference between two different objects.,"6.5.6:9, J.2:1 item 48",Undefined Behavior,
 UB-CEA2,Pointer difference outside the range that can be represented by object of type ptrdiff_t.,"6.5.6:9, J.2:1 item 50",Undefined Behavior,
-UB-CEA6,"Unspecified value in signed addition, possible overflow.","6.5:5, J.2:1 item 36",Undefined Behavior,
 UB-CEB2,The right operand in a bitwise shift is negative.,"6.5.7:3, J.2:1 item 51",Undefined Behavior,
 UB-CEB3,The right operand in a bitwise shift is greater than or equal to the bit width of the left operand.,"6.5.7:3, J.2:1 item 51",Undefined Behavior,
 UB-CEB4,The left operand in a bitwise left-shift is negative.,"6.5.7:4, J.2:1 item 52",Undefined Behavior,
@@ -110,9 +109,11 @@ UB-PTHREAD5,Called lock on an object that was not initialized with pthread_mutex
 UB-PTHREAD6,Attempting to unlock a PTHREAD_MUTEX_DEFAULT or PTHREAD_MUTEX_NORMAL mutex which is not robust and which has not been locked by the current thread.,POSIX 2008 sec. pthread_mutex_lock,Undefined Behavior,X
 UB-PTHREAD7,Called unlock on an object that was not initialized with pthread_mutex_init.,POSIX 2008 sec. pthread_mutex_unlock,Undefined Behavior,X
 UB-PTHREAD8,Called trylock on an object that was not initialized with pthread_mutex_init.,POSIX 2008 sec. pthread_mutex_trylock,Undefined Behavior,X
-USP-CEER2,Trying to reinterpret integer bytes as floating bytes.,"6.2.6.1:1, J.1:1 item 9",Unspecified Behavior,
 USP-CEER6,Unspecified value returned from main function.,5.1.2.2.3:1,Unspecified Behavior,
 USP-CERL7,Comparison of unspecified value.,6.5.9,Unspecified Behavior,
+USP-CMR1,Trying to reinterpret integer bytes as floating bytes.,"6.2.6.1:1, J.1:1 item 9",Unspecified Behavior,
+USP-CMR2,Trying to reinterpret floatng bytes as integer bytes.,"6.2.6.1:1, J.1:1 item 9",Unspecified Behavior,
+USP-ESS1,Switching on an unspecified controlling expression.,6.8.4.2:5,Unspecified Behavior,
 USP-STDIO2,Printing an unspecified value.,7.21.6.1:8,Unspcified Behavior,
 USP-STDLIB3,Called the atexit function after normal program termination has begun.,"7.22.4.2:2, J.1:1 item 44",Unspecified Behavior,
 USP-STDLIB6,Called the at_quick_exit function after normal program termination has begun.,"7.22.4.3:2, J.1:1 item 45",Unspecified Behavior,
@@ -133,6 +134,8 @@ CV-CEM3,Attempting to access member but it does not exist.,6.5.2.3:1,Constraint
 CV-CER1,Unary '&' operator applied to non-lvalue.,6.5.3.2:1,Constraint Violation,
 CV-CER2,Unary '&' operator applied to a value with register storage class.,6.5.3.2:1,Constraint Violation,
 CV-CERL5,Directly comparing an integer type with a pointer type.,6.5.8:2,Constraint Violation,
+CV-CERL8,Invalid opeand types to ==.,6.5.9:2,Constraint Violation,
+CV-CERL9,Invalid opeand types to !=.,6.5.9:2,Constraint Violation,
 CV-CMW2,Trying to write through a const lvalue.,6.5.16.1:1,Constraint Violation,
 CV-TDG2,Declaration for identifier appears with multiple storage class specifiers.,6.7.1:2,Constraint Violation,
 CV-TDG4,Declaration appears with invalid storage class specifiers.,6.9:2,Constraint Violation,
@@ -169,7 +172,6 @@ CV-SSA2,Static assertion failed: ,6.7.10:2,Constraint Violation,
 CV-CTI3,The width of a bit field shall be an integer constant expression.,6.7.2.1:4,Constraint Violation,
 CV-CTI2,Arrays must have positive length.,6.7.6.2:1,Constraint Violation,
 IMPL-CCV2,Conversion to signed integer outside the range that can be represented.,"6.3.1.3:3, J.3.5:1 item 4",Implementation Defined Behavior,
-IMPL-CCV8,Conversion of a null pointer fragment to an integer type.,"6.3.2.3:6, J.3.7:1 item 1",Implementation Defined Behavior,
 IMPL-CEB8,The left operand in a bitwise right-shift is negative.,"6.5.7:5, J.3.5:1 item 5",Implementation Defined Behavior,
 IMPL-CTI4,"Bitfield with type other than signed int, unsigned int, or _Bool.","6.7.2.1:5, J.3.9:1 item 2",Implementation Defined Behavior,
 IMPL-EIO5,Trying to modify an object with thread or auto storage duration in a thread other than the one in which the object is associated.,"6.2.4:4, 6.2.4:5, J.3.13:1 item 2",Implementation Defined Behavior,

examples/error-codes/undefined/UB-EIO10-bad.output

@@ -4,7 +4,7 @@ Type: Undefined behavior.
 See also: C11 sec. 6.5:7, J.2:1 item 37
   at main(UB-EIO10-bad.c:6)
   at <file-scope>(<unknown>)
-Error: USP-CEER2
+Error: USP-CMR1
 Description: Trying to reinterpret integer bytes as floating bytes.
 Type: Unspecified value or behavior.
 See also: C11 sec. 6.2.6.1:1, J.1:1 item 9

examples/error-codes/undefined/UB-STDLIB1-bad.c

@@ -4,6 +4,6 @@
 int main(void){
 	char a[5] = "abc";
 	char* p = realloc(a, 5);
-	p[0];
+	p[0] = 'a';
 	return 0;
 }

examples/error-codes/undefined/UB-STDLIB1-good.c

@@ -4,6 +4,6 @@
 int main(void){
 	unsigned char a[5] = "abc";
 	unsigned char* p = realloc(0, 5);
-	p[0];
+	p[0] = 'a';
 	return 0;
 }

examples/error-codes/unspecified/Makefile

@@ -32,11 +32,6 @@ comparison: ${TEST_COMPARISON}
 	@echo -n "Running $<... "
 	@./$< > $@.tmp 2>&1; ${CHECK_RESULT_RUN}
 
-# we handle this case specially because unlike the others, it by necessity returns an error code on the command line
-USP-CEER6-bad.out: USP-CEER6-bad.kcc
-	@echo -n "Running $<... "
-	@./$< > $@.tmp 2>&1; ${CHECK_RESULT_RUN_FATAL}
-
 %-good.gcc: %-good.c
 	@echo -n "Compiling $< (reference)... "
 	@$(CC) -std=c11 -o $@ $< -lm > $@.tmp.out 2>&1; ${CHECK_RESULT_COMPILE}

examples/error-codes/unspecified/USP-CEER6-bad.output

@@ -2,4 +2,3 @@ Error: USP-CEER6
 Description: Unspecified value returned from main function.
 Type: Unspecified value or behavior.
 See also: C11 sec. 5.1.2.2.3:1
-Execution failed (configuration dumped)

examples/error-codes/unspecified/USP-CEER2-bad.output → examples/error-codes/unspecified/USP-CMR1-bad.output

@@ -1,6 +1,6 @@
-Error: USP-CEER2
+Error: USP-CMR1
 Description: Trying to reinterpret integer bytes as floating bytes.
 Type: Unspecified value or behavior.
 See also: C11 sec. 6.2.6.1:1, J.1:1 item 9
-  at main(USP-CEER2-bad.c:10)
+  at main(USP-CMR1-bad.c:10)
   at <file-scope>(<unknown>)

examples/error-codes/undefined/UB-CEA6-good.c → examples/error-codes/unspecified/USP-CMR2-bad.c

@@ -1,12 +1,12 @@
 // Copyright (c) 2015 Runtime Verification, Inc. (RV-Match team). All Rights Reserved.
 
-int x;
 union {
-  short x;
-  int y;
+  int x;
+  float y;
 } foo;
-int main(void){
-  foo.y = 1;
-  int y = 5 + foo.y;
+
+int main() {
+  foo.y = 1.0;
+  int x = foo.x;
   return 0;
 }

examples/error-codes/unspecified/USP-CMR2-bad.output

@@ -0,0 +1,6 @@
+Error: USP-CMR2
+Description: Trying to reinterpret floating bytes as integer bytes.
+Type: Unspecified value or behavior.
+See also: C11 sec. 6.2.6.1:1, J.1:1 item 9
+  at main(USP-CMR2-bad.c:10)
+  at <file-scope>(<unknown>)

examples/error-codes/undefined/UB-CEA6-bad.c → examples/error-codes/unspecified/USP-CMR2-good.c

@@ -1,12 +1,12 @@
 // Copyright (c) 2015 Runtime Verification, Inc. (RV-Match team). All Rights Reserved.
 
-int x;
 union {
-  short x;
-  int y;
+  int x;
+  float y;
 } foo;
-int main(void){
-  foo.x = 1;
-  int y = 5 + foo.y;
+
+int main() {
+  foo.y = 1.0;
+  char x = *((char *)&foo.x);
   return 0;
 }

examples/error-codes/unspecified/USP-ESS1-bad.c

@@ -0,0 +1,13 @@
+union U {
+	char a;
+	int b;
+} u;
+
+int main(void){
+	u.b = 0;
+	u.a = 0;
+	switch(u.b) {
+        case 1:
+            break;
+        }
+}

examples/error-codes/unspecified/USP-ESS1-bad.output

@@ -0,0 +1,6 @@
+Error: USP-ESS1
+Description: Switching on an unspecified controlling expression.
+Type: Unspecified value or behavior.
+See also: C11 sec. 6.8.4.2:5
+  at main(USP-ESS1-bad.c:9)
+  at <file-scope>(<unknown>)

examples/error-codes/unspecified/USP-ESS1-good.c

@@ -0,0 +1,14 @@
+union U {
+	char a;
+	int b;
+} u;
+
+int main(void){
+	u.b = 0;
+	u.a = 0;
+        // u.b is now unspecified
+	switch(u.a) {
+        case 1:
+            break;
+        }
+}

examples/error-codes/unspecified/USP-STDIO2-bad.output

@@ -5,4 +5,4 @@ See also: C11 sec. 7.21.6.1:8
   at printf(USP-STDIO2-bad.c:10)
   at main(USP-STDIO2-bad.c:10)
   at <file-scope>(<unknown>)
-0
+2139062016

examples/error-codes/violates-constraint/fatal/CV-CERL8-bad-static.c

@@ -0,0 +1,8 @@
+int main() {
+  float a;
+  float *b = &a;
+  int x;
+  int *y = &x;
+  y == b;
+  return 0;
+}

examples/error-codes/violates-constraint/fatal/CV-CERL8-bad-static.output

@@ -0,0 +1,7 @@
+File: CV-CERL8-bad-static.c
+Line: 6
+Error: CV-CERL8
+Description: Invalid operand types to ==.
+Type: Constraint violation.
+See also: C11 sec. 6.5.9:2
+Translation failed (config dumped). Run kcc -d CV-CERL8-bad-static.c to see commands run.

examples/error-codes/violates-constraint/fatal/CV-CERL8-good.c

@@ -0,0 +1,8 @@
+int main() {
+  float a;
+  float *b = &a;
+  int x;
+  int *y = &x;
+  y == (int *)b;
+  return 0;
+}

examples/error-codes/violates-constraint/fatal/CV-CERL9-bad-static.c

@@ -0,0 +1,8 @@
+int main() {
+  float a;
+  float *b = &a;
+  int x;
+  int *y = &x;
+  y != b;
+  return 0;
+}

examples/error-codes/violates-constraint/fatal/CV-CERL9-bad-static.output

@@ -0,0 +1,7 @@
+File: CV-CERL9-bad-static.c
+Line: 6
+Error: CV-CERL9
+Description: Invalid operand types to !=.
+Type: Constraint violation.
+See also: C11 sec. 6.5.9:2
+Translation failed (config dumped). Run kcc -d CV-CERL9-bad-static.c to see commands run.

examples/error-codes/violates-constraint/fatal/CV-CERL9-good.c

@@ -0,0 +1,8 @@
+int main() {
+  float a;
+  float *b = &a;
+  int x;
+  int *y = &x;
+  y != (int *)b;
+  return 0;
+}

examples/error-codes/violates-constraint/nonfatal/CV-TTE3-bad-static.c

@@ -2,6 +2,6 @@
 
 int main() {
   int x = 0;
-  int *y = 1 ? &x : 1;
+  int *y = 1 ? &x : 2;
   return 0;
 }

examples/error-codes/violates-constraint/nonfatal/CV-TTE3-bad-static.output

@@ -4,3 +4,9 @@ Error: CV-TTE3
 Description: if one of a conditional expression's branches has pointer type and the other has integer type, the integer must be a null pointer constant.
 Type: Constraint violation.
 See also: C11 sec. 6.5.15:3
+File: CV-TTE3-bad-static.c
+Line: 5
+Error: UB-CEE2
+Description: Indeterminate value used in an expression.
+Type: Undefined behavior.
+See also: C11 sec. 6.2.4, 6.7.9, 6.8, J.2:1 item 11

rv-match/x86-gcc-limited-libc/semantics/settings.k

@@ -48,7 +48,7 @@ module C-SETTINGS
 
      rule cfg:intToPointer(0, _) => NullPointer
      rule cfg:intToPointer(_, _) => trap [owise]
-     rule cfg:pointerToInt(_, _) => unknown
+     rule cfg:pointerToInt(_, T::UType) => unknown(max(T))
 
      rule isErrorRecovery => true
      rule hasLint => true

semantics/language/common/bits.k

@@ -2,8 +2,7 @@ module C-BITS-SYNTAX
      imports C-SYMLOC-SYNTAX
 
      syntax Trap ::= "trap" [klabel(trap)]
-     syntax Unknown ::= "unknown" [klabel(unknown)]
-     syntax Unknown ::= unknownAlignedInt(Int)
+     syntax Unknown ::= unknown(Int)
      syntax Bits ::= Trap
      syntax Bits ::= Unknown
 
@@ -14,23 +13,37 @@ module C-BITS-SYNTAX
      syntax Bits ::= bitRange(Bits, Int, Int)
 
      // value, (length - byte-offset), type
-     syntax Bits ::= encodedFloat(Float, Int, UType)
+     syntax Bits ::= encodedFloat(Float, Int, Int, UType)
      // object, start piece, end piece
-     syntax Bits ::= subObject(SymLoc, Int, Int)
+     syntax SubObject ::= subObject(SymLoc, Int, Int)
+     syntax Bits ::= SubObject
+     syntax IntPtr ::= SubObject
 
      syntax KItem ::= fillToBytes(K) [strict]
      syntax KItem ::= "fillToBytes-aux" "(" K "," List ")" [function]
 
      syntax DataList ::= dataList(List)
      syntax KResult ::= DataList
 
+     syntax KItem ::= makeUnknown(K) [function, klabel(makeUnknown1)]
+     syntax KItem ::= makeUnknown2(K) [strict]
+     syntax KItem ::= stripUnknown(K) [function]
+
+     syntax Int ::= maxIntPtrValue(IntPtr) [function]
+     syntax SymLoc ::= locOf(SubObject) [function]
+
 endmodule
 
 module C-BITS
      imports C-BITS-SYNTAX
      imports COMPAT-SYNTAX
      imports C-SETTINGS-SYNTAX
 
+     rule base(subObject(S:SymLoc, _, _)) => base(S)
+     rule sameBase((subObject(S:SymLoc, _, _) => S), _)
+     rule sameBase(_, (subObject(S:SymLoc, _, _) => S))
+     rule locOf(subObject(S:SymLoc, _, _)) => S
+
      // this maintains byte order
      rule fillToBytes(dataList(L:List))
           => fillToBytes-aux(dataList(L), .List)
@@ -60,6 +73,16 @@ module C-BITS
      rule fillToBytes-aux(dataList(.List), L:List) => dataList(L)
           [structural]
 
+     rule makeUnknown(tv(I:Int, T::UType)) => tv(unknown(I), T)
+     rule makeUnknown(R::RValue) => R [owise]
+     rule makeUnknown2(R:RValue) => makeUnknown(R)
+     rule stripUnknown(tv(unknown(I:Int), T::UType)) => tv(I, T)
+     rule stripUnknown(tv(V::CValue, T::UType)) => tv(V, T)
+          requires notBool isUnknown(V)
+
+     rule maxIntPtrValue(_:SymLoc) => (1 <<Int (cfg:bitsPerByte *Int cfg:ptrsize -Int 1)) -Int 1
+     rule maxIntPtrValue(subObject(_, N:Int, M:Int)) => (1 <<Int (cfg:bitsPerByte *Int (M -Int N +Int 1) -Int 1)) -Int 1
+
      // coallesce bitranges that are adjacent
      rule piece(bitRange(N::Bits, SuccTo:Int, To':Int), Len:Int)
                bit:: piece(bitRange(N, From:Int, To:Int), Len':Int)

semantics/language/common/conversion.k

@@ -31,7 +31,7 @@ module C-CONVERSION
      rule arithInterpret(T:IntegerUType, N:Int) => tv(N, T)
           requires (min(T) <=Int N)
                andBool (max(T) >=Int N)
-     rule arithInterpret(T::UType, unknown) => tv(unknown, T)
+     rule arithInterpret(T::UType, unknown(I:Int)) => makeUnknown(arithInterpret(T, I))
      rule arithInterpret(T::UType, trap) => trap(T)
      rule arithInterpret(T:FloatUType, F:Float) => tv(F, T)
           requires fmin(T) <=Float F andBool fmax(T) >=Float F
@@ -84,17 +84,9 @@ module C-CONVERSION
           => tv(V, cast(T', T))
           requires notBool isBoolUType(T')
                andBool inRange(V, T')
-     rule cast(T':IntegerUType, tv(subObject(NullPointer, N:Int, M:Int), T:IntegerUType))
-          => castHold(T', tv(subObject(NullPointer, N, M), T))
-          requires notBool isBoolUType(T')
-               andBool M -Int N <Int byteSizeofType(T')
-
-     rule (.K => IMPL("CCV8", "Conversion of a null pointer fragment to an integer type.", "6.3.2.3:6, J.3.7:1 item 1") )
-          ~> castHold(T':IntegerUType, tv(subObject(NullPointer, N:Int, M:Int), T:IntegerUType))
 
      rule cast(T':IntegerUType, tv(subObject(L:SymLoc, N:Int, M:Int), T:IntegerUType)) => tv(subObject(L, N, M), T')
           requires notBool isBoolUType(T')
-               andBool L =/=K NullPointer
                andBool M -Int N <Int byteSizeofType(T')
 
      /*@ \fromStandard{\source[n1570]{\para{6.3.1.3}{2}}}{
@@ -171,8 +163,9 @@ module C-CONVERSION
           requires notBool inRange(I, T')
           [structural]
 
-     rule cast(T'::UType, tv(unknown, T::UType))
-          => tv(unknown, cast(T', T))
+     rule cast(T'::UType, tv(unknown(I:Int), T::UType))
+          => makeUnknown(cast(T', tv(I, T)))
+          requires notBool isPointerUType(T')
 
      /*@ \fromStandard{\source[n1570]{\para{6.3.1.4}{1}}}{
      When a finite value of real floating type is converted to an integer type