From 4c2c27dbd7ff2ef7ff9557863584bf77ce180907 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 8 Feb 2022 21:32:54 +0000 Subject: [PATCH] Single-path symex must not fail an invariant when verification succeeds Single-path symex takes a best-effort approach to produce a proof by using the symex equation of that path that was last visited. This, however, failed an invariant when trying to access the equation that had already been popped from the worklist. Leave the last equation in place to avoid this problem. --- regression/cbmc/Address_of1/test.desc | 6 +++++- src/goto-checker/single_path_symex_checker.cpp | 8 +++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/Address_of1/test.desc b/regression/cbmc/Address_of1/test.desc index 9efefbc7362..7cf1c8ac5b3 100644 --- a/regression/cbmc/Address_of1/test.desc +++ b/regression/cbmc/Address_of1/test.desc @@ -1,8 +1,12 @@ CORE main.c - +--stop-on-fail ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +Adding "--stop-on-fail" should not make a difference for successful +verification, but previously caused an invariant failure when running CBMC with +"--paths." diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index d87b18a014a..13f4ce14acd 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -75,6 +75,10 @@ operator()(propertiest &properties) return result; } + // leave the last worklist item in place for the benefit of output_proof + if(worklist->size() == 1) + break; + worklist->pop(); } @@ -83,7 +87,7 @@ operator()(propertiest &properties) final_update_properties(properties, result.updated_properties); - // Worklist is empty: we are done. + // Worklist just has the last element left: we are done. return result; } @@ -182,6 +186,8 @@ void single_path_symex_checkert::output_error_witness( void single_path_symex_checkert::output_proof() { // This is incorrect, but the best we can do at the moment. + // operator()(propertiest &properties) leaves in place the last worklist item + // just for this purpose. const path_storaget::patht &resume = worklist->peek(); output_graphml(resume.equation, ns, options); }