New intrinsic for initialization of variables #436

rafaelsamenezes · 2021-04-29T15:04:23Z

This add the intrinsic __ESBMC_init_var(void*), which initializes the value of a given symbol with nondeterministic values, this is useful for initializing constant-sized arrays and structures.

lucasccordeiro

LGTM.

mikhailramalho · 2021-04-29T16:14:16Z

We don't actually need an intrinsic for that...

Two easier solutions:

When processing the goto program, you can add a transformation module that add nondet side effects to all decl_exprt.
During symex, you can add the nondet initialization when handling DECL instructions.

On both cases, you'll only need to add a flag to esbmc that should force such behavior (I think cbmc has a flag for that as well) . I suggest going for option 1, which is a more modular approach.

rafaelsamenezes · 2021-04-29T16:32:55Z

We don't actually need an intrinsic for that...

From what I understood, this means that every non-initialized variable is going to be nondeterministic, right?

How that would work for global arrays? For instance:

char arr[100];
int loop_init() {
        nondet_init_array();
        int a = foo();
        while (a > 1)
                a = a / 2;
        __ESBMC_assert(a == 2, "Failed as expected");

        return 0;
}

mikhailramalho · 2021-04-29T16:54:11Z

Nope, because global and static variables are initialized by the frontend. If you print the goto program of your example, you'll probably see char arr[100] = array_of(0). Em qui., 29 de abr. de 2021 às 12:33, Rafael Sá Menezes < ***@***.***> escreveu:

…

We don't actually need an intrinsic for that... From what I understood, this means that every non-initialized variable is going to be nondeterministic, right? How that would work for global arrays? For instance: char arr[100];int loop_init() { nondet_init_array(); int a = foo(); while (a > 1) a = a / 2; __ESBMC_assert(a == 2, "Failed as expected"); return 0; } — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub <#436 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKEJHZDREWFJTHIULH5IUDTLGC45ANCNFSM432CX3TQ> .

-- Mikhail Ramalho.

rafaelsamenezes · 2021-04-29T17:27:32Z

Nope, because global and static variables are initialized by the frontend.

Is there a way to mark a global array as nondet? This was the main intent of this intrinsic.

mikhailramalho · 2021-04-29T17:50:44Z

There are a couple of places where this can be implemented: 1. clang_c_convertert::get_var (when initializing global/static variables to zero) 2. static_lifetime_init (clang_c_main.cpp) 3. You can create a decl_expr in init_variable (clang_c_main.cpp) and use the modular approach I suggested in the previous email. We never created a decl_expr in init_variable before because we always expected global to be initialized as zero (except if they are marked as extern). Em qui., 29 de abr. de 2021 às 13:27, Rafael Sá Menezes < ***@***.***> escreveu:

…

Nope, because global and static variables are initialized by the frontend. Is there a way to mark a global array as nondet? This was the main intent of this intrinsic. — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub <#436 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKEJH2BFW6GQGILVACIFUDTLGJJVANCNFSM432CX3TQ> .

-- Mikhail Ramalho.

mikhailramalho · 2021-04-29T18:05:51Z

BTW, if you want the benefits of removing these loops, loop transformations would massively benefit esbmc, stuff like converting: char arr[N]; for(int i = 0; i < N; i++) arr[i] = nondet_char() to: char arr[N] = nondet_char_arr(N); Implementing this as a goto transformation and supporting some easy cases should be trivial. Em qui., 29 de abr. de 2021 às 13:50, Mikhail Ramalho Gadelha < ***@***.***> escreveu:

…

There are a couple of places where this can be implemented: 1. clang_c_convertert::get_var (when initializing global/static variables to zero) 2. static_lifetime_init (clang_c_main.cpp) 3. You can create a decl_expr in init_variable (clang_c_main.cpp) and use the modular approach I suggested in the previous email. We never created a decl_expr in init_variable before because we always expected global to be initialized as zero (except if they are marked as extern). Em qui., 29 de abr. de 2021 às 13:27, Rafael Sá Menezes < ***@***.***> escreveu: > Nope, because global and static variables are initialized by the frontend. > > Is there a way to mark a global array as nondet? This was the main intent > of this intrinsic. > > — > You are receiving this because your review was requested. > Reply to this email directly, view it on GitHub > <#436 (comment)>, or > unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAKEJH2BFW6GQGILVACIFUDTLGJJVANCNFSM432CX3TQ> > . > -- Mikhail Ramalho.

-- Mikhail Ramalho.

rafaelsamenezes · 2022-03-21T10:04:28Z

There still a need for this Intrinsic. Some users want to have a default way not only to mark a variable as nondet but to also keep making it nondet during the flow. Also this should be a part of #652

int a;
__ESBMC_init_var(a);
// do stuff with a ...
__ESBMC_init_var(a);
// do stuff with other a ...

@mikhailramalho could you look into this again?

rafaelsamenezes · 2022-03-21T10:04:28Z

There still a need for this Intrinsic. Some users want to have a default way not only to mark a variable as nondet but to also keep making it nondet during the flow. Also this should be a part of #652

