fix: Correct null-related checking of type bounds, and add axioms

[RustanLeino]

Fixes #5719
Fixes #5726

Description

This PR solves both soundness and incompleteness problems related to when a nullable type extends a trait.

To fix the soundness issue (#5726), the resolver was changed to check type bounds after type inference. For example, the resolver now generates an error if a nullable reference type E? is used as a type argument with a bound B that is not a nullable reference type. Note that this check cannot be done completely during pre-type inference, because pre-types don't distinguish between E? and E; therefore, the definitive check for this is done in the same place where type arguments are checked to have the specified type characteristics ((==), (0), ...).

To fix the incompleteness issues (#5719), changes were made in the generated axioms. To describe them, consider the following types:

trait RefTrait extends object { }
trait GeneralTrait { }  // does not extend object, and thus is not a reference type
class /* or trait */ E extends RefTrait, GeneralTrait { }

• Previously, this generated the following type axioms (and analogous allocation axioms for $IsAlloc):

  // type axiom for trait parent: E extends RefTrait
  axiom (forall $o: ref ::
    { $Is($o, Tclass.E?()) }
    $o != null && $Is($o, Tclass.E?())         // CHANGE: remove o != null
       ==> $Is($o, Tclass.RefTrait()));        // CHANGE: RefTrait --> RefTrait?
  
  // type axiom for trait parent: E extends GeneralTrait
  axiom (forall $o: ref ::
    { $Is($o, Tclass.E?()) }                   // CHANGE:  replace E? with E
    $o != null && $Is($o, Tclass.E?())         // CHANGE:  remove o != null, and replace E? with E
       ==> $IsBox($Box($o), Tclass.GeneralTrait()));

  The new axioms say:

  // type axiom for trait parent: E extends RefTrait
  axiom (forall $o: ref ::
    { $Is($o, Tclass.E?()) }
    $Is($o, Tclass.E?()) ==> $Is($o, Tclass.RefTrait?()));
  
  // type axiom for trait parent: E extends GeneralTrait
  axiom (forall $o: ref ::
     { $Is($o, Tclass.E()) }
    $Is($o, Tclass.E()) ==> $IsBox($Box($o), Tclass.GeneralTrait()));

• To make the first of these axioms still be able to connect E? with RefTrait, the axiom that connects a nullable type X? with its non-null reference type X was extended with an additional matching pattern:

  // $Is axiom for non-null type X
  axiom (forall c#0: ref :: 
    { $Is(c#0, Tclass.X()) }
    { $Is(c#0, Tclass.X?()) }      // CHANGE: this matching pattern was added
    $Is(c#0, Tclass.X()) <==> $Is(c#0, Tclass.X?()) && c#0 != null);

• The property that a type parameter T with a bound B has is (elsewhere) given as a quantification over boxes. To make this property known of a type that extends a trait, the following axioms were added:

  axiom (forall bx: Box :: 
    { $IsBox(bx, Tclass.E?()) } 
    $IsBox(bx, Tclass.E?()) ==> $IsBox(bx, Tclass.RefTrait?()));
  
  axiom (forall bx: Box :: 
    { $IsBox(bx, Tclass.E()) } 
    $IsBox(bx, Tclass.E()) ==> $IsBox(bx, Tclass.GeneralTrait()));

  These are essentially box versions of the type axioms above.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[atomb]

This all looks reasonable. And it's thoroughly tested!