goto-instrument 5.84 crashes on simple looping program

[rod-chapman]

I am trying to verify a simple integer square root function, using contracts and loop invariants, using CBMC 5.84, running in M1 Apple macOS 13.1.1.

Here's the program:

#ifdef CBMC
#else
#define __CPROVER_assert(...)
#define __CPROVER_requires(...)
#define __CPROVER_ensures(...)
#define __CPROVER_loop_invariant(...)
#endif

int32_t isqrt(int32_t x)
__CPROVER_requires (x >= 0)
__CPROVER_ensures ((__CPROVER_function_result * __CPROVER_function_result <= x) &&
                   ((__CPROVER_function_result + 1 ) * (__CPROVER_function_result + 1) > x))
{
    int32_t upper, lower, middle;
    lower = 0;
    upper = 46341; // sqrt (MAX_INT) + 1
    while(lower + 1 != upper)
    __CPROVER_loop_invariant(lower * lower <= x)
    __CPROVER_loop_invariant(upper * upper > x)
    {
        middle = (lower + upper) / 2;
        if((middle * middle) > x)
            upper = middle;
        else
            lower = middle;
    }
    return lower;
}

Compiles fine with clang 14.0.3 and goto-cc:

rodchap@f4d4889dcf6d try % gcc -c -Wall sqrt.c
rodchap@f4d4889dcf6d try % 
rodchap@f4d4889dcf6d try % 
rodchap@f4d4889dcf6d try % goto-cc -DCMBC -o sqrt.goto sqrt.c                                                            

but crashes goto-instrument:

rodchap@f4d4889dcf6d try % goto-instrument --enforce-contract isqrt --apply-loop-contracts sqrt.goto sqrt2.goto
Reading GOTO program from 'sqrt.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Enforcing contracts
Found CFG SCC with size 8
        // 11 no location
     3: SKIP

        // 9 file sqrt.c line 26 function isqrt
        GOTO 3

        // 10 file sqrt.c line 28 function isqrt
     2: ASSIGN isqrt::1::lower := isqrt::1::middle

        // 8 file sqrt.c line 26 function isqrt
        ASSIGN isqrt::1::upper := isqrt::1::middle

        // 7 file sqrt.c line 25 function isqrt
        IF ¬(isqrt::1::middle * isqrt::1::middle > isqrt::x) THEN GOTO 2

        // 6 file sqrt.c line 24 function isqrt
        ASSIGN isqrt::1::middle := (isqrt::1::lower + isqrt::1::upper) / 2

        // 5 file sqrt.c line 20 function isqrt
     1: IF ¬(isqrt::1::lower + 1 ≠ isqrt::1::upper) THEN GOTO 4

--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20230525-15049-1i7eyc/src/goto-instrument/contracts/contracts.cpp:1139 function: check_frame_conditions_function
Condition: is_loop_free(function_body, ns, log)
Reason: Loops remain in function 'isqrt', assigns clause checking instrumentation cannot be applied.
Backtrace:
0   goto-instrument                     0x0000000100acfd4c _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 120
1   goto-instrument                     0x0000000100ad009c _Z13get_backtracev + 44
2   goto-instrument                     0x000000010069e224 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3   goto-instrument                     0x000000010069e1f0 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 0
4   goto-instrument                     0x00000001006c5acc _ZN15code_contractst31check_frame_conditions_functionERK8dstringt + 1848
5   goto-instrument                     0x00000001006c5d84 _ZN15code_contractst16enforce_contractERK8dstringt + 44
6   goto-instrument                     0x00000001006c842c _ZN15code_contractst17enforce_contractsERKNSt3__13setINS0_12basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEENS0_4lessIS7_EENS5_IS7_EEEESD_ + 136
7   goto-instrument                     0x000000010073389c _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 4284
8   goto-instrument                     0x00000001007300dc _ZN30goto_instrument_parse_optionst4doitEv + 552
9   goto-instrument                     0x0000000100af83e8 _ZN19parse_options_baset4mainEv + 180
10  goto-instrument                     0x000000010069d99c main + 48
11  dyld                                0x0000000181917f28 start + 2236

--- end invariant violation report ---
zsh: abort      goto-instrument --enforce-contract isqrt --apply-loop-contracts sqrt.goto 

[remi-delmas-3000]

Hi @rod-chapman,

the goto-instrument command line you were using invokes the old contracts system which was designed to work in two separate passes (first remove loops, second instrument function calls).

Starting from v5.84 to instrument this model you need to add an entry point (the main function) that just provides dummy arguments to the function under verification,

#include <stdlib.h>
#include <stdint.h>

