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

Crash due to failed ABC assertion #233

Closed
TomMD opened this issue Nov 8, 2017 · 3 comments
Closed

Crash due to failed ABC assertion #233

TomMD opened this issue Nov 8, 2017 · 3 comments
Assignees
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@TomMD
Copy link
Contributor

TomMD commented Nov 8, 2017

I can produce a crash:

saw: src/sat/bsat/satClause.h:306: Sat_MemAppend: Assertion `nInts
+ 3 < (1 << p->nPageSize)' failed.

Using a prng test:

// A non-cryptographic PRNG from http://burtleburtle.net/bob/rand/smallprng.html

typedef unsigned long int  u4;
typedef struct ranctx { u4 a; u4 b; u4 c; u4 d; } ranctx;
static u4 ranval( ranctx *x );
static void raninit( ranctx *x, u4 seed );

#define NR_CMP 1024

// Different seeds result in different output.
int test(u4 seed1, u4 seed2)
{
    ranctx a,b;
    int i;
    int eq = 1;
    raninit(&a,seed1); raninit(&b,seed2);
    for(i = 0 ; i < NR_CMP ; i++) {
        eq &= ranval(&a) == ranval(&b);
    }
    return (seed1 == seed2) || !eq;
}

#define rot(x,k) (((x)<<(k))|((x)>>(32-(k))))
static u4 ranval( ranctx *x ) {
    u4 e = x->a - rot(x->b, 27);
    x->a = x->b ^ rot(x->c, 17);
    x->b = x->c + x->d;
    x->c = x->d + e;
    x->d = e + x->a;
    return x->d;
}

static void raninit( ranctx *x, u4 seed ) {
    u4 i;
    x->a = 0xf1ea5eed, x->b = x->c = x->d = seed;
    for (i=0; i<20; ++i) {
        (void)ranval(x);
    }
}

And saw script:

v1 <- llvm_load_module "final_master_master.bc";
let v2 =
    do {
        v3 <- crucible_fresh_var "args[0]" (llvm_int 64);
        let v4 =
            crucible_term v3;
        v5 <- crucible_fresh_var "args[1]" (llvm_int 64);
        let v6 =
            crucible_term v5;
        crucible_execute_func [v4, v6];
        crucible_return (crucible_term {{ (1 : [32]) }});
    };
crucible_llvm_verify v1 "test" [] true v2 abc;
@atomb atomb added this to the 0.3 milestone Feb 5, 2018
@atomb atomb self-assigned this Feb 9, 2018
@atomb atomb added the type: bug Issues reporting bugs or unexpected/unwanted behavior label Jun 13, 2018
@atomb
Copy link
Contributor

atomb commented Jul 18, 2018

How long did you have to run it before it crashed? I'm trying a new ABC version, and it hasn't crashed yet, but it's still running. Do you think that this problem should be solvable?

@atomb atomb removed this from the 0.3 milestone Apr 2, 2019
@atomb
Copy link
Contributor

atomb commented Apr 2, 2019

I'm unable to reproduce the crash, so I'm removing the milestone.

@atomb atomb added the maybe fixed Issues where there's reason to think they might be fixed but that still requires confirmation label Apr 12, 2019
@atomb atomb added this to the 1.0 milestone Jun 4, 2019
@atomb atomb modified the milestones: 1.0, 0.4 Oct 1, 2019
@atomb atomb modified the milestones: 0.4, 1.0 Oct 16, 2019
@atomb atomb modified the milestones: 0.5, 0.6 Mar 24, 2020
@atomb atomb modified the milestones: 0.6, 0.7 Aug 6, 2020
@atomb atomb modified the milestones: 0.7, Remove abcBridge Oct 16, 2020
@atomb
Copy link
Contributor

atomb commented Jul 22, 2021

The code this refers to no longer exists.

@atomb atomb closed this as completed Jul 22, 2021
@sauclovian-g sauclovian-g removed the maybe fixed Issues where there's reason to think they might be fixed but that still requires confirmation label Oct 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

3 participants