Fixed type resolution crash (#992)

Type resolution crashes if there is an unknown type name. This PR makes a change so that this unknown name is resolved to bool type to allow type resolution to continue safely.
boogie-org · Dec 2, 2024 · 7f9f784 · 7f9f784
1 parent 3a23efe
commit 7f9f784
Show file tree

Hide file tree

Showing 7 changed files with 14 additions and 11 deletions.
diff --git a/Source/Core/AST/AbsyType.cs b/Source/Core/AST/AbsyType.cs
@@ -1678,8 +1678,8 @@ public override Type ResolveType(ResolutionContext rc)
       }
 
       // otherwise: this name is not declared anywhere
-      rc.Error(this, "undeclared type: {0}", Name);
-      return this;
+      rc.Error(this, "undeclared type: {0} (replacing with \"bool\" to continue resolving)", Name);
+      return Type.Bool;
     }
 
     private List<Type> ResolveArguments(ResolutionContext rc)

diff --git a/Test/bitvectors/bv2.bpl.expect b/Test/bitvectors/bv2.bpl.expect
@@ -1,4 +1,4 @@
 bv2.bpl(6,13): Error: bitvector bounds in illegal position
-bv2.bpl(8,13): Error: undeclared type: x
+bv2.bpl(8,13): Error: undeclared type: x (replacing with "bool" to continue resolving)
 bv2.bpl(9,14): Error: bitvector bounds in illegal position
 3 name resolution errors detected in bv2.bpl
diff --git a/Test/civl/large-samples/shared-vector.bpl b/Test/civl/large-samples/shared-vector.bpl
@@ -38,6 +38,7 @@ modifies IntArrayPool;
 }
 yield procedure {:layer 2} IntArray_Alloc(v: Vec int) returns (loc_iv: Loc)
 refines Atomic_IntArray_Alloc;
+ensures call Yield(loc_iv);
 preserves call IntArrayDom();
 {
   var {:linear} one_loc_mutex: One Loc;
@@ -56,7 +57,7 @@ preserves call IntArrayDom();
   call {:layer 2} OldMutexPool := Copy(MutexPool);
   i := 0;
   while (i < Vec_Len(v))
-  invariant {:layer 2} 0 <= i;
+  invariant {:layer 2} 0 <= i && i <= Vec_Len(v);
   invariant {:layer 2} mutexes->dom == values->dom;
   invariant {:layer 2} mutexes->dom->val == (lambda j: int :: 0 <= j && j < i);
   invariant {:layer 2} (forall j: int:: 0 <= j && j < i ==> Map_Contains(MutexPool, Map_At(mutexes, j)->val));

diff --git a/Test/civl/large-samples/treiber-stack.bpl b/Test/civl/large-samples/treiber-stack.bpl
@@ -70,6 +70,8 @@ modifies TreiberPool;
 }
 yield procedure {:layer 4} Alloc() returns (loc_t: Loc)
 refines AtomicAlloc;
+ensures call TopInStack(loc_t);
+ensures call ReachInStack(loc_t);
 preserves call StackDom();
 {
   var top: Option LocTreiberNode;

diff --git a/Test/test0/Types1.bpl.expect b/Test/test0/Types1.bpl.expect
@@ -1,4 +1,4 @@
-Types1.bpl(8,11): Error: undeclared type: x
-Types1.bpl(9,11): Error: undeclared type: x
-Types1.bpl(9,14): Error: undeclared type: x
+Types1.bpl(8,11): Error: undeclared type: x (replacing with "bool" to continue resolving)
+Types1.bpl(9,11): Error: undeclared type: x (replacing with "bool" to continue resolving)
+Types1.bpl(9,14): Error: undeclared type: x (replacing with "bool" to continue resolving)
 3 name resolution errors detected in Types1.bpl
diff --git a/Test/test20/Prog0.bpl.expect b/Test/test20/Prog0.bpl.expect
@@ -1,5 +1,5 @@
 Prog0.bpl(19,10): Error: type variable must occur in map arguments: a
 Prog0.bpl(31,27): Error: more than one declaration of type variable: beta
-Prog0.bpl(34,22): Error: undeclared type: alpha
-Prog0.bpl(35,35): Error: undeclared type: alpha
+Prog0.bpl(34,22): Error: undeclared type: alpha (replacing with "bool" to continue resolving)
+Prog0.bpl(35,35): Error: undeclared type: alpha (replacing with "bool" to continue resolving)
 4 name resolution errors detected in Prog0.bpl
diff --git a/Test/test20/TypeDecls0.bpl.expect b/Test/test20/TypeDecls0.bpl.expect
@@ -3,8 +3,8 @@ TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a
 TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a
 TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b
 TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C
-TypeDecls0.bpl(26,9): Error: undeclared type: A0
-TypeDecls0.bpl(27,9): Error: undeclared type: F
+TypeDecls0.bpl(26,9): Error: undeclared type: A0 (replacing with "bool" to continue resolving)
+TypeDecls0.bpl(27,9): Error: undeclared type: F (replacing with "bool" to continue resolving)
 TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
 TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
 TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E