#ifdef CBMC
#else
#define __CPROVER_assert(...)
#define __CPROVER_requires(...)
#define __CPROVER_ensures(...)
#define __CPROVER_loop_invariant(...)
#endif

int32_t isqrt(int32_t x)
__CPROVER_requires (x >= 0)
__CPROVER_ensures ((__CPROVER_return_value * __CPROVER_return_value <= x) &&
                   ((__CPROVER_return_value + 1 ) * (__CPROVER_return_value + 1) > x))
{
    int32_t upper, lower, middle;
    lower = 0;
    upper = 46341; // sqrt (MAX_INT) + 1
    while(lower + 1 != upper)
    __CPROVER_loop_invariant(lower * lower <= x)
    __CPROVER_loop_invariant(upper * upper > x)
    {
        middle = (lower + upper) / 2;
        if((middle * middle) > x)
            upper = middle;
        else
            lower = middle;
    }
    return lower;
}

// entry point for the analysis
int main() {
    int32_t x;
    isqrt(x);
}

Compile the code to goto like this:

goto-cc -DCBMC isqrt.c -o isqrt.o

instrument the goto binary like so (note the --dfcc main switch that activates the dynamic frames system using main as entry point)

goto-instrument --dfcc main --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt-contracts.o

Then analyse the instrumented model like so:

cbmc  --stop-on-fail --signed-overflow-check --unsigned-overflow-check --conversion-check --bounds-check --pointer-check --pointer-overflow-check --external-sat-solver cadical isqrt-contracts.o 

For contract problems cadical or kissat is recommended as SAT back end.

[rod-chapman]

I correct my contracts and added a top-level harness as you suggest. Now I get:

rodchap@f4d4889dcf6d try % goto-instrument -dfcc isqrt_test --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt2.o
Reading GOTO program from 'isqrt.o'
Failed to open 'isqrt.o'
Numeric exception : 0
rodchap@f4d4889dcf6d try % goto-instrument -dfcc isqrt_test --apply-loop-contracts --enforce-contract isqrt sqrt.o sqrt2.o 
Reading GOTO program from 'sqrt.o'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
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 'isqrt_test'
Wrapping 'isqrt' with contract 'isqrt' in CHECK mode
No assigns clause provided for loop isqrt_wrapped_for_contract_checking.0 at file sqrt.c line 20 function isqrt. The inferred set {isqrt::1::lower, isqrt::1::middle, isqrt::1::upper} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.
No decrease clause provided for loop isqrt_wrapped_for_contract_checking.0 at file sqrt.c line 20 function isqrt. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 3 targets
Removing unused functions
Dropping 67 of 67 functions (1 used)
Updating init function
--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20230525-15049-1i7eyc/src/goto-instrument/nondet_static.cpp:89 function: nondet_static
Condition: fct_entry != goto_functions.function_map.end()
Reason: Check return value
Backtrace:
0   goto-instrument                     0x000000010298fd4c _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 120
1   goto-instrument                     0x000000010299009c _Z13get_backtracev + 44
2   goto-instrument                     0x000000010255e224 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3   goto-instrument                     0x000000010255e1f0 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 0
4   goto-instrument                     0x0000000102632388 _ZL13nondet_staticRK10namespacetR15goto_functionstRK8dstringt + 1084
5   goto-instrument                     0x0000000102632d0c _Z13nondet_staticR11goto_modeltRKNSt3__13setINS1_12basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEENS1_4lessIS8_EENS6_IS8_EEEE + 1988
6   goto-instrument                     0x000000010258d148 _ZN5dfcct18reinitialize_modelEv + 176
7   goto-instrument                     0x000000010258ae78 _ZN5dfcctC2ERK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalINSt3__14pairIS5_S5_EEEEbRKNSB_3mapIS5_S5_NSB_4lessIS5_EENSB_9allocatorINSC_IS6_S5_EEEEEE24dfcc_loop_contract_modetR16message_handlertRKNSB_3setINSB_12basic_stringIcNSB_11char_traitsIcEENSK_IcEEEENSI_ISY_EENSK_ISY_EEEE + 404
8   goto-instrument                     0x000000010258ac50 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalINSt3__14pairIS4_S4_EEEEbRKNSA_3mapIS4_S4_NSA_4lessIS4_EENSA_9allocatorINSB_IS5_S4_EEEEEEbbRKNSA_3setINSA_12basic_stringIcNSA_11char_traitsIcEENSJ_IcEEEENSH_ISU_EENSJ_ISU_EEEER16message_handlert + 112
9   goto-instrument                     0x000000010258a564 _Z4dfccRK8optionstR11goto_modeltRK8dstringtRKN6nonstd13optional_lite8optionalIS4_EEbRKNSt3__13setIS4_NSD_4lessIS4_EENSD_9allocatorIS4_EEEEbbRKNSE_INSD_12basic_stringIcNSD_11char_traitsIcEENSH_IcEEEENSF_ISQ_EENSH_ISQ_EEEER16message_handlert + 304
10  goto-instrument                     0x00000001025f3bc4 _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 5092
11  goto-instrument                     0x00000001025f00dc _ZN30goto_instrument_parse_optionst4doitEv + 552
12  goto-instrument                     0x00000001029b83e8 _ZN19parse_options_baset4mainEv + 180
13  goto-instrument                     0x000000010255d99c main + 48
14  dyld                                0x000000018a073f28 start + 2236

