PKU-ASAL / SeeWasm

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

AssertionError in test.py sample heap_bo_l1.wasm #56

Closed 99hansling closed 2 years ago

99hansling commented 2 years ago

Describe the bug In implement engine on heap_bo_l1.wasm, an AssertionError occurred. Here is Traceback information:

Traceback (most recent call last):
  File "eunomia_entry", line 182, in <module>
    main()
  File "eunomia_entry", line 169, in main
    graph.traverse()
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 360, in traverse
    self.final_states[entry_func] = self.traverse_one(entry_func)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 159, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 406, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 527, in algo_interval
    final_states = cls.visit_interval(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 652, in visit_interval
    halt_flag, emul_states = consumer(item)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/graph.py", line 591, in consumer
    emul_states = cls.wasmVM.emulate_basic_block(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 135, in emulate_basic_block
    ret = self.emulate_one_instruction(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/emulator.py", line 180, in emulate_one_instruction
    return instr_obj.emulate(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 310, in emulate
    return self.deal_with_call(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/instructions/ControlInstructions.py", line 133, in deal_with_call
    func.emul(state, param_str, return_str, data_section, analyzer)
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 207, in emul
    src_string = C_extract_string_by_mem_pointer(
  File "/root/123/Wasm-SE-active-pure-wasm-no-eos/eunomia/arch/wasm/internalFunctions.py", line 991, in C_extract_string_by_mem_pointer
    assert default_len is not None, f"extract {mem_pointer} from memory, however, the loaded part is a symbol, the default len should not be None"
AssertionError: extract 5246416 from memory, however, the loaded part is a symbol, the default len should not be None

To Reproduce Steps to reproduce the behavior: 1.Use the command /usr/bin/python3 test.py e, you'll get the AssertionError under test.py context 2.Also you can reproduce the behavior by directly execute the command /usr/bin/python3 eunomia_entry -f ./Wasm-samples/c_samples.nosync/emcc/heap_bo_l1.wasm -s --onlyfunc main --need_mapper

Expected behavior The AssertionError will be resolved for good.

Additional context Just under python environment of the requirements with Ubuntu 20.09 LTS.

HNYuuu commented 2 years ago

Please refer to #57, the heap_bo_l1.wasm cannot be analyzed correctly as the external function dlfree.

Maybe invoking runtime, e.g., WASI, to dynamically execute this function in the future, instead of statically emulate it.