How to use manticore - 10 common examples

def test():
    from manticore.native import Manticore

    if __name__ == "__main__":
        import sys

        prog = sys.argv[1]
        params = sys.argv[2:]
    else:
        prog = "test_exploit_generation_example/bof"
        params = ["AAAAAAAAAAAAAAAAAAAAAAA"]

    m = Manticore(prog, params)
    m.verbosity(2)
    # 'trace' will contain the executed instructions
    m.context["trace"] = []

    # None: The hook will be applied to all the instructions
    @m.hook(None)
    def record_trace(state):
        pc = state.cpu.PC
        ins = state.cpu.instruction
        # Store the instruction
        with m.locked_context() as c:
            c["trace"] += [pc]

            # We manipulate directly capstone instruction
            c["last_ins"] = "%s %s" % (ins.mnemonic, ins.op_str)
            # print(state.cpu)

r2 = r2pipe.open(file)
    r2.cmd("aaa")
    for x in range(0, 11):
        dis = r2.cmd("pdf @ sym.check_char_{}".format(x))
        dis = dis.decode()
        entry = int(dis.split("\n")[4].split()[1], 16)
        for line in dis.split("\n"):
            # print(line)
            if "exit" in line:
                exit_call = int(line.split()[2], 16)
            elif "je 0x" in line:
                je_statement = int(line.split()[2], 16)

        addrs.append((entry, je_statement, exit_call))

    m = Manticore(file)
    m.context["solved"] = False
    buff_addr = None

    @m.hook(0x4009A4)
    def hook(state):
        """ Jump over `puts` and `fgets` calls """
        state.cpu.EIP = 0x4009C1

    @m.hook(0x4009C8)
    def hook(state):
        """ Inject symbolic buffer instead of fgets """
        buff_addr = state.cpu.RDI
        with m.locked_context() as context:
            context["buff_addr"] = state.cpu.RDI
        print("Buf addr: {:x}".format(buff_addr))
        buffer = state.new_symbolic_buffer(12)

def symbolic_run(prog, params, trace, pc_crash):
    print("Starting symbolic execution")

    trace_set = set(trace)
    m = Manticore(prog, params)

    # The hook will be applied only to the instruction @pc_crash
    @m.hook(pc_crash)
    def crash_analysis(state):
        # Add the constraint on eax
        state.constrain(state.cpu.EAX == 0x0804887C)  # 0x0804887c = @call_me
        # Retrieve the arguments corresponding to argv[1]
        argv_1 = next((i for i in state.input_symbols if i.name == "ARGV1"), None)
        if argv_1:
            # Ask the value of argv_1 to the solver
            val_argv_1 = state.solve_one(argv_1)
            # Pretty print of the solution
            print("The solution is:")
            print("\\x" + "\\x".join("{:02x}".format(c) for c in val_argv_1))
        state.abandon()

def concrete_run(prog, params):
    print("Starting concrete execution")

    m = Manticore(prog, params)
    # 'trace' will contain the executed instructions
    m.context["trace"] = []

    # None: The hook will be applied to all the instructions
    @m.hook(None)
    def record_trace(state):
        pc = state.cpu.PC

        # Store the instruction
        with m.locked_context() as c:
            c["trace"] += [pc]

    m.run()

    # Print number of instructions recorded