<commit_before>from frontend.stmt_inferrer import *
from frontend.import_handler import ImportHandler

import ast
import os
import time
import astunparse

base_folder = 'tests/imp'
file_name = 'imp'

t = ImportHandler.get_module_ast(file_name, base_folder)

solver = z3_types.TypesSolver(t, base_folder=base_folder)

context = Context(t.body, solver)
solver.infer_stubs(context, infer)

for stmt in t.body:
    infer(stmt, context, solver)

solver.push()


def print_solver(z3solver):
    printer = z3_types.z3printer
    printer.set_pp_option('max_lines', 4000)
    printer.set_pp_option('max_width', 120)
    printer.set_pp_option('max_visited', 10000000)
    printer.set_pp_option('max_depth', 1000000)
    printer.set_pp_option('max_args', 512)
    printer.pp(z3solver)


def print_context(ctx, ind=""):
    for v in sorted(ctx.types_map):
        z3_t = ctx.types_map[v]
        if isinstance(z3_t, (Context, AnnotatedFunction)):
            continue
        try:
            t = model[z3_t]
            print(ind + "{}: {}".format(v, t if t is not None else z3_t))
        except z3_types.Z3Exception:
            print(ind + "{}: {}".format(v, z3_t))
        if ctx.has_context_in_children(v):
            print_context(ctx.get_context_from_children(v), "\t" + ind)
        if not ind:
            print("---------------------------")
    children = False
    for child in ctx.children_contexts:
        if ctx.name == "" and child.name == "":
            children = True
            print_context(child, "\t" + ind)
    if not ind and children:
        print("---------------------------")

start_time = time.time()
check = solver.optimize.check()
end_time = time.time()

if check == z3_types.unsat:
    print("Check: unsat")
    solver.check(solver.assertions_vars)
    print(solver.unsat_core())
    print([solver.assertions_errors[x] for x in solver.unsat_core()])
else:
    model = solver.optimize.model()
    context.generate_typed_ast(model, solver)

    # uncomment this to write typed source into a file
    write_path = "inference_output/" + base_folder
    if not os.path.exists(write_path):
        os.makedirs(write_path)
    write_path += '/' + file_name + '.py'
    file = open(write_path, 'w')
    file.write(astunparse.unparse(t))
    file.close()

    ImportHandler.write_to_files(model, solver)
    # print(astunparse.unparse(t))


print("Ran in {} seconds".format(end_time - start_time))<commit_msg>Record constraints collection and solving times separately<commit_after>from frontend.stmt_inferrer import *
from frontend.import_handler import ImportHandler

import ast
import os
import time
import astunparse

start_time = time.time()
base_folder = 'tests/imp'
file_name = 'imp'

t = ImportHandler.get_module_ast(file_name, base_folder)

solver = z3_types.TypesSolver(t, base_folder=base_folder)

context = Context(t.body, solver)
solver.infer_stubs(context, infer)

for stmt in t.body:
    infer(stmt, context, solver)

end_time = time.time()
print("Constraints collection took  {}s".format(end_time - start_time))

solver.push()



def print_solver(z3solver):
    printer = z3_types.z3printer
    printer.set_pp_option('max_lines', 4000)
    printer.set_pp_option('max_width', 120)
    printer.set_pp_option('max_visited', 10000000)
    printer.set_pp_option('max_depth', 1000000)
    printer.set_pp_option('max_args', 512)
    printer.pp(z3solver)


def print_context(ctx, ind=""):
    for v in sorted(ctx.types_map):
        z3_t = ctx.types_map[v]
        if isinstance(z3_t, (Context, AnnotatedFunction)):
            continue
        try:
            t = model[z3_t]
            print(ind + "{}: {}".format(v, t if t is not None else z3_t))
        except z3_types.Z3Exception:
            print(ind + "{}: {}".format(v, z3_t))
        if ctx.has_context_in_children(v):
            print_context(ctx.get_context_from_children(v), "\t" + ind)
        if not ind:
            print("---------------------------")
    children = False
    for child in ctx.children_contexts:
        if ctx.name == "" and child.name == "":
            children = True
            print_context(child, "\t" + ind)
    if not ind and children:
        print("---------------------------")

start_time = time.time()
check = solver.optimize.check()
end_time = time.time()

if check == z3_types.unsat:
    print("Check: unsat")
    solver.check(solver.assertions_vars)
    print(solver.unsat_core())
    print([solver.assertions_errors[x] for x in solver.unsat_core()])
else:
    model = solver.optimize.model()
    context.generate_typed_ast(model, solver)

    # uncomment this to write typed source into a file
    write_path = "inference_output/" + base_folder
    print("Output is written to {}".format(write_path))
    if not os.path.exists(write_path):
        os.makedirs(write_path)
    write_path += '/' + file_name + '.py'
    file = open(write_path, 'w')
    file.write(astunparse.unparse(t))
    file.close()

    ImportHandler.write_to_files(model, solver)
    # print(astunparse.unparse(t))


print("Constraints solving took  {}s".format(end_time - start_time))
{'fraction_non_alphanumeric': 0.14134067230194614, 'fraction_numerical': 0.01494004324749361, 'mean_word_length': 3.073658927141713, 'pattern_counts': {'":': 2, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 2, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '741946', 'n_tokens_mistral': 1768, 'n_tokens_neox': 1708, 'n_words': 358}