int a;
__ESBMC_init_var(a);
// do stuff with a ...
__ESBMC_init_var(a);
// do stuff with other a ...

@mikhailramalho could you look into this again?

src/goto-symex/symex_main.cpp

src/clang-c-frontend/clang_c_language.cpp

mikhailramalho · 2022-03-21T13:29:51Z

There still a need for this Intrinsic. Some users want to have a default way not only to mark a variable as nondet but to also keep making it nondet during the flow. Also this should be a part of #652
int a;
__ESBMC_init_var(a);
// do stuff with a ...
__ESBMC_init_var(a);
// do stuff with other a ...
@mikhailramalho could you look into this again?

Oh, now I see! Indeed, marking a variable nondet is a bit cumbersome because of the return types of our nondet builtins. Let me just try something using macros here and I'll get back to you. My idea is something like:

#define __ESBMC_mark_nondet(var)
    __auto_type(var) nondet##var();
    var = nondet##var();

If that works, we can simply add this macro to the preprocessor!

mikhailramalho · 2022-03-21T13:55:19Z

@rafaelsamenezes, how about something like:

#include<assert.h>

#define __ESBMC_mark_nondet(var) \
    typeof(var) nondet_##var(); \
    var = nondet_##var() \

int main() {
  int v;
  v = 0;

  assert(v == 0);
  __ESBMC_mark_nondet(v);
  assert(v == 0);
}

drawbacks: we'll create one empty symbol for each variable that we mark nondet (in this example, we are creating a new nondet_v() symbol).

This needs to be expanded to prevent type conflicts, e.g., if we define a variable v in another function in the same TU with a different type the frontend will abort the verification, but we can solve that by using a location macro (LINE maybe?).

Let me know what you think, if this ends up being too complicated, I agree we should use the new builtin.

rafaelsamenezes · 2022-03-21T18:27:53Z

Let me know what you think, if this ends up being too complicated, I agree we should use the new builtin.

The main drawback for me is that it wont't work for arrays.

int main() {
  int v[10];
  v[5] = 0;

  assert(v[5] == 0);
  __ESBMC_mark_nondet(v);
  assert(v[5] == 0);
}

mikhailramalho · 2022-03-22T15:18:02Z

Let me know what you think, if this ends up being too complicated, I agree we should use the new builtin.

The main drawback for me is that it wont't work for arrays.
int main() {
  int v[10];
  v[5] = 0;

  assert(v[5] == 0);
  __ESBMC_mark_nondet(v);
  assert(v[5] == 0);
}

True :/

The only thing annoying me is the void*, can we templatefy it? Using C's extension __auto_type?

If we can't use it, I agree we should proceed with the void pointer.

rafaelsamenezes · 2022-05-05T10:07:29Z

Using C's extension __auto_type?

We can only do this for function definitions: error: a parameter list without types is only allowed in a function definition

mikhailramalho

I get the reasoning now, and I'm fine with this PR after checking the 2 comments I left.

src/goto-symex/symex_main.cpp

lucasccordeiro · 2022-05-30T10:40:04Z

@fbrausse: could you please review this PR?

fbrausse

Besides exception handling and some bikeshedding regarding the name (see comments), LGTM.

src/goto-symex/symex_main.cpp

mikhailramalho

LGTM, just one minor comment.

mikhailramalho · 2022-06-16T13:09:50Z

regression/goto-assertions/intrinsics_assert_mode_2_true/main.c

