Using CVC4 crashes on linux with broken pipe

I'm trying to verify a program using Boogie and CVC4, but I get the following error:

$ ./Source/BoogieDriver/bin/Debug/netcoreapp3.1/BoogieDriver ~/Workbench/Projects/vercors/temp.bpl /proverOpt:SOLVER=CVC4
Unhandled exception. System.AggregateException: One or more errors occurred. (Broken pipe) (Broken pipe) (Broken pipe) (Broken pipe) (Broken pipe) (Broken pipe)
 ---> System.IO.IOException: Broken pipe
   at System.IO.FileStream.WriteNative(ReadOnlySpan`1 source)
   at System.IO.FileStream.FlushWriteBuffer()
   at System.IO.FileStream.FlushInternalBuffer()
   at System.IO.FileStream.Flush(Boolean flushToDisk)
   at System.IO.FileStream.Flush()
   at System.IO.StreamWriter.Flush(Boolean flushStream, Boolean flushEncoder)
   at System.IO.StreamWriter.WriteLine(String value)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.Send(String cmd) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 111
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send(String s, Boolean isCommon) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 214
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendCommon(String s) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 198
   at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable`1 coll, Action`1 fn) in /home/bobe/Downloads/boogie/Source/Core/Util.cs:line 63
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.FlushAxioms() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 486
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 553
   at Microsoft.Boogie.Checker.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler, Int32 timeout, Int32 rlimit, Nullable`1 randomSeed) in /home/bobe/Downloads/boogie/Source/VCGeneration/Checker.cs:line 374
   at VC.Split.BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, Int32 no, Int32 timeout, Int32 rlimit) in /home/bobe/Downloads/boogie/Source/VCGeneration/Split.cs:line 1174
   at VC.VCGen.SplitAndVerify(Implementation impl, Dictionary`2 gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, Outcome& outcome) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 882
   at VC.VCGen.VerifyImplementation(Implementation impl, VerifierCallback callback) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 1086
   at VC.ConditionGeneration.VerifyImplementation(Implementation impl, List`1& errors, String requestId) in /home/bobe/Downloads/boogie/Source/VCGeneration/ConditionGeneration.cs:line 137
   at Microsoft.Boogie.ExecutionEngine.VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, String requestId, Dictionary`2 extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, Int32 index, OutputCollector outputCollector, List`1 checkers, String programId) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 1201
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass28_2.<InferAndVerify>b__5(Object dummy) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 992
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__274_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location where exception was thrown ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)
   --- End of inner exception stack trace ---
   at System.AggregateException.Handle(Func`2 predicate)
   at Microsoft.Boogie.ExecutionEngine.InferAndVerify(Program program, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 1026
   at Microsoft.Boogie.ExecutionEngine.ProcessFiles(IList`1 fileNames, Boolean lookForSnapshots, String programId) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 511
   at Microsoft.Boogie.OnlyBoogie.Main(String[] args) in /home/bobe/Downloads/boogie/Source/BoogieDriver/BoogieDriver.cs:line 65
 ---> (Inner Exception #1) System.IO.IOException: Broken pipe
   at System.IO.FileStream.WriteNative(ReadOnlySpan`1 source)
   at System.IO.FileStream.FlushWriteBuffer()
   at System.IO.FileStream.FlushInternalBuffer()
   at System.IO.FileStream.Flush(Boolean flushToDisk)
   at System.IO.FileStream.Flush()
   at System.IO.StreamWriter.Flush(Boolean flushStream, Boolean flushEncoder)
   at System.IO.StreamWriter.WriteLine(String value)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.Send(String cmd) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 111
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send(String s, Boolean isCommon) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 214
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendCommon(String s) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 198
   at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable`1 coll, Action`1 fn) in /home/bobe/Downloads/boogie/Source/Core/Util.cs:line 63
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.FlushAxioms() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 486
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.FlushAndCacheCommons() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 477
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 539
   at Microsoft.Boogie.Checker.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler, Int32 timeout, Int32 rlimit, Nullable`1 randomSeed) in /home/bobe/Downloads/boogie/Source/VCGeneration/Checker.cs:line 374
   at VC.Split.BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, Int32 no, Int32 timeout, Int32 rlimit) in /home/bobe/Downloads/boogie/Source/VCGeneration/Split.cs:line 1174
   at VC.VCGen.SplitAndVerify(Implementation impl, Dictionary`2 gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, Outcome& outcome) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 882
   at VC.VCGen.VerifyImplementation(Implementation impl, VerifierCallback callback) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 1086
   at VC.ConditionGeneration.VerifyImplementation(Implementation impl, List`1& errors, String requestId) in /home/bobe/Downloads/boogie/Source/VCGeneration/ConditionGeneration.cs:line 137
   at Microsoft.Boogie.ExecutionEngine.VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, String requestId, Dictionary`2 extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, Int32 index, OutputCollector outputCollector, List`1 checkers, String programId) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 1201
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass28_2.<InferAndVerify>b__5(Object dummy) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 992
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__274_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location where exception was thrown ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)<---

 ---> (Inner Exception #2) System.IO.IOException: Broken pipe
   at System.IO.FileStream.WriteNative(ReadOnlySpan`1 source)
   at System.IO.FileStream.FlushWriteBuffer()
   at System.IO.FileStream.FlushInternalBuffer()
   at System.IO.FileStream.Flush(Boolean flushToDisk)
   at System.IO.FileStream.Flush()
   at System.IO.StreamWriter.Flush(Boolean flushStream, Boolean flushEncoder)
   at System.IO.StreamWriter.WriteLine(String value)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.Send(String cmd) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 111
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send(String s, Boolean isCommon) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 214
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendCommon(String s) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 198
   at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable`1 coll, Action`1 fn) in /home/bobe/Downloads/boogie/Source/Core/Util.cs:line 63
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.FlushAxioms() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 486
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.FlushAndCacheCommons() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 477
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler) in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs:line 539
   at Microsoft.Boogie.Checker.BeginCheck(String descriptiveName, VCExpr vc, ErrorHandler handler, Int32 timeout, Int32 rlimit, Nullable`1 randomSeed) in /home/bobe/Downloads/boogie/Source/VCGeneration/Checker.cs:line 374
   at VC.Split.BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, Int32 no, Int32 timeout, Int32 rlimit) in /home/bobe/Downloads/boogie/Source/VCGeneration/Split.cs:line 1174
   at VC.VCGen.SplitAndVerify(Implementation impl, Dictionary`2 gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, Outcome& outcome) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 882
   at VC.VCGen.VerifyImplementation(Implementation impl, VerifierCallback callback) in /home/bobe/Downloads/boogie/Source/VCGeneration/VCGen.cs:line 1086
   at VC.ConditionGeneration.VerifyImplementation(Implementation impl, List`1& errors, String requestId) in /home/bobe/Downloads/boogie/Source/VCGeneration/ConditionGeneration.cs:line 137
   at Microsoft.Boogie.ExecutionEngine.VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, String requestId, Dictionary`2 extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, Int32 index, OutputCollector outputCollector, List`1 checkers, String programId) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 1201
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass28_2.<InferAndVerify>b__5(Object dummy) in /home/bobe/Downloads/boogie/Source/ExecutionEngine/ExecutionEngine.cs:line 992
   at System.Threading.Tasks.Task.InnerInvoke()
   at System.Threading.Tasks.Task.<>c.<.cctor>b__274_0(Object obj)
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
--- End of stack trace from previous location where exception was thrown ---
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread)<---

