#!/usr/bin/env python

import argparse
import os, sys

def get_base_cmd():
    return "opt " + \
            "-load $LLVM_ROOT/install/lib/id-manager.so " + \
            "-load $LLVM_ROOT/install/lib/bc2bdd.so " + \
            "-load $LLVM_ROOT/install/lib/callgraph-fp.so " + \
            "-load $LLVM_ROOT/install/lib/mbb.so " + \
            "-load $LLVM_ROOT/install/lib/cfg.so " + \
            "-load $LLVM_ROOT/install/lib/preparer.so " + \
            "-load $LLVM_ROOT/install/lib/slicer-trace.so " + \
            "-load $LLVM_ROOT/install/lib/max-slicing.so " + \
            "-load $LLVM_ROOT/install/lib/int.so " + \
            "-load $LLVM_ROOT/install/lib/int-test.so "

if __name__ == "__main__":
    parser = argparse.ArgumentParser(description = "Dump integer constraints")
    parser.add_argument("bc",
            help = "the bitcode of the program to be analyzed")
    parser.add_argument("lt",
            help = "the landmark trace (.lt file)")
    args = parser.parse_args()

    cmd = get_base_cmd()
    cmd += "-int-test "
    cmd += "-input-landmark-trace " + args.lt + " "
    cmd += "-disable-output "
    cmd += "< " + args.bc
    print >> sys.stderr, cmd
    os.system(cmd)