--- end invariant violation report ---
zsh: abort      goto-instrument -dfcc isqrt_test --apply-loop-contracts --enforce-contract   

I see the note about the loop needing an assigns and a decreases contract - I will try to add those next.

[rod-chapman]

I added the decreases and assigns contracts for the loop - same crash.

[qinheping]

I tried the commands and program in @remi-delmas-3000's comments, but couldn't reproduce the crash. Here is what I got:

➜   goto-instrument --dfcc main --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt-contracts.o

Reading GOTO program from 'isqrt.o'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Loading CPROVER C library (x86_64)
Adding the cprover_contracts library (x86_64)
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'
Wrapping 'isqrt' with contract 'isqrt' in CHECK mode
No assigns clause provided for loop isqrt_wrapped_for_contract_checking.0 at file quip.c line 20 function isqrt. The inferred set {isqrt::1::lower, isqrt::1::middle, isqrt::1::upper} might be incomplete or imprecise, please provide an assigns clause if the analysis fails.
No decrease clause provided for loop isqrt_wrapped_for_contract_checking.0 at file quip.c line 20 function isqrt. Termination will not be checked.
no body for function '__CPROVER_assignable'
Instrumenting 'malloc'
Instrumenting 'free'
Specializing cprover_contracts functions for assigns clauses of at most 3 targets
Removing unused functions
Dropping 44 of 65 functions (21 used)
Updating init function
Setting entry point to main
Writing GOTO program to 'isqrt-contracts.o'

[qinheping]

The issue is in the command you use goto-instrument -dfcc isqrt_test --apply-loop-contracts --enforce-contract The function name after the flag -dfcc should be an entry function but not the function with contracts that you want to check. So it should be goto-instrument --dfcc main --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt-contracts.o

[rod-chapman]

Like this?

void isqrt_test()
{
    uint32_t x, y;
    x = nondet_uint32_t();
    __CPROVER_assume(x >= 0);
    y = isqrt(x);
    __CPROVER_assert(y * y <= x, "postcondition lower bound");
    __CPROVER_assert((y + 1) * (y + 1) <= x, "postcondition upper bound");
}

Does it really have to be called "main" ???

[qinheping]

This entry function looks good to me. No, the name of the entry function doesn't have to be main. In this case, the command should be goto-instrument --dfcc isqrt_test --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt-contracts.o

[rod-chapman]

Aha! It's OK if the top-level function is called "main", but crashes if it's called "main2" ... I'm going to need lots of these, so insisting on them all being called "main" seems a bit odd...

[rod-chapman]

Better still.. as you say... just automate the generation of the "main" wrapper so I don't have to write it at all. This is how Frama-C and SPARK do it...

[remi-delmas-3000]

I'm going to need lots of these, so insisting on them all being called "main" seems a bit odd...

They don't have to be named main, just pass the name of the entry point to the --dfcc switch

[rod-chapman]

OK... I have something that produces results now... impressively, it spots the potential overflow of "upper * upper" on line 25 if that contract were actually executed... I wasn't sure it was going to get that!

[rod-chapman]

I changed it to "main2" in the source code, AND gave "main2" on the command line. It still crashes.

[qinheping]

I confirm that goto-instrument crash with the invariant check Condition: fct_entry != goto_functions.function_map.end() failed when the name of the entry function is isqrt_test. We need to fix it.

[remi-delmas-3000]

If the entry point is named main2 and not main you have to use the switch --function main2 with goto-cc, which tells it to use main2 as entry point.

goto-cc --function main2 isqrt.c -o isqrt.o

and then pass it again to goto-instrument using the --dfcc main2 flag

goto-instrument --dfcc main2 --apply-loop-contracts --enforce-contract isqrt isqrt.o isqrt2.p

[rod-chapman]

Resolution: if the harness function is not called "main" then that name needs to be passed to goto-cc using the --function switch AND passed to goto-instrument using the --dfcc switch.

[rod-chapman]

Better error messages and/or not crashing would also be good.