[klee-dev] Symbolizing a struct with a std::string and a std::vector

[Alastair Reid]

I ran into this problem in Rust where I wanted a way to create symbolic
vectors, btrees, strings, etc.
And, importantly, I wanted to use the existing standard types so that I
could pass them to Rust functions that used the standard library.

The generic approach that I took was to do it entirely using the library's
API.
eg to create a vector of length N with symbolic u32 entries, I would do

let mut v: Vec<u32> = Vec::with_capacity(N);  // empty vector with room for
N entries
for _ in 0..N { // loop that executes N times
    v.push(u32::arbitrary()); // insert a symbolic value at tail of vector
}

[The actual code is templated so that 'u32' is replaced with a template
parameter - but easier to show the untemplated code]

For structures that store the object in some specific order, I modified
this approach slightly
by inserting objects in ascending order.

        let mut r: BTreeMap<u32, i64> = BTreeMap::new(); // map from u32 to
i64

        // Keys are generated in increasing order to reduce the number of
effectively equivalent paths through the generation code.
        let mut k = u32::arbitrary(); // pick the first key
        for _ in 0..len {
            let v = i32::arbitrary(); // pick next value
            r.insert(k, v); // Add "k -> v" to the map
            let next = u32::arbitrary(); // pick next key
            verifier::assume(k <= next); // generate entries in fixed order
            k = next; // use this key next time
        }

Using this approach, I was able to create symbolic values for all the major
types in Rust's container library with the exception of Rust's HashMap
where I guessed (but did not actually try) that the hashing would be too
complex for KLEE to do anything useful with.

I have tried this in a bunch of simple tests - but not really used it in
anger on real code yet.

The main restriction of this approach is that the data structure's size has
to be a concrete value.
I could probably relax that slightly using klee_get_value() to pick a few
concrete values to test with - I've been experimenting with how to use this
effectively.

--
Alastair

I have modified this approach slightly for generating symbolic strings
because *maybe* it's more efficient (I have not actually measured whether
it is or not).
Rust's Vec<T> type is just a triple of <*T, int, int> where the two ints
are amount of space used and the amount of space allocated.
You can choose to take the Vec apart and put it back together in unsafe
Rust code - although almost anything you might do with that triple strays
into undefined behaviour. But, the one thing you can do is assign values to
the data and put the triple back together again.

    let v: Vec<u8> = Vec::with_capacity(n);

    // take vector apart so that we can access unused capacity
    let mut v = mem::ManuallyDrop::new(v);
    let p = v.as_mut_ptr();

    unsafe {
        // mark contents of vector as symbolic
        let data = p as *mut raw::c_void;
        let null = 0 as *const i8;
        klee_make_symbolic(data, n, null);

        // put vector back together again,
        // with same capacity but increased length
        Vec::from_raw_parts(p, n, n)
    }



On Tue, Mar 16, 2021 at 8:31 AM Alberto Garcia <agarciaillera at gmail.com>
wrote:

> Hi,
> I've read every tutorial in the documentation and the external resources
> but I've not found any information on symbolizing C++ containers.
> What would be the best approach to symbolize a struct containing a
> std::string and a std::vector?
> Here is some quick code I wrote to demonstrate what I'm trying to do?
>
> struct A{
>   std::string str;
>   std::vector<int> vec;
>   bool flag;
> };
>
>
> void test(struct A myStruct){
>   if(str.size()>4 && str[3] == 'A'){
>     printf("Winer");
>    }
>    else {
>     printf("Losser");
>   }
>
> int main(){
>   struct A myStruct;
>   myStruct.str = std::string("test"); // Just so there is some memory allocated at myStruct.str
>   myStruct.vec= {1,2,3,4}; // To create a std::vector of 4 elements
>
>   klee_make_symbolic(&myStruct.str[0], myStruct.str.size(), "my string");
>
>   for(int i= 0; i<myStruct.vec.size(); i++ ){
>     klee_make_symbolic(&myStruct.vec[i], sizeof(int), "my int vector item"); // I may have to not give the same name to every item in vector
>   }
>   test(myStruct);
>   return 0;
> }
>
> Is this the correct way to symbolize a std::string and a std::vector? How
> can I make the size of either of them symbolic?
>
> Thank you.
>
> --
> Alberto García Illera
>
> GPG Public Key <https://goo.gl/yshdwh>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed