Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[SMT] fix pointer typecast for byte update #2197

Merged
merged 4 commits into from
Dec 16, 2024
Merged

[SMT] fix pointer typecast for byte update #2197

merged 4 commits into from
Dec 16, 2024

Conversation

XLiZHI
Copy link
Collaborator

@XLiZHI XLiZHI commented Dec 15, 2024 •
edited
Loading

For this code:

int some_var;

int main()
{
  void *bar;
  char *ptr = &bar;
  ptr[0] = nondet_char();
  
  __ESBMC_assert(bar != &some_var, "");
}

Nondet pointer breaks byte update, see details: #2153 (comment)

ASSIGNMENT ()
bar?1!0&0#1 == nondet_symbol(symex::nondet0)

Thread 0 file main4.c line 7 column 12 function main
ASSIGNMENT ()
bar?1!0&0#2 == byte_update_little_endian(bar?1!0&0#1, 0, (unsigned char)(nondet_symbol(symex::nondet1)))

We take into account the constraint, the counterexample to bar != &some_var is bar == &some_var, i.e.
byte_update_little_endian(bar, 0, symex::nondet1) == &some_var

====> bar = &some_var

@XLiZHI XLiZHI linked an issue Dec 15, 2024 that may be closed by this pull request
[firmware] incorrect true #2153
Open
lucasccordeiro
lucasccordeiro approved these changes Dec 15, 2024
View reviewed changes
Copy link
Contributor

@lucasccordeiro lucasccordeiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for submitting this PR, @XLiZHI.

I have added a few comments to clarify the code.

Can you also run this PR over the SV-COMP benchmarks?

src/solvers/smt/smt_casts.cpp Outdated Show resolved Hide resolved
src/solvers/smt/smt_casts.cpp Show resolved Hide resolved
src/solvers/smt/smt_casts.cpp Show resolved Hide resolved
src/solvers/smt/smt_casts.cpp Show resolved Hide resolved
@XLiZHI
Copy link
Collaborator Author

XLiZHI commented Dec 15, 2024 •
edited
Loading

Master:

Statistics:          33569 Files
  correct:           18480
    correct true:    11150
    correct false:    7330
  incorrect:            83
    incorrect true:     62
    incorrect false:    21
  unknown:           15006
  Score:             27310 (max: 55885)
https://github.com/esbmc/esbmc/actions/runs/12295397375/job/34313090912

This PR:

Statistics:          33569 Files
  correct:           18489
    correct true:    11158
    correct false:    7331
  incorrect:            81
    incorrect true:     61
    incorrect false:    20
  unknown:           14999
  Score:             27375 (max: 55885)
https://github.com/esbmc/esbmc/actions/runs/12339875558

lucasccordeiro
lucasccordeiro approved these changes Dec 15, 2024
View reviewed changes
Copy link
Contributor

@lucasccordeiro lucasccordeiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Many thanks, @XLiZHI.

LGTM.

Let's check for the SV-COMP results.

@XLiZHI XLiZHI marked this pull request as ready for review December 15, 2024 17:11
@lucasccordeiro
Copy link
Contributor

@XLiZHI: I have just checked this patch on the code:

Command-line: $ esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check tdg_servtd_wr__cover__success_havoc_memory.i --64 --witness-output witness.graphml --enable-unreachability-intrinsic --no-pointer-check --interval-analysis --no-bounds-check --error-label ERROR --goto-unwind --unlimited-goto-unwind --k-induction --max-inductive-step 3

Program: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i?ref_type=heads

c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i

ESBMC still gives incorrect true.

The reduced version provided by @rafaelsamenezes misses something else in this example.

We'll have to investigate it further as part of another PR.

@XLiZHI
Copy link
Collaborator Author

XLiZHI commented Dec 15, 2024

@XLiZHI: I have just checked this patch on the code:

Command-line: $ esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check tdg_servtd_wr__cover__success_havoc_memory.i --64 --witness-output witness.graphml --enable-unreachability-intrinsic --no-pointer-check --interval-analysis --no-bounds-check --error-label ERROR --goto-unwind --unlimited-goto-unwind --k-induction --max-inductive-step 3

Program: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i?ref_type=heads

c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i

ESBMC still gives incorrect true.

The reduced version provided by @rafaelsamenezes misses something else in this example.

We'll have to investigate it further as part of another PR.

I did a quick check and here's the problem:

void init_loop(void *base, unsigned int size) {
  for (int i = 0; i < 1 ; i++) {
    *((char *)base + i) = nondet_char();
  }
}

It's SSA:

ASSIGNMENT ()
bug?1!0&0#2 == ( struct my_obj { void * bar; })(byte_update_little_endian((unsigned long int)bug?1!0&0#1, 0, (unsigned char)(nondet_symbol(symex::nondet1))))

I think it should be:

Thread 0 file main3.c line 5 column 27 function init_loop
ASSIGNMENT ()
bug?1!0&0#2 == (bug?1!0&0#1 WITH [bar:=byte_update_little_endian(bug?1!0&0#1.bar, 0, (unsigned char)(nondet_symbol(symex::nondet1)))])

@lucasccordeiro lucasccordeiro merged commit 110986f into master Dec 16, 2024
10 checks passed
@lucasccordeiro lucasccordeiro deleted the XL/firmware branch December 16, 2024 07:47
@lucasccordeiro
Copy link
Contributor

Thanks for submitting this PR, @XLiZHI.

Can I ask you to submit a separate PR to handle the Intel benchmark case?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lucasccordeiro lucasccordeiro lucasccordeiro approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[firmware] incorrect true
2 participants
@XLiZHI @lucasccordeiro