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.

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

Suboptimal CFG reconstruction #523

Open
sonmarcho opened this issue Jan 14, 2025 · 2 comments
Open

Suboptimal CFG reconstruction #523

sonmarcho opened this issue Jan 14, 2025 · 2 comments
Labels
C-bug A bug in charon

Comments

@sonmarcho
Copy link
Member

sonmarcho commented Jan 14, 2025

A few more minimized examples where the CFG reconstruction is sub-optimal:

fn f1(b : bool, c : bool)
{
    let a;
    
    if b
    {
        a = 1;
        assert!( a == 1 ); // The presence of this assert triggers the issue
    }
    else if c
    {
        return;
    }
}

which gets reconstructed as:

fn f1(bool b, bool c)
{
  if (!b)
  {
    if (!c)
    {
      return;
    }
    return;
  }
  a = 1;
  assert (a == 1);
}

And:

fn f2(b : bool, c : u32)
{
    let mut a = 0;
    while
    {
        if b
        {
            a = 1;
        }
        c > a
    } {}
}

which gets reconstructed as:

fn f2(bool b, uint32_t c)
{
  let a = 0;
  loop
  {
    if (b)
    {
      a = 1;
      if (!(c > a))
      {
        break;
      }
    }
    else if (!(c > a))
    {
      break;
    }
  }
}
@sonmarcho sonmarcho added the C-bug A bug in charon label Jan 14, 2025
@Nadrieril Nadrieril changed the title Invalid CFG reconstruction Subptop CFG reconstruction Jan 14, 2025
@Nadrieril Nadrieril changed the title Subptop CFG reconstruction Suboptimal CFG reconstruction Jan 14, 2025
@Nadrieril
Copy link
Member

Could you link the other open issues we have on the topic?

@sonmarcho
Copy link
Member Author

sonmarcho commented Jan 14, 2025

The other issues are:
#507
#297

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-bug A bug in charon
Projects
None yet
Development

No branches or pull requests

2 participants