Aborted (core dumped)

It's the following file: temp.bpl.txt. It's the output of viper's carbon backend, which in turn was processing an example from the VerCors verifier. The original program only consisted of a few goto statements, so I don't think the .bpl input program is doing very complex things.

CVC4 version (installed through the manjaro package manager):

$ cvc4 --version
This is CVC4 version 1.8
compiled with GCC version 10.2.0
on Sep 14 2020 11:24:28

Boogie version (compiled from master)

$ ./Source/BoogieDriver/bin/Debug/netcoreapp3.1/BoogieDriver /version
Boogie program verifier version 2.8.29.0, Copyright (c) 2003-2014, Microsoft.

I'm running Manjaro. To compile boogie, I used the "dotnet-runtime-bin" (5.0.5.sdk202-1) package on AUR and the "dotnet-sdk-bin" (also 5.0.5.sdk202-1) from AUR. For running it I needed the "dotnet-runtime-3.1" package from the official manjaro repositories (not sure why these were needed, since I compiled with 5...?). Verifying the file without the /proverOpt flag verifies it as expected (one assert failed).

Is this beyond the "experimental support", or is it possible to fix this? (Or, even better, is there a crucial piece of machinery I missed?)

I believe CVC4 is terminating unexpectedly. As a result, the pipe from Boogie to CVC4 is broken and Boogie crashes. I ran CVC4 directly on the generated SMTLIB2 file and got the following parse error:

