PKU-ASAL / SeeWasm

A native symbolic execution engine for WebAssembly
40 stars 3 forks source link

invalid memory in query_cache() #100

Open harveyghq opened 1 year ago

harveyghq commented 1 year ago

Describe the bug

Can't symbolically analyze rust program branch_on_args_num.d.wasm, raising invalid memory exception. However, when feeding concrete args, the program can successfully analyze.

Here is the traceback (using original interval traverse method):

image

Note that I have also tried the new dfs traverse method, however, it also failed with the same error.

To Reproduce python launcher.py -f branch_on_args_num.d.wasm -s -v debug --source_type rust --sym_args 4

Expected behavior No invalid memory exception.

Additional context Here is the original Rust code snippet:

use std::env;

fn main() {
    let args: Vec<String> = env::args().collect();
    if args.len() == 1 {
        println!("only one argument!");
    } else if args.len() == 2 {
        println!("got two arguments!");
    } else {
        println!("more than two arguments!");
    }
    // dbg!(args);
}