verifying a program with struct without field-sensitivity in Cprover5.12

[Sepideh Asadi]

Dear CBMC team, I have a question.

We have a BMC tool relies on Cprover5.12 framework in generating GOTO-programs and SSA encoding. For our application we'd need to avoid constant-propagation due to preserving local variables inside functions.  When verifying a program with struct  we would like to disable field-sensitive L2 SSA renaming and constant propagation.

I tried to disable constant-propagation   options.set_option("propagation", false); but didn't resolve the issue.

I am wondering is there a way to disable "field-sensitive level-2 SSA renaming" in Cprover5.12 framework and keep the old style of handling structs?


P.S. Previously, our BMC tool with CPROVER 5.10 worked fine in verifying the following program with struct, but after upgrading our front-end to Cprover5.12 we hit a failure in Invariant check:

 Reason: value_sett::assign types should match 

rhs.type(): struct_tag but lhs.type(): struct

C example: 

struct S{
int x;
int y;
};

struct S s;


f(){
s.x = 0;
}

void main(){
s.x = 1;
s.y = 2;
f();
assert(s.x == 0);
}

[Martin Nyx Brain]

On Wed, 2021-02-10 at 17:33 -0800, Sepideh Asadi wrote:
>
> Dear CBMC team, I have a question.
>
> We have a BMC tool relies on Cprover5.12 framework in generating
> GOTO-programs and SSA encoding.

Cool! Is this HiFrog or something else?

> For our application we'd need to avoid
> constant-propagation due to preserving local variables inside
> functions.
> When verifying a program with struct we would like to
> disable field-sensitive L2 SSA renaming and constant propagation.
>
> I tried to disable constant-

> propagation options.set_option("propagation",

> false); but didn't resolve the issue.

https://github.com/diffblue/cbmc/blob/3b406c604ee0513228cb8a02900d6347d1bfe463/src/goto-symex/symex_main.cpp#L39

This should work. I tried with cbmc --no-propagation and it seemed to
disable it. You might also be interested in the "simplify" option
which will preserve even more expression structure (but at some cost).

> I am wondering is there a way to disable "field-sensitive level-2
> SSA
> renaming" in Cprover5.12 framework and keep the old style of
> handling
> structs?

The field sensitivity code isn't mine so I don't know for sure (ask
Michael) but I don't think there is an optiont setting to remove it.
But, if I understand correctly it works by renaming so the old handling
should still be possible if you just skip the renaming. Try flipping

https://github.com/diffblue/cbmc/blob/3b406c604ee0513228cb8a02900d6347d1bfe463/src/goto-symex/field_sensitivity.cpp#L19

or

https://github.com/diffblue/cbmc/blob/3b406c604ee0513228cb8a02900d6347d1bfe463/src/goto-symex/field_sensitivity.h#L155

If that works then there should probably be a patch to have an optiont
setting to do this and some test cases with one program and two .desc
files, with and without field sensitivity. That should stop the older
functionality bit-rotting.

> P.S. Previously, our BMC tool with CPROVER 5.10 worked fine in
> verifying
> the following program with struct, but after upgrading our front-end
> to
> Cprover5.12 we hit a failure in Invariant check:
>
> Reason: value_sett::assign types should match
>
> rhs.type(): struct_tag but lhs.type(): struct
>
> C example:
> struct S{
> int x;
> int y;
> };
>
> struct S s;
>
>
> f(){
> s.x = 0;
> }
>
> void main(){
> s.x = 1;
> s.y = 2;
> f();
> assert(s.x == 0);
> }

Yeah; that would sound like an issue with struct renaming.

Let us know how you get on and we can investigate further if needed.

Cheers,
- Martin

[Martin Nyx Brain]

More generally, if you are building on CProver, then maybe we (for some
scoping of we) should look at better / more automated ways of making
sure that changes to the develop branch don't break your code.

Cheers,
- Martin

[Sepideh Asadi]

Is this HiFrog

Yes! HiFrog and our tool at USI Lugano called UpProver for incrementally verifying program revisions.

Many thanks Martin for the tips! I tried —no-propagation option , as well as commenting #define ENABLE_ARRAY_FIELD_SENSITIVITY and setting run_apply = false

 but  our tool hits the same invariant check in the struct example below.

 more automated ways of making
sure that changes to the develop branch don't break your code.

Yes, it would make our life much easier if Cprover maintains the backward compatibility : )

I CC’de Michele and Chris, I would really appreciate if they could give me some hints how to deactivate field-sensitive L2 renaming in struct. 

Best Regards,
Sepideh

We have a BMC tool relies on Cprover5.12 framework in generating GOTO-programs and SSA encoding. For our application we'd need to avoid constant-propagation due to preserving local variables inside functions.  When verifying a program with struct  we would like to disable field-sensitive L2 SSA renaming and constant propagation.

I tried to disable constant-propagation   options.set_option("propagation", false); but didn't resolve the issue.

I am wondering is there a way to disable "field-sensitive level-2 SSA renaming" in Cprover5.12 framework and keep the old style of handling structs?

P.S. Previously, our BMC tool with CPROVER 5.10 worked fine in verifying the following program with struct, but after upgrading our front-end to Cprover5.12 we hit a failure in Invariant check:

 Reason: value_sett::assign types should match 

rhs.type(): struct_tag but lhs.type(): struct

C example: 

struct S{
int x;
int y;
};

struct S s;


f(){
s.x = 0;
}

void main(){
s.x = 1;
s.y = 2;
f();
assert(s.x == 0);
}

Best Regards,
Sepideh

[Martin Nyx Brain]

On Thu, 2021-02-11 at 17:17 +0100, Sepideh Asadi wrote:
> > Is this HiFrog
> Yes! HiFrog and our tool at USI Lugano called UpProver for
> incrementally verifying program revisions.

Awesome! ( I figure you know about goto-diff? )

> Many thanks Martin for the tips! I tried —no-propagation option , as
> well as commenting #define ENABLE_ARRAY_FIELD_SENSITIVITY and setting
> run_apply = false
> but our tool hits the same invariant check in the struct example
> below.

Sorry to hear this. Do you know the last revision where this works?

> > more automated ways of making
> > sure that changes to the develop branch don't break your code.
>
> Yes, it would make our life much easier if Cprover maintains the
> backward compatibility : )

Understood but backwards compatibility of what? There is an effort to
preserve backwards compatibility of tool functionality and command-line
interface but with internal interfaces it is less clear which should be
maintained and how long. Some things have been marked DEPRECATED and
left for a while before removal. However without some visibility of
external tools (which is a social problem really -- CProver could do a
lot better at communication between developers) it's hard to know what
should stay.

Possible approaches:

*. Merge your tools into CProver so that maintenance of functionality
is the same as other tools. This is probably the technically most
simple but by far the most complicated socially.

*. Add CI passes to CProver that build your tools. It is not clear
who's problem breaks would be. If it is the author of the PR's
responsibility / they are blocking CI checks then it is a more
complicated and error prone version of the previous option.

*. Add regression or unit tests to CProver for the functionality you
need along with comments saying "before you change this, have a chat
with...". It might be hard to capture everything you need though.

*. Add a CI or scheduled job to build your system(s) with the latest
CProver develop branch so that you get timely notification of any
problems.

> I CC’de Michele and Chris, I would really appreciate if they could
> give me some hints how to deactivate field-sensitive L2 renaming in
> struct.

I saw the issue raised and I will follow up there.

Cheers,
- Martin

[Sepideh Asadi]

Thanks Martin for the suggestions! we’ll think about them.

I figure you know about goto-diff

Yes, I am aware of the goto-diff directory but I have n’t had a change to check that part of the code in CBMC and use it.

Are there any documentation/publication for goto-diff in CBMC? 

In UpProver and its predecessor EVolCheck, we implemented a diff utility that compares two versions of a program function-wise and marks the changed functions. 

Then proceeds with the incremental verification of the changed functions using the info of the previous version.

For benchmarking we use ‘regression’ category in SV-COMP. If your team happen to know any other C benchmarks with revisions would be very interesting to challenge our tool.

Best Regards,
Sepideh

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/b25f46f31465dcec673d09bb5606d5e1cf06f2fb.camel%40cs.ox.ac.uk.

[Martin Nyx Brain]

On Sun, 2021-02-14 at 17:33 +0100, Sepideh Asadi wrote:
> Thanks Martin for the suggestions! we’ll think about them.

I am working on another out-of-tree tool based on CPROVER so I am
interested in how others manage this kind of problem.

> > I figure you know about goto-diff
> Yes, I am aware of the goto-diff directory but I have n’t had a
> change to check that part of the code in CBMC and use it.
> Are there any documentation/publication for goto-diff in CBMC?

I am not aware of any. Peter Schrammel is the person to ask.

> In UpProver and its predecessor EVolCheck, we implemented a diff
> utility that compares two versions of a program function-wise and
> marks the changed functions.
> Then proceeds with the incremental verification of the changed
> functions using the info of the previous version.

I believe that goto-diff does some of this.

> For benchmarking we use ‘regression’ category in SV-COMP. If your
> team happen to know any other C benchmarks with revisions would be
> very interesting to challenge our tool.

It's not quite what you are looking for but Hempitera might be of
interest:

https://export.arxiv.org/pdf/1805.03450

Cheers,
- Martin