Contract.Assert does not cause failures in published Dafny builds

[robin-aws]

Follow-up from #1347 - we've addressed the actual assertion failure, but not the fact that the assertion was only hit when building Dafny from source.

AFAICT, it's likely an issue with how we are calling dotnet publish in Scripts/package.py - perhaps the -c Checked argument is not being picked up by dependent packages?

[sorawee]

I'm not sure if this is related, but I currently have trouble with Contract too, and this is building from source!

Consider:

method Main () 
{
  y :| y in x;
}

This program fails with:

/Users/sorawee/projects/dsmith/tmp.dfy(5,2): Error: unresolved identifier: y
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.ErrorReporter.Error(MessageSource source, Expression e, String msg, Object[] args) in /Users/sorawee/projects/dafny/Source/Dafny/Reporting.cs:line 96
   at Microsoft.Dafny.Resolver.CheckIsLvalue(Expression lhs, ICodeContext codeContext) in /Users/sorawee/projects/dafny/Source/Dafny/Resolver.cs:line 13347
...

At CheckIsLvalue (in Resolver.cs), we can see that there's Contract.Requires(lhs != null);. However, lhs is in fact null, but no error occurs. The same occurs for Error(MessageSource, Expression, string, params object[]) which requires that Expression is not null, but it actually is.

[robin-aws]

It looks like this broke back when we moved to .NET Core and simplified the *.csproj files: https://github.com/dafny-lang/dafny/pull/794

The Contracts methods are conditionally compiled only if there are matching symbols defined. In particular, Assert will be active if DEBUG is defined. The Checked configuration (and others) used to define TRACE;DEBUG;NO_ENABLE_IRONDAFNY, but now only define TRACE.

@sorawee To address your case, it looks like Requires is only active if CONTRACTS_FULL is defined, not just DEBUG, so AFAICT those calls are never evaluated (which is a related but separate problem - I've not yet tracked down at what point we lost or intentionally stopped exercising that mode).

[robin-aws]

I suspect CONTRACTS_FULL was previously set as a side-effect of all of this configuration that we lost: https://github.com/dafny-lang/dafny/pull/794/files?file-filters%5B%5D=.csproj&hide-deleted-files=true#diff-5dc6d3bfa7aee54262f385473d0713ed07fcc57947a59b4eb6d36d003ade2a29L48-L80

[keyboardDrummer]

I believe contracts don't work in .NET Core: https://github.com/dotnet/docs/issues/6361

Only Contracts.Assert still has an effect and it's the same as Debug.Assert, meaning it will throw an error if the assertion fails when the DEBUG constants is defined, which is when running a debug build.

A significant amount of Dafny's usage of contracts, say >50%, relates to nullability, which we can replace with C# 8's support for nullable types. The remaining contracts seem difficult to salvage.

[sorawee]

I separated my issue to #1438.