PKU-ASAL / SeeWasm

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

z3.z3types.Z3Exception: b'invalid extract application' #99

Open harveyghq opened 1 year ago

harveyghq commented 1 year ago

Describe the bug When using Rust std::env::args_os to accept command line arguments, z3 backend generates an error. I think z3 doesn't support some types, because std::env::args_os is designed to accept invalid unicode argument. ref

image

Some of the last analyzed functions:

image

To Reproduce python launcher.py -f args_os.d.wasm -s -v debug --source_type rust

Expected behavior No errors.

Additional context args_os.d.wasm.tar.gz

harveyghq commented 1 year ago

I find Rust std::env::args_os is widely used in command line parser library (e.g. clap), so it'd better fix this.

harveyghq commented 1 year ago

btw here is the code snippet, and I use rustc 1.63.0 to compile to wasm32-wasi

use std::env;

fn main() { 
    // Prints each argument on a separate line
    for argument in env::args_os() {
        println!("{argument:?}");
    }
}