(error "Parse Error: temp.smt2:27.36: Symbol 'RoundingMode' not declared as a type")

You can generate the SMTLIB2 file yourself to do the experiment yourself as follows:

boogie /proverOpt:SOLVER=cvc4 temp.bpl /proverLog:temp.smt2

RoundingMode appears to be a built-in type that is understood by Z3 but not CVC4. Not sure what in the Boogie file is generating an expression of type RoundingMode. Perhaps, the use of the type real:

type Perm = real;

RoundingMode must be related to the floating-point type we added to Boogie. Note that CVC4 does not support the full-blown SMT theory of floating-points (as far as I know), which is probably what is causing this issue. I suggest you either study what exactly CVC4 supports in terms of floating-points (and make sure your Boogie program matches that), or you drop floating-points from your Boogie program, or you use Z3 instead of CVC4.

@shazqadeer Thank you for the detailed explanation. I cannot reproduce your error however, for me it complains about a type "RegEx" not existing. Are you using cvc4 from the master branch? While I'm using the latest release, I think mine is still quite old compared to cvc4 master.

@zvonimir I have minimised my input program up to this minimal program:

type Ref;
type Field A B;

procedure myproc() returns (Result: bool)
{
}

At this point, removing either Field A B or myproc causes it to verify without problems. Below I have included the smt2 for both with Field and without Field:

Without Field, the smt2 becomes very minimal, only 10 lines or so, so I'm not surprised cvc4 doesn't complain in that case. It seems some kind of preamble is emitted when Field is included? I have a feeling I minimised it too far, if @shazqadeer can confirm which version of cvc4 he is using I can get that version as well and have another try at minimising the file more effectively.

As for the floating-point aspect, I don't think my input program uses floating point explicitly. We do use reals, as @shazqadeer pointed out. There are also some decimal numbers in the file (1.00000 and 0.00000), but these are assigned to reals immediately. It might be that reals are also divided, but I would assume that division of reals stays within the real type...? Could it be that those literals are triggering the floating-point logic?

In any case, I think I first have to be able to reproduce @shazqadeer's error, before I can debug this further. I would be very grateful if you could have another look at my problem with this new information.

Edit: I have downloaded the latest cvc4 nightly version, which is almost a month old now, but at least it doesn't crash on my minimised input program above. I'll try to minimise my program again, but this time with cvc4 nightly, for hopefully better results.

Edit 2: My minimal program above does cause one error:

$ boogie goto2_minimised.bpl /proverOpt:SOLVER=CVC4 /proverOpt:PROVER_NAME=cvc4-master
Unhandled exception. System.AggregateException: One or more errors occurred. (Index was outside the bounds of the array.) (Index was outside the bounds of the array.)
 ---> System.IndexOutOfRangeException: Index was outside the bounds of the array.
   at System.String.get_Chars(Int32 index)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.ParseId() in /home/bobe/Downloads/boogie/Source/Provers/SMTLib/SMTLibProcess.cs:line 311
   at Microsoft.Boogie.SMTLib.SMTLibProcess.ParseSExprs(Boolean top)+MoveNext() in /home/bobe/D

So it seems that for the minimal program, the broken pipe error is gone, but some other part of boogie is still not happy with its interaction with cvc4...

Here is the cvc4 version I am using.

shaz-mbp:Temp shaz$ cvc4 --version
This is CVC4 version 1.9-prerelease [git master aac53f51]

Thank you. With the nightly from the cvc4 site I was able to slim it down to the following program:

function  state(Heap: HeapType, Mask: MaskType): bool;

type Ref;
var Heap: HeapType;
// const null: Ref;
type Field A B;
// type NormalField;
type HeapType = <A, B> [Ref, Field A B]B;

type Perm = real;
type MaskType = <A, B> [Ref, Field A B]Perm;
var Mask: MaskType;

type FrameType;

type TYPEDomainType;

