klara.klara_z3.cov_manager.CovManager

class documentation

class CovManager(manager.AstManager): (source)

View In Hierarchy

Coverage specific manager

Method add_conditions Undocumented
Method arg_is_z3_var check if `arg` is initialized as z3 variables
Method build_cfg Undocumented
Method check_assumptions Undocumented
Method check_assumptions_and_get_model check assumption for satisfiability. Return True if assumptions is empty
Method clear_z3_cache Undocumented
Method disable_infer_check_sat Undocumented
Method enable_infer_check_sat enable inference system to filter unsat inference path
Method initialize Initialize all required process for analysis.
Method initialize_z3 Undocumented
Method initialize_z3_var_from_func Create z3 constant for all arguments in the function, type is based on arg annotation
Method load_cov_extensions get all file_path of plugins in plugins directory
Method uninitialize Undocumented
Instance Variable cov_cached Undocumented
Instance Variable leaf_cells_dict Undocumented
Instance Variable predicate_expr Undocumented
Instance Variable z3_assumptions_cache Undocumented
Instance Variable z3_assumptions_computed_cache Undocumented
Instance Variable z3_cache Undocumented
Instance Variable z3_solver Undocumented
Method _fresh_init Undocumented
Instance Variable _cov_manager_status Undocumented
Instance Variable _infer_wrapper Undocumented
Instance Variable _z3_func_args Undocumented

Inherited from AstManager:

Method __init__ Undocumented
Method add_weak_ref Undocumented
Method apply_transform Undocumented
Method bootstrap_builtins Construct builtin class type (e.g. int, float) in ast form This will need to only parse builtins.pyi for the class definition, and construct the class with appropriate locals method with the return type.
Method build_tree Undocumented
Method dump_infer Undocumented
Method infer_wrapper optional wrapper around infer()
Method load_default_extension Undocumented
Method load_default_stub_files Undocumented
Method load_extension simply import the file_obj since it's python file. But do some bookkeeping for printing purpose :param file_path: the file path in string to import :return: None
Method load_user_extension Undocumented
Method make_z3_var make a z3 field for python variable
Method reload_protocol reload all necessary protocol based on config reload the dunder method based on py_version in config
Method temp_manager save the manager state and restore it after the operation.
Method unload_all_extensions Undocumented
Constant BUILTINS_FILE Undocumented
Instance Variable __dict__ Undocumented
Instance Variable built_tree Undocumented
Instance Variable builtins_tree Undocumented
Instance Variable config Undocumented
Instance Variable loaded_extension Undocumented
Instance Variable loaded_modules Undocumented
Instance Variable register_transform Undocumented
Instance Variable transform Undocumented
Instance Variable unregister_transform Undocumented
Instance Variable weakrefs Undocumented
Instance Variable z3var_maps Undocumented
Method _reload_protocol Undocumented
Instance Variable _ast_manager_status Undocumented

Inherited from BaseManager (via AstManager):

Method clear_infer_cache Undocumented
Method get_infer_statistics Undocumented
Method reset Undocumented
Instance Variable builtins_ast_cls Undocumented
Instance Variable infer_cache Undocumented
Instance Variable infer_count Undocumented
Instance Variable logger Undocumented
Instance Variable skipped_infer_count Undocumented
Instance Variable skipped_same_operand_count Undocumented
Instance Variable skipped_same_operand_nested_count Undocumented
Instance Variable skipped_z3_operand Undocumented
Constant _LOG_METHOD_REPR Undocumented
Constant _VERBOSITY_LEVEL Undocumented
Class Variable _core Undocumented
Instance Variable _manager_status Undocumented
def add_conditions(self, conditions): (source)

Undocumented

Parameters
conditions:setUndocumented
def arg_is_z3_var(self, arg): (source)

check if `arg` is initialized as z3 variables

Parameters
arg:nodes.ArgUndocumented
def build_cfg(self, as_tree): (source)

Undocumented

def check_assumptions(self, assumptions): (source)

Undocumented

Parameters
assumptions:setUndocumented
def check_assumptions_and_get_model(self, assumptions): (source)

check assumption for satisfiability. Return True if assumptions is empty

Parameters
assumptions:setUndocumented
def clear_z3_cache(self): (source)

Undocumented

def disable_infer_check_sat(self): (source)

Undocumented

def enable_infer_check_sat(self, infer_check_sat): (source)

enable inference system to filter unsat inference path

def initialize(self, config=None): (source)
overrides klara.core.AstManager.initialize

Initialize all required process for analysis.

def initialize_z3(self): (source)

Undocumented

@contextlib.contextmanager
def initialize_z3_var_from_func(self, func): (source)

Create z3 constant for all arguments in the function, type is based on arg annotation

Parameters
func:nodes.FunctionDefUndocumented
def load_cov_extensions(self): (source)

get all file_path of plugins in plugins directory

def uninitialize(self): (source)
overrides klara.core.AstManager.uninitialize

Undocumented

cov_cached: dict = (source)

Undocumented

leaf_cells_dict: dict = (source)

Undocumented

predicate_expr: bool = (source)

Undocumented

z3_assumptions_cache: dict = (source)

Undocumented

z3_assumptions_computed_cache: dict = (source)

Undocumented

z3_cache: dict = (source)

Undocumented

z3_solver = (source)

Undocumented

def _fresh_init(self, config=None): (source)
overrides klara.core.AstManager._fresh_init

Undocumented

_cov_manager_status: bool = (source)

Undocumented

_infer_wrapper = (source)

Undocumented

_z3_func_args = (source)

Undocumented