Are there any methods provided by haybale for constraining certain variables?

[Just1ceP4rtn3r]

e.g.

int foo(struct Context* context) {
  //assert(context->x == 1);
  if (context->x == 0)
     return 0;
  
  if (context->y < 0)
     return -1;
  else 
     return 1;
} 

So I just want to take "context->y" as a symbolic value and restrict "context->x" to 1. Can we reach this but not modify the origin LLVM IR ?

[Just1ceP4rtn3r]

I found that symex_function provides a parameter named "params: Option<Vec>". But how to set some initial value for a pointer of struct?

[cdisselkoen]

One way to do this is:

1. use symex_function with params=None to get an ExecutionManager
2. use ExecutionManager::mut_state() to access the State, from which you can allocate some bits representing the struct Context you want to pass in, receiving a BV pointer to the new allocation
3. constrain the x field of that allocation to be 1
4. finally, use ExecutionManager::param_bvs() to access the context parameter, and then constrain it to be equal to the pointer received in step 2.

For a more thorough solution, you can take a look at what pitchfork built on top of haybale, in particular pitchfork's AbstractData.

[cdisselkoen]

You can do

let context_inmem = mutState.read(&contextPtr, struct_size_bits).unwrap();
context_inmem._eq(&context).assert().unwrap();

Or, even better, just constrain the x field of context_inmem directly, without creating a separate BV:

let context = mutState.read(&contextPtr, struct_size_bits).unwrap();  // instead of BV::new
// use `context` as in the above comment

[Just1ceP4rtn3r]

Thanks, I see now what you mean!
But the struct Context is more complex in the real code. For example, Haybale will throw errors Error::NullPointerDereference when access context->next->a because we didn't allocate next:

struct Context{
    struct Context * next;
    char a;
    char b;
    char x;
    char y;
}

Is necessary for us to allocate the next field and other global variables(cause haybale is used to analyze a function that is not main) that may lead to a Null Pointer error?

[cdisselkoen]

Sorry for the delayed response (to this and the other thread) -- a lot on my plate right now.

Yes, you will have to initialize those other fields if you want Haybale to consider specific values for them. If you don't initialize them, Haybale will consider that memory to be unconstrained, i.e., could have any value, including NULL, hence the null pointer error.

For null pointer errors specifically, you may want to configure Config.null_pointer_checking instead; this has a few different options for how Haybale treats and reports possible null pointer dereferences.

[Just1ceP4rtn3r]

Haha, no problem. Then I need to initialize those fields. Otherwise, not only it will lead to the null pointer error, but also may consume a large of time to solve constraints. Thanks!