procedure instanceof_TYPE_TYPE#definedness(t_2: TYPEDomainType, u_1: TYPEDomainType) returns (Result: bool)
  modifies Heap, Mask;
{ }

procedure Ref___contract_unsatisfiable__t2_EncodedGlobalVariables_Integer(diz: Ref, globals: Ref, n: int) returns (sys__result: int)
  modifies Heap, Mask;
{ }

It still gives the broken pipe program, but I am unsure about its usage of floating-point or reals...

I can explain what is going on. Your Boogie program uses polymorphic features, such as:

 type HeapType = <A, B> [Ref, Field A B]B;
type MaskType = <A, B> [Ref, Field A B]Perm;

To encode such features into SMTLIB, Boogie does a type encoding which essentially embeds values of all possible types in the Boogie program to a single large type with functions (constrained by axioms) converting values back and forth. It looks like Boogie pulls in all possible types that are built into Boogie when it is collecting types for the type encoding. RoundingMode and RegEx happen to be such types. And since those types are not recognized by CVC4, you get a typing error which causes Boogie to crash.

I started to implement a monomorphization feature in Boogie which circumvents type encoding but monomorphizing a polymorphic Boogie program before handing it off to subsequent stages in the Boogie pipeline. However, my implementation does not handle the polymorphic arrays you are using in the program above.

Thank you for explaining the internals. Am I correct to assume that these appendix types can just be removed from the boogie smt2 output?

To answer my own question: I just now took the "temp.smt2" output, and removed (manually) four constants of type Regex & RoundingMode, and removed all quantifiers that mention it (again four), and now cvc4 runs with only "success" and warnings that attributes "weight" and "skolemid" are not supported. The entire file passes now, I hope that's a good sign!

It is okay for me for now if verifying a .bpl file needs some manual intervention (maybe I can automate the RegEx/RoundingMode type stripping). I have one more question: is this "temp.smt2" log outputted by boogie the complete smt2 file submitted to cvc4, or is it partial (say, the smt2 emitted up until the crash)?

And of course, it would be great if you could improve your monomorphization implementation. However, I only want to do some tests on one or two input files, so I'm not sure if it would be worth the trouble.

I suspect the file is likely to be partial. To test this hypothesis out, you could compare the file generated with Z3 with the file generated with CVC4. With Z3, you will get the full file because there is no crash.

@RustanLeino : The issue being discussed here is related to this code in TypeErasure.cs. Here, type conversion axioms are being generated for all built-in types without regard to whether these types are used in the program or not. Perhaps, this code could be strengthened. Another approach could be to declare uninterpreted types for those base types that are not supported by CVC4 when the user is using CVC4.

The file when using z3 is indeed 100 lines shorter than when using cvc4. However, I just tried feeding the z3 smt2 output to cvc4, and with minimal changes (commenting out some late (set-option) calls, and removing RegEx and RoundingMode) it seems to work, with the following output:

$ cvc4-master temp_non_cvc4.smt2 --incremental --lang=smt2.6
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
temp_non_cvc4.smt2:15.13: No set-logic command was given before this point.
temp_non_cvc4.smt2:15.13: CVC4 will make all theories available.
temp_non_cvc4.smt2:15.13: Consider setting a stricter logic for (likely) better performance.
temp_non_cvc4.smt2:15.13: To suppress this warning in the future use (set-logic ALL).
unsat
unsupported
unsupported
unsupported
unsupported
temp_non_cvc4.smt2:112.13: No set-logic command was given before this point.
temp_non_cvc4.smt2:112.13: CVC4 will make all theories available.
temp_non_cvc4.smt2:112.13: Consider setting a stricter logic for (likely) better performance.
temp_non_cvc4.smt2:112.13: To suppress this warning in the future use (set-logic ALL).
unsat

There are quite a few unsupported's, but I think those are because of the z3-specific options.

It seems I have enough to start my tests now! Only thing left to do is cross my fingers and hope this approach works for my bigger input files as well...

@bobismijnnaam : Is it fine to close this issue?

If it's easy to generate the conversion axioms only for types that are actually used, that would be nice. For example, I remember recently being surprised that there was something called regexType in what was being sent to the SMT solver.

@shazqadeer Yes, my problem was resolved by (manually with RegEx in a python script) stripping out RegexMode and RoundingMode constants. Thank you for all your assistance.

boogie-org / boogie

Using CVC4 crashes on linux with broken pipe #369