Comments (8)
qinheping
commented on June 28, 2024
UPDATE:
If there are two expressions
forall x. e1 and forall x. e1 => e2, the first expression will be correctly converted to
(define-fun B1 () Bool (forall x. e1))
But the second expression will be converted to
(define-fun B2 () Bool (=> (and true B1) e2))
where e2 is no more quantified.
The quantified scope is not correctly handled.
from cbmc.
rod-chapman
commented on June 28, 2024
Do you have a simple, reproducible test case? I hope so! Please add and commit that first, so reviewers can see what's going wrong, then see the subsequent commits that correct the behaviour.
from cbmc.
qinheping
commented on June 28, 2024
Yes, here is a small test case I reproduced the issue with:
#include <assert.h>
#include <stdbool.h>
#define N 16
void main()
{
int a[N];
a[10] = 0;
bool flag = true;
for(int j = 0; j < N; ++j)
__CPROVER_loop_invariant(j <= N)
{
for(int i = 0; i < N; ++i)
__CPROVER_assigns(i, __CPROVER_object_whole(a))
__CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
int k;
(0 <= k && k <= N) ==> (k<i ==> a[k] == 1)
})
{
a[i] = 1;
}
}
assert(a[10] == 1);
}Running
goto-instrument --dfcc main --apply-loop-contracts a.out b.out
cbmc b.out --smt2
will get the error message
SMT2 solver returned error message:
"line 10912 column 208: unknown constant main::tmp_cc$0!0@2#0"
from cbmc.
qinheping
commented on June 28, 2024
In the outfile produced with the --outfile flag, we can see that
(declare-fun B1526 () Bool)
(assert (= B1526 (and (bvsge |main::1::1::1::1::i!0@1#4| (_ bv0 32)) (not (bvsge |main::1::1::1::1::i!0@1#4| (_ bv17 32)))
(forall ((|main::tmp_cc$0!0@2#0| (_ BitVec 32))) (or (not (bvsge |main::tmp_cc$0!0@2#0| (_ bv0 32))) (bvsge |main::tmp_cc$0!0@2#0| (_ bv17 32)) (bvsge |main::tmp_cc$0!0@2#0| |main::1::1::1::1::i!0@1#4|) (= (select array.54 ((_ sign_extend 32) |main::tmp_cc$0!0@2#0|)) (_ bv1 32)))))))
...
; convert
; Converting var_no 1592 with expr ID of =>
(define-fun B1592 () Bool (=> (and true B1526 B1527 B1528)
(=> |goto_symex::&92;guard#10|
(or (not (bvsge |main::1::1::1::1::i!0@2#4| (_ bv0 32)))
(bvsge |main::1::1::1::1::i!0@2#4| (_ bv17 32))
(not (bvsge |main::tmp_cc$0!0@2#0| (_ bv0 32))) (bvsge |main::tmp_cc$0!0@2#0| (_ bv17 32)) (bvsge |main::tmp_cc$0!0@2#0| |main::1::1::1::1::i!0@2#4|) (bvsge (bvmul ((_ sign_extend 32) |main::tmp_cc$0!0@2#0|) (_ bv4 64)) (_ bv0 64))))))
The variable main::tmp_cc$0!0@2#0 is correctly quantified in B1592 but not in B1526.
from cbmc.
rod-chapman
commented on June 28, 2024
I tried to reproduce that. I just copied the text above into a file called 8329.c, then:
rodchap@f4d4889dcf6d bugs % goto-cc -c -o a.goto 8329.c
rodchap@f4d4889dcf6d bugs % goto-instrument --dfcc main --apply-loop-contracts a.goto b.goto
Reading GOTO program from 'a.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Loading CPROVER C library (arm64)
Adding the cprover_contracts library (arm64)
file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value
symbol '__CPROVER_alloca_object' already has an initial value
symbol '__CPROVER_new_object' already has an initial value
file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value
Instrumenting harness function 'main'
No decrease clause provided for loop main.0 at file 8329.c line 14 function main. Termination will not be checked.
No assigns clause provided for loop main.1 at file 8329.c line 11 function main. The inferred set {side_effect statement="function_call"(__CPROVER_object_whole, arguments(address_of(main::1::a))), main::1::1::j} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.
No decrease clause provided for loop main.1 at file 8329.c line 11 function main. Termination will not be checked.
file 8329.c line 15 function main: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
file <built-in-additions> line 32: no body for function '__CPROVER_object_whole'
no body for function '__CPROVER_assignable'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 2 targets
Removing unused functions
Updating init function
--- begin invariant violation report ---
Invariant check failed
File: /Users/rodchap/Desktop/rod/tools/src/cbmc/src/goto-instrument/nondet_static.cpp:90 function: nondet_static
Condition: fct_entry != goto_model.goto_functions.function_map.end()
Reason: Check return value
Backtrace:
0 goto-instrument 0x00000001028c4968 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 124
1 goto-instrument 0x00000001028c4df4 _Z13get_backtracev + 160
2 goto-instrument 0x00000001023a90c8 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3 goto-instrument 0x00000001023a9094 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 0
4 goto-instrument 0x00000001024c6b80 _ZL13nondet_staticRK10namespacetR11goto_modeltRK8dstringt + 1064
5 goto-instrument 0x00000001024c75a8 _Z13nondet_staticR11goto_modeltRKNSt3__13setINS1_12basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEENS1_4lessIS8_EENS6_IS8_EEEE + 2324
6 goto-instrument 0x000000010240a228 _ZN5dfcct18reinitialize_modelEv + 180
7 goto-instrument 0x0000000102407730 _ZN5dfcctC2ERK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalINS8_4pairIS5_S5_EEEEbRKNS8_3mapIS5_S5_NS8_4lessIS5_EENS8_9allocatorINSA_IS6_S5_EEEEEE24dfcc_loop_contract_modetR16message_handlertRKNS8_3setINS8_12basic_stringIcNS8_11char_traitsIcEENSI_IcEEEENSG_ISW_EENSI_ISW_EEEE + 552
8 goto-instrument 0x0000000102406d70 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKNSt3__18optionalIS4_EEbRKNS7_3setIS4_NS7_4lessIS4_EENS7_9allocatorIS4_EEEEbbRKNSC_INS7_12basic_stringIcNS7_11char_traitsIcEENSF_IcEEEENSD_ISO_EENSF_ISO_EEEER16message_handlert + 384
9 goto-instrument 0x00000001024953b4 _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 8080
10 goto-instrument 0x0000000102490b3c _ZN30goto_instrument_parse_optionst4doitEv + 660
11 goto-instrument 0x00000001028ee6c0 _ZN19parse_options_baset4mainEv + 180
12 goto-instrument 0x00000001023a8858 main + 40
13 dyld 0x0000000187a8ff28 start + 2236
--- end invariant violation report ---
I'm running CBMC 6.0.0 on macOS...
from cbmc.
rod-chapman
commented on June 28, 2024
Anyway - please add that test case below https://github.com/diffblue/cbmc/tree/develop/regression
somewhere, so the difference in behaviour can be reviewed later as part of this Issue/PR.
from cbmc.
qinheping
commented on June 28, 2024
A test added in #8361.
from cbmc.
qinheping
commented on June 28, 2024
#8361 resolves this issue of unknown constant. But on your example, I encountered the issue of CBMC not terminating again, which is similar to #8326 and #8301 .
from cbmc.
Related Issues (20)
- --refine imprecision
- CBMC 5.95.1 crashes on proof of simple array equality function HOT 7
- Inconsistency in the results by different SMT solvers HOT 2
- CBMC wavefront does not terminate on simple decreases clause in loop HOT 7
- Incorrect result for --external-sat-solver z3 option HOT 2
- CBMC 6.0.0-alpha crashes on array copy function HOT 1
- CBMC fails to co-exist with GCC 13 HOT 10
- [QUESTION] Conversion Error HOT 4
- Generating GOTO-programs as front-end to other tool HOT 2
- String abstraction crash on very simple C program
- Zero-termination assertion fails on zero-terminated strings
- CBMC contracts crash when dynamic allocation is not in the harness. HOT 5
- Non-termination of proof on simple array copy example HOT 2
- Opened in error - apologies. Please delete or close.
- CBMC-6.0.0 fails if local variable name overloads name of quantified variable in contract
- no bounds check assertion HOT 1
- Unwind Issue: How to make a loop inductive? HOT 25
- aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE
- goto-cc 6.0.0 fails compilation of s2n-tls unit on Linux, but works on macOS HOT 10
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from cbmc.