search

PKU-ASAL / SeeWasm

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

br_table instruction emulation error #33

Closed HNYuuu closed 2 years ago

HNYuuu commented 2 years ago

Describe the bug There may be some bugs in emulating br_table instruction

To Reproduce The command is:

python3 eunomia_entry -f ./Wasm-samples/c_samples.nosync/emcc/df2cf_cp_l1.wasm -s --onlyfunc main --need_mapper -v

The output is:

...
DEBUG:root:
Instruction:    get_local 4
Offset:         63
Current Func:   $func7
Stack:          []
Local Var:      defaultdict(<function WasmVMstate.__init__.<locals>.local_default at 0x119231f70>, {0: 4294967288, 1: 5246448, 2: 16, 3: 5246432, 4: 4294967288, 5: 9})
Global Var:     {0: 5246448, 1: 0, 2: 0}
Memory:         {(5246492, 5246496): 0, (5246480, 5246484): 5246491, (5246468, 5246476): 22533511558725584, (5246447, 5246448): 248}
Constraints:    []

DEBUG:root:
Instruction:    br_table 10, [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], 10
Offset:         65
Current Func:   $func7
Stack:          [4294967288]
Local Var:      defaultdict(<function WasmVMstate.__init__.<locals>.local_default at 0x119231f70>, {0: 4294967288, 1: 5246448, 2: 16, 3: 5246432, 4: 4294967288, 5: 9})
Global Var:     {0: 5246448, 1: 0, 2: 0}
Memory:         {(5246492, 5246496): 0, (5246480, 5246484): 5246491, (5246468, 5246476): 22533511558725584, (5246447, 5246448): 248}
Constraints:    []

WARNING:root:End df2cf
DEBUG:root:
Instruction:    set_local 17
Offset:         116
Current Func:   $func8
Stack:          []
Local Var:      defaultdict(<function WasmVMstate.__init__.<locals>.local_default at 0x119231f70>, {0: 5246491, 1: 5246480, 2: 32, 3: 5246448, 4: 5246491, 5: 0, 6: 24, 7: 0, 8: 0, 9: 48, 10: 4294967248, 11: 4294967248, 12: 10, 13: 4294967288, 14: 24, 15: 4160749568, 16: 4294967288})
Global Var:     {0: 5246448, 1: 0, 2: 0}
Memory:         {(5246492, 5246496): 0, (5246480, 5246484): 5246491, (5246468, 5246476): 22533511558725584}
Constraints:    []

Traceback (most recent call last):
  File "eunomia_entry", line 181, in <module>
    main()
  File "eunomia_entry", line 168, in main
    graph.traverse()
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 321, in traverse
    self.final_states[entry_func] = self.traverse_one(entry_func)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 356, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 400, in algo_interval
    final_states = cls.visit_interval(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 664, in visit_interval
    f, emul_states = consumer(item)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 594, in consumer
    _, emul_states = cls.wasmVM.emulate_basic_block(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 142, in emulate_basic_block
    halt, ret = self.emulate_one_instruction(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 186, in emulate_one_instruction
    return instr_obj.emulate(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/instructions/ControlInstructions.py", line 321, in emulate
    return False, self.deal_with_call(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/instructions/ControlInstructions.py", line 169, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 356, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 400, in algo_interval
    final_states = cls.visit_interval(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 664, in visit_interval
    f, emul_states = consumer(item)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 594, in consumer
    _, emul_states = cls.wasmVM.emulate_basic_block(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 142, in emulate_basic_block
    halt, ret = self.emulate_one_instruction(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 186, in emulate_one_instruction
    return instr_obj.emulate(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/instructions/ControlInstructions.py", line 321, in emulate
    return False, self.deal_with_call(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/instructions/ControlInstructions.py", line 169, in deal_with_call
    possible_states = Graph.traverse_one(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 356, in traverse_one
    final_states = cls.algo_interval(entry_bb, state, has_ret, blks)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 400, in algo_interval
    final_states = cls.visit_interval(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 664, in visit_interval
    f, emul_states = consumer(item)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/graph.py", line 594, in consumer
    _, emul_states = cls.wasmVM.emulate_basic_block(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 142, in emulate_basic_block
    halt, ret = self.emulate_one_instruction(
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/emulator.py", line 195, in emulate_one_instruction
    instr_obj.emulate(state)
  File "/Users/ningyuhe/Documents/GitHub/Wasm-SE/eunomia/arch/wasm/instructions/VariableInstructions.py", line 26, in emulate
    var = state.symbolic_stack.pop()
IndexError: pop from empty list

You can see the $func7 is terminated after the emulation of br_table instruciton

zzhzz commented 2 years ago

bug fix in 36513af