Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Crash in FigureOutNativeType #2095

Closed
cpitclaudel opened this issue May 4, 2022 · 0 comments · Fixed by #2096
Closed

Crash in FigureOutNativeType #2095

cpitclaudel opened this issue May 4, 2022 · 0 comments · Fixed by #2096
Assignees
@cpitclaudel
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking

Comments

@cpitclaudel
Copy link
Member 

module Test {
  const a: bv9
  newtype i = i: int | 0 <= i < if !a == 0 then 3 else 6
}

produces

Unhandled exception. System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.Resolver.<>c__DisplayClass73_0.<FigureOutNativeType>b__1(Expression e, Stack`1 consts) in C:\dafny\Source\Dafny\Resolver.cs:line 3806
   at Microsoft.Dafny.Resolver.<>c__DisplayClass73_0.<FigureOutNativeType>b__1(Expression e, Stack`1 consts) in C:\dafny\Source\Dafny\Resolver.cs:line 3835
   at Microsoft.Dafny.Resolver.<>c__DisplayClass73_0.<FigureOutNativeType>b__1(Expression e, Stack`1 consts) in C:\dafny\Source\Dafny\Resolver.cs:line 4288
   at Microsoft.Dafny.Resolver.<>c__DisplayClass73_0.<FigureOutNativeType>b__2(Expression e) in C:\dafny\Source\Dafny\Resolver.cs:line 4302
   at Microsoft.Dafny.Resolver.FigureOutNativeType(NewtypeDecl dd) in C:\dafny\Source\Dafny\Resolver.cs:line 4320
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in C:\dafny\Source\Dafny\Resolver.cs:line 2887
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in C:\dafny\Source\Dafny\Resolver.cs:line 1032
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in C:\dafny\Source\Dafny\Resolver.cs:line 507
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in C:\dafny\Source\Dafny\DafnyMain.cs:line 162
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in C:\dafny\Source\Dafny\DafnyMain.cs:line 113
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 249
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 67
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass6_0.<Main>b__0() in C:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 47
   at System.Threading.Thread.StartCallback()

I'll have a patch ready soon.
@cpitclaudel cpitclaudel added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking crash Dafny crashes on this input, or generates malformed code that can not be executed labels May 4, 2022
cpitclaudel added a commit that referenced this issue May 4, 2022
@cpitclaudel
refactor(translator): Move resolution of UnaryOpExpr to resolver
535c853 
* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).
@cpitclaudel cpitclaudel mentioned this issue May 4, 2022
Merged
cpitclaudel added a commit that referenced this issue May 4, 2022
@cpitclaudel
refactor(translator): Move resolution of UnaryOpExpr to resolver
5ce88a1 
* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).
cpitclaudel added a commit that referenced this issue May 6, 2022
@cpitclaudel
refactor(translator): Move resolution of UnaryOpExpr to resolver
456d0b1 
* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).
cpitclaudel added a commit that referenced this issue May 7, 2022
@cpitclaudel
refactor(translator): Move resolution of UnaryOpExpr to resolver
a06a168 
* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).
amaurremi added a commit that referenced this issue May 12, 2022
@cpitclaudel @amaurremi
Move resolution of UnaryOpExpr to resolver (#2096)
1647032 
* refactor(translator): Move resolution of UnaryOpExpr to resolver

* Source/Dafny/AST/DafnyAst.cs:

  (ResolvedOpcode):
    New enum.
  (ResolvedOp):
    New property (computed on demand, cached).
  (ResolveOp):
    New function to force the computation of ResolvedOp.

* Source/Dafny/Compilers/SinglePassCompiler.cs:

  (UnaryOpCodeMap):
    New map from resolved unary operators to compiler-level resolved unary
    operators (compilers treat all cardinalities in the same way).

  (TrExpr):
    Simplify `UnaryOpExpr` case using `UnaryOpCodeMap`.

* Source/Dafny/Resolver.cs:

  (FigureOutNativeType):
    Simplify `UnaryOpExpr` case and fix GH-2095.

  (CheckTypeInference_Visitor.VisitOneExpr):
    Force resolution of unary operators.

* Source/Dafny/Resolver/BoundsDiscovery.cs:

  (DiscoverAllBounds_Aux_SingleVar):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Triggers/TriggerExtensions.cs:

  (ShallowEq(BinaryExpr, BinaryExpr)):
    Remove redundant contracts.

  (ShallowEq(UnaryOpExpr, UnaryOpExpr)):
    Compare resolved operators.

* Source/Dafny/Verifier/Translator.ExpressionTranslator.cs:

  (TrExpr):
    Simply `UnaryOpExpr` case.

* Source/Dafny/Verifier/Translator.cs:

  (TrSplitExpr):
    Use `ResolvedOp` (should be a no-op because we're already in Bool context).

* Update Source/Dafny/AST/DafnyAst.cs

* Update Source/Dafny/Resolver.cs

Co-authored-by: Marianna Rapoport <[email protected]>

Co-authored-by: Marianna Rapoport <[email protected]>
@cpitclaudel cpitclaudel self-assigned this Jul 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@cpitclaudel cpitclaudel

Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Move resolution of UnaryOpExpr to resolver dafny-lang/dafny
1 participant
@cpitclaudel