@@ -0,0 +1,5 @@
+int main() {


Maybe these belong to a separate PR?

oops. Nice catch

lucasccordeiro

LGTM.

lucasccordeiro · 2022-06-16T13:39:39Z

@rafaelsamenezes: could you please update our documentation page https://ssvlab.github.io/esbmc/documentation.html? You have created many intrinsics that are not documented for the ESBMC users.

lucasccordeiro · 2022-06-16T13:39:46Z

@rafaelsamenezes: could you please update our documentation page https://ssvlab.github.io/esbmc/documentation.html? You have created many intrinsic that are not documented anywhere.

rafaelsamenezes · 2022-06-17T08:12:38Z

@lucasccordeiro I just added it ssvlab/ssvlab.github.io#9

You have created many intrinsic that are not documented anywhere.

We definitely should define a proper way to document intrinsics.

lucasccordeiro · 2022-06-17T08:18:59Z

I just added it ssvlab/ssvlab.github.io#9

Thanks!

rafaelsamenezes requested review from mikhailramalho and lucasccordeiro April 29, 2021 15:04

lucasccordeiro approved these changes Apr 29, 2021

View reviewed changes

rafaelsamenezes force-pushed the init_var branch from 6de973d to d11e4eb Compare May 13, 2021 18:58

rafaelsamenezes force-pushed the init_var branch from 1fbf28d to b9de642 Compare March 21, 2022 10:02

rafaelsamenezes requested review from lucasccordeiro March 21, 2022 10:04

lucasccordeiro requested a review from fbrausse March 21, 2022 10:17

lucasccordeiro requested changes Mar 21, 2022

View reviewed changes

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/clang-c-frontend/clang_c_language.cpp Outdated Show resolved Hide resolved

rafaelsamenezes added the ucode label Mar 21, 2022

rafaelsamenezes added this to the ESBMC 6.10 milestone Mar 22, 2022

rafaelsamenezes force-pushed the init_var branch from a8bc420 to fe281b6 Compare May 5, 2022 10:07

mikhailramalho reviewed May 5, 2022

View reviewed changes

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/goto-symex/symex_main.cpp Show resolved Hide resolved

rafaelsamenezes mentioned this pull request May 6, 2022

Add support for __ESBMC_array_of(foo) to the frontend #59

Open

rafaelsamenezes force-pushed the init_var branch from fe281b6 to c7bc1f1 Compare May 12, 2022 08:26

rafaelsamenezes force-pushed the init_var branch from c7bc1f1 to a185bbb Compare May 28, 2022 05:07

fbrausse requested changes May 30, 2022

View reviewed changes

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/goto-symex/symex_main.cpp Outdated Show resolved Hide resolved

src/goto-symex/symex_main.cpp Show resolved Hide resolved

src/goto-symex/symex_main.cpp Show resolved Hide resolved

rafaelsamenezes force-pushed the init_var branch from 7989507 to 877b15d Compare May 31, 2022 13:19

rafaelsamenezes and others added 5 commits June 16, 2022 13:21

added esbmc_init_var intrinsic

6e5ef80

added esbmc_init_var test cases

2e54649

[msg] replaced cerr with msg.error

a5942e1

[init_var] improved assertion condition

a91526e

[init_object] renamed init_var into init_object

8a3e7b4

rafaelsamenezes force-pushed the init_var branch from 020142e to 8a3e7b4 Compare June 16, 2022 12:21

rafaelsamenezes requested review from fbrausse and mikhailramalho June 16, 2022 12:21

mikhailramalho approved these changes Jun 16, 2022

View reviewed changes

lucasccordeiro approved these changes Jun 16, 2022

View reviewed changes

fixup! [init_object] renamed init_var into init_object

3a3948d

fixup! fixup! [init_object] renamed init_var into init_object

ba6afbb

rafaelsamenezes merged commit 2761907 into master Jun 17, 2022

rafaelsamenezes deleted the init_var branch June 17, 2022 10:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New intrinsic for initialization of variables #436

New intrinsic for initialization of variables #436

rafaelsamenezes commented Apr 29, 2021

lucasccordeiro left a comment

mikhailramalho commented Apr 29, 2021

rafaelsamenezes commented Apr 29, 2021

mikhailramalho commented Apr 29, 2021 via email

rafaelsamenezes commented Apr 29, 2021

mikhailramalho commented Apr 29, 2021 via email

mikhailramalho commented Apr 29, 2021 via email

rafaelsamenezes commented Mar 21, 2022

rafaelsamenezes commented Mar 21, 2022

mikhailramalho commented Mar 21, 2022

mikhailramalho commented Mar 21, 2022

rafaelsamenezes commented Mar 21, 2022

mikhailramalho commented Mar 22, 2022

rafaelsamenezes commented May 5, 2022

mikhailramalho left a comment

lucasccordeiro commented May 30, 2022

fbrausse left a comment

mikhailramalho left a comment

mikhailramalho Jun 16, 2022

rafaelsamenezes Jun 16, 2022

lucasccordeiro left a comment

lucasccordeiro commented Jun 16, 2022

lucasccordeiro commented Jun 16, 2022

rafaelsamenezes commented Jun 17, 2022

lucasccordeiro commented Jun 17, 2022

New intrinsic for initialization of variables #436

New intrinsic for initialization of variables #436

Conversation

rafaelsamenezes commented Apr 29, 2021

lucasccordeiro left a comment

Choose a reason for hiding this comment

mikhailramalho commented Apr 29, 2021

rafaelsamenezes commented Apr 29, 2021

mikhailramalho commented Apr 29, 2021 via email

rafaelsamenezes commented Apr 29, 2021

mikhailramalho commented Apr 29, 2021 via email

mikhailramalho commented Apr 29, 2021 via email

rafaelsamenezes commented Mar 21, 2022

rafaelsamenezes commented Mar 21, 2022

mikhailramalho commented Mar 21, 2022

mikhailramalho commented Mar 21, 2022

rafaelsamenezes commented Mar 21, 2022

mikhailramalho commented Mar 22, 2022

rafaelsamenezes commented May 5, 2022

mikhailramalho left a comment

Choose a reason for hiding this comment

lucasccordeiro commented May 30, 2022

fbrausse left a comment

Choose a reason for hiding this comment

mikhailramalho left a comment

Choose a reason for hiding this comment

mikhailramalho Jun 16, 2022

Choose a reason for hiding this comment

rafaelsamenezes Jun 16, 2022

Choose a reason for hiding this comment

lucasccordeiro left a comment

Choose a reason for hiding this comment

lucasccordeiro commented Jun 16, 2022

lucasccordeiro commented Jun 16, 2022

rafaelsamenezes commented Jun 17, 2022

lucasccordeiro commented Jun 17, 2022