diff --git a/QueryBuilding/formula_building.py b/QueryBuilding/formula_building.py index 4fd28b0..c45f997 100644 --- a/QueryBuilding/formula_building.py +++ b/QueryBuilding/formula_building.py @@ -12,16 +12,90 @@ StateValueInInterval - models the atom (s(x) in I) for some state s, a name x and an interval (list) I. TransitionDurationInInterval - models the atom (d(delta t) in I) for some transition delta t and an interval (list) I. -Atoms are generated once states or transitions have been described by calling - """ import inspect # be careful with versions here... from collections import OrderedDict +import ast from VyPR.monitor_synthesis import formula_tree +""" +Function selection. +""" + + +class Module(object): + """ + Used to point to a module/function in specifications. + """ + + def __init__(self, module_name): + self._module_name = module_name + + def Function(self, function_name): + self._function_name = function_name + return self + + +class Functions(object): + """ + Given as keys in the initial specification config file dictionary by the developer. + """ + + def __init__(self, **parameter_dictionary): + """ + Parameters given here, with their values, act as criteria to select a set of functions in a project. + Multiple parameter values will be used in conjunction. + """ + # set the parameters given as object parameters that can be used in the search performed by instrumentation + self.criteria_dict = parameter_dictionary + + def is_satisfied_by(self, function_ast, scfg): + """ + Given a Function AST, decide whether the criteria defined by this instance are satisfied. + :param function_ast: + :param scfg: + :return: True or False + """ + for criterion_name in self.criteria_dict: + if criterion_name == "containing_call_of": + edges = scfg.edges + call_found = False + for edge in edges: + if edge._operates_on and self.criteria_dict[criterion_name] in edge._operates_on: + call_found = True + # if no call was found, this criterion has not been met, + # so return False because the conjunction is broken + if not call_found: + return False + elif criterion_name == "containing_change_of": + vertices = scfg.vertices + change_found = False + for vertex in vertices: + if self.criteria_dict[criterion_name] in vertex._name_changed: + change_found = True + elif hasattr(vertex, "_structure_obj"): + if type(vertex._structure_obj) is ast.For: + if type(vertex._structure_obj.target) is ast.Tuple: + if (self.criteria_dict[criterion_name] in + map(lambda item: item.id, vertex._structure_obj.target)): + change_found = True + else: + if self.criteria_dict[criterion_name] == vertex._structure_obj.target.id: + change_found = True + # if no change was found, this criterion has not been met, + # so return False because the conjunction is broken + if not (change_found): + return False + # we found no evidence against satisfaction, so return True + return True + + def __repr__(self): + return "<%s>" % str(self.criteria_dict) + + """ General structure-building classes and methods. """ @@ -95,7 +169,7 @@ def __repr__(self): if self._formula is None: return "Forall(%s)" % self.bind_variables else: - return "Forall(%s).Formula(%s)" % \ + return "Forall(%s).Check(%s)" % \ (self.bind_variables, self.get_formula_instance()) def Forall(self, **bind_variable): @@ -226,6 +300,54 @@ def requires_state_or_transition(obj): return type(obj) in [StateValue, StateValueLength] +class PossiblyNumeric(object): + """ + Models a quantity that one can perform arithmetic on. + Should be inherited by any class that wants a user to be able to perform arithmetic with it. + """ + + def __mul__(self, value): + """ + Given a constant (we assume this for now), + add an object to the arithmetic stack so it can be applied + later when values are checked. + """ + if type(value) in [int, float]: + base_variable = composition_sequence_from_value([self._state], self._state)[-1] + if base_variable._arithmetic_build: + self._state._arithmetic_stack.append(formula_tree.ArithmeticMultiply(value)) + return self + else: + raise Exception("Value used to multiply quantity %s must be of type int or float." % self) + + def __add__(self, value): + if type(value) in [int, float]: + base_variable = composition_sequence_from_value([self._state], self._state)[-1] + if base_variable._arithmetic_build: + self._state._arithmetic_stack.append(formula_tree.ArithmeticAdd(value)) + return self + else: + raise Exception("Value added to quantity %s must be of type int or float." % self) + + def __sub__(self, value): + if type(value) in [int, float]: + base_variable = composition_sequence_from_value([self._state], self._state)[-1] + if base_variable._arithmetic_build: + self._state._arithmetic_stack.append(formula_tree.ArithmeticSubtract(value)) + return self + else: + raise Exception("Value subtracted from quantity %s must be of type int or float." % self) + + def __truediv__(self, value): + if type(value) in [int, float] and value != 0: + base_variable = composition_sequence_from_value([self._state], self._state)[-1] + if base_variable._arithmetic_build: + self._state._arithmetic_stack.append(formula_tree.ArithmeticTrueDivide(value)) + return self + else: + raise Exception("Value used to divide quantity %s must be non-zero and of type int or float." % self) + + class StaticState(object): """ Models a state attained by the monitored program at runtime. @@ -244,7 +366,11 @@ def __init__(self, bind_variable_name, name_changed, instruction_coordinates, us self._arithmetic_build = False def __call__(self, name): - return StateValue(self, name) + if type(name) is str: + return StateValue(self, name) + else: + raise Exception("Value given to state '%s' must be of type str, not %s." % (self, name.__class__.__name__)) + def next_call(self, function, record=None): """ @@ -252,15 +378,19 @@ def next_call(self, function, record=None): points if there is nesting. It is a list of variable values to record at the start of the next call to function. """ - return NextStaticTransition(self, function, record=record) + if type(function) is str: + return NextStaticTransition(self, function, record=record) + else: + raise Exception("Value given to (%s).next_call must be of type str, not %s." % + (self, function.__class__.__name__)) def __repr__(self): if self._required_binding: - return "%s = StaticState(changes=%s, uses=%s)" % \ + return "%s = changes('%s', uses=%s)" % \ (self._bind_variable_name, self._name_changed, self._required_binding) else: - return "%s = StaticState(changes=%s)" % \ + return "%s = changes('%s')" % \ (self._bind_variable_name, self._name_changed) def __eq__(self, other): @@ -278,6 +408,8 @@ class SourceStaticState(StaticState): def __init__(self, outgoing_transition): self._outgoing_transition = outgoing_transition + self._arithmetic_stack = [] + self._arithmetic_build = False def __repr__(self): return "(%s).input()" % self._outgoing_transition @@ -294,6 +426,8 @@ class DestinationStaticState(StaticState): def __init__(self, incoming_transition): self._incoming_transition = incoming_transition + self._arithmetic_stack = [] + self._arithmetic_build = False def __repr__(self): return "(%s).result()" % self._incoming_transition @@ -303,7 +437,7 @@ def __eq__(self, other): self._incoming_transition == other._incoming_transition) -class StateValue(object): +class StateValue(PossiblyNumeric): """ Models the value to which some state maps a program variable. """ @@ -316,11 +450,63 @@ def _in(self, interval): """ Generates an atom. """ - return formula_tree.StateValueInInterval( - self._state, - self._name, - interval - ) + if type(interval) is list and len(interval) == 2: + return formula_tree.StateValueInInterval( + self._state, + self._name, + interval + ) + elif type(interval) is tuple and len(interval) == 2: + return formula_tree.StateValueInOpenInterval( + self._state, + self._name, + interval + ) + else: + raise Exception("Value of type %s given to _in operator with %s('%s') is not supported." % + (interval.__class__.__name__, self._state, self._name)) + + def __lt__(self, value): + """ + Generates an atom. + """ + if type(value) is int: + return formula_tree.StateValueInOpenInterval( + self._state, + self._name, + [0, value] + ) + elif type(value) is StateValue: + return formula_tree.StateValueLessThanEqualStateValueMixed( + self._state, + self._name, + value._state, + value._name + ) + else: + raise Exception("Value of type %s given to < comparison with %s('%s') is not supported." % + (value.__class__.__name__, self._state, self._name)) + + def __le__(self, value): + """ + Generates an atom. + """ + if type(value) is int: + return formula_tree.StateValueInInterval( + self._state, + self._name, + [0, value] + ) + elif type(value) is StateValue: + return formula_tree.StateValueLessThanStateValueMixed( + self._state, + self._name, + value._state, + value._name + ) + else: + raise Exception("Value of type %s given to < comparison with %s('%s') is not supported." % + (value.__class__.__name__, self._state, self._name)) def equals(self, value): """ @@ -349,38 +535,8 @@ def length(self): def type(self): return StateValueType(self._state, self._name) - """ - Arithmetic overloading is useful for mixed atoms - when observed quantities are being compared to each other. - """ - - def __mul__(self, value): - """ - Given a constant (we assume this for now), - add an object to the arithmetic stack so it can be applied - later when values are checked. - """ - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticMultiply(value)) - return self - - def __add__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticAdd(value)) - return self - - def __sub__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticSubtract(value)) - return self - def __truediv__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticTrueDivide(value)) - return self - - -class StateValueLength(object): +class StateValueLength(PossiblyNumeric): """ Models the length being measured of a value given by a state. """ @@ -393,41 +549,67 @@ def _in(self, interval): """ Generates an atom. """ - return formula_tree.StateValueLengthInInterval( - self._state, - self._name, - interval - ) + if type(interval) is list and len(interval) == 2: + return formula_tree.StateValueLengthInInterval( + self._state, + self._name, + interval + ) + elif type(interval) is tuple and len(interval) == 2: + return formula_tree.StateValueLengthInOpenInterval( + self._state, + self._name, + interval + ) + else: + raise Exception("Value of type %s given to _in comparison with %s('%s').length() is not supported." % + (interval.__class__.__name__, self._state, self._name)) """ - Arithmetic overloading is useful for mixed atoms - when observed quantities are being compared to each other. + Overload comparison operators. """ - def __mul__(self, value): + def __lt__(self, value): """ - Given a constant (we assume this for now), - add an object to the arithmetic stack so it can be applied - later when values are checked. + Generates an atom. """ - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticMultiply(value)) - return self - - def __add__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticAdd(value)) - return self - - def __sub__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticSubtract(value)) - return self + if type(value) is int: + return formula_tree.StateValueLengthInOpenInterval( + self._state, + self._name, + [0, value] + ) + elif type(value) is StateValueLength: + return formula_tree.StateValueLengthLessThanStateValueLengthMixed( + self._state, + self._name, + value._state, + value._name + ) + else: + raise Exception("Value of type %s given to _in comparison with %s('%s').length() is not supported." % + (value.__class__.__name__, self._state, self._name)) - def __truediv__(self, value): - if self._state._arithmetic_build: - self._state._arithmetic_stack.append(formula_tree.ArithmeticTrueDivide(value)) - return self + def __le__(self, value): + """ + Generates an atom. + """ + if type(value) is int: + return formula_tree.StateValueLengthInInterval( + self._state, + self._name, + [0, value] + ) + elif type(value) is StateValueLength: + return formula_tree.StateValueLengthLessThanEqualStateValueLengthMixed( + self._state, + self._name, + value._state, + value._name + ) + else: + raise Exception("Value of type %s given to _in comparison with %s('%s').length() is not supported." % + (value.__class__.__name__, self._state, self._name)) class StateValueType(object): @@ -470,7 +652,11 @@ def next_call(self, function, record=None): record will only matter for the final instrumentation points if there is nesting. It is a list of variable values to record at the start of the next call to function. """ - return NextStaticTransition(self, function, record=record) + if type(function) is str: + return NextStaticTransition(self, function, record=record) + else: + raise Exception("Value given to state '%s' must be of type str, not %s." % + (self, function.__class__.__name__)) def input(self): return SourceStaticState(self) @@ -481,19 +667,19 @@ def result(self): def __repr__(self): if self._required_binding: if self._record: - return "%s = StaticTransition(operates_on=%s, uses=%s, record=%s)" % \ + return "%s = calls('%s', uses=%s, record=%s)" % \ (self._bind_variable_name, self._operates_on, self._required_binding, str(self._record)) else: - return "%s = StaticTransition(operates_on=%s, uses=%s)" % \ + return "%s = calls('%s', uses=%s)" % \ (self._bind_variable_name, self._operates_on, self._required_binding) else: if self._record: - return "%s = StaticTransition(operates_on=%s, record=%s)" % \ + return "%s = calls('%s', record=%s)" % \ (self._bind_variable_name, self._operates_on, str(self._record)) else: - return "%s = StaticTransition(operates_on=%s)" % \ + return "%s = calls('%s')" % \ (self._bind_variable_name, self._operates_on) def __eq__(self, other): @@ -526,7 +712,7 @@ def __eq__(self, other): self._operates_on == other._operates_on) -class Duration(object): +class Duration(PossiblyNumeric): """ Models the duration of a transition. """ @@ -549,7 +735,8 @@ def _in(self, interval): interval ) else: - raise Exception("Duration predicate wasn't defined properly.") + raise Exception("Value of type %s given to _in comparison on %s is not supported." % + (interval.__class__.__name__, self._transition)) def __lt__(self, value): """ @@ -573,6 +760,44 @@ def __lt__(self, value): self._transition, value._transition, ) + elif type(value) in [int, float]: + return formula_tree.TransitionDurationInOpenInterval( + self._transition, + [0, value] + ) + else: + raise Exception("Value of type %s given to < comparison on %s is not supported." % + (value.__class__.__name__, self._transition)) + + def __le__(self, value): + """ + Generates an atom. + """ + if type(value) is StateValue: + return formula_tree.TransitionDurationLessThanEqualStateValueMixed( + self._transition, + value._state, + value._name + ) + elif type(value) is StateValueLength: + return formula_tree.TransitionDurationLessThanEqualStateValueLengthMixed( + self._transition, + value._state, + value._name + ) + elif type(value) is Duration: + return formula_tree.TransitionDurationLessThanEqualTransitionDurationMixed( + self._transition, + value._transition, + ) + elif type(value) in [int, float]: + return formula_tree.TransitionDurationInInterval( + self._transition, + [0, value] + ) + else: + raise Exception("Value of type %s given to <= comparison on %s is not supported." % + (value.__class__.__name__, self._transition)) """ @@ -610,9 +835,42 @@ def _in(self, interval): interval ) else: - raise Exception("TimeBetween predicate wasn't defined properly.") + raise Exception("Value of type %s given to _in comparison on %s is not supported." % + (interval.__class__.__name__, self)) + + def __lt__(self, value): + """ + Generates an atom. + """ + if type(value) in [int, float]: + return formula_tree.TimeBetweenInOpenInterval( + self._lhs, + self._rhs, + [0, value] + ) + else: + raise Exception("Value of type %s given to < comparison on %s is not supported." % + (value.__class__.__name__, self)) + + def __le__(self, value): + """ + Generates an atom. + """ + if type(value) in [int, float]: + return formula_tree.TimeBetweenInInterval( + self._lhs, + self._rhs, + [0, value] + ) + else: + raise Exception("Value of type %s given to <= comparison on %s is not supported." % + (value.__class__.__name__, self)) +""" +Utility functions to extract information from formulas. +""" + def composition_sequence_from_value(sequence, current_operator): while not (type(current_operator) in [StaticState, StaticTransition]): sequence.append(current_operator) @@ -641,12 +899,7 @@ def derive_composition_sequence(atom): else: current_operator = atom - if type(atom) in [formula_tree.StateValueEqualToMixed, - formula_tree.TransitionDurationLessThanTransitionDurationMixed, - formula_tree.TransitionDurationLessThanStateValueMixed, - formula_tree.TransitionDurationLessThanStateValueLengthMixed, - formula_tree.TimeBetweenInInterval, - formula_tree.TimeBetweenInOpenInterval]: + if formula_tree.is_mixed_atom(atom): # atom is mixed - two composition sequences @@ -667,12 +920,18 @@ def derive_composition_sequence(atom): if type(current_operator) == formula_tree.TransitionDurationInInterval: current_operator = current_operator._transition + if type(current_operator) == formula_tree.TransitionDurationInOpenInterval: + current_operator = current_operator._transition elif type(current_operator) == formula_tree.StateValueEqualTo: current_operator = current_operator._state elif type(current_operator) == formula_tree.StateValueLengthInInterval: current_operator = current_operator._state + elif type(current_operator) == formula_tree.StateValueLengthInOpenInterval: + current_operator = current_operator._state elif type(current_operator) == formula_tree.StateValueInInterval: current_operator = current_operator._state + elif type(current_operator) == formula_tree.StateValueInOpenInterval: + current_operator = current_operator._state elif type(current_operator) == formula_tree.StateValueTypeEqualTo: current_operator = current_operator._state diff --git a/SCFG/construction.py b/SCFG/construction.py old mode 100755 new mode 100644 index 8a4f547..31f6622 --- a/SCFG/construction.py +++ b/SCFG/construction.py @@ -129,10 +129,19 @@ def get_reversed_string_list(obj, omit_subscripts=False): elif type(obj.slice.value) is ast.Name: return ["[%s]" % obj.slice.value.id] + get_reversed_string_list(obj.value, omit_subscripts=omit_subscripts) + elif type(obj.slice.value) is ast.Subscript: + return ["[...]"] + get_reversed_string_list(obj.value, omit_subscripts=omit_subscripts) + elif type(obj.slice.value) is ast.Call: + if type(obj.slice.value.func) is ast.Attribute: + return [get_attr_name_string(obj.slice.value.func)] + else: + return [obj.slice.value.func.id] elif type(obj) is ast.Call: return get_function_name_strings(obj) elif type(obj) is ast.Str: return [obj.s] + else: + return [str(obj)] def get_attr_name_string(obj, omit_subscripts=False): @@ -197,7 +206,13 @@ def __init__(self, entry=None, path_length=None, structure_obj=None, reference_v # nothing else could be changed self._name_changed = [] elif type(entry) is ast.Raise: - self._name_changed = [entry.type.func.id] + if type(entry.type) is ast.Call: + if type(entry.type.func) is ast.Attribute: + self._name_changed = [get_attr_name_string(entry.type.func)] + else: + self._name_changed = [entry.type.func.id] + else: + self._name_changed = [] elif type(entry) is ast.Pass: self._name_changed = ["pass"] elif type(entry) is ast.Continue: @@ -246,7 +261,14 @@ def __init__(self, condition, instruction=None): elif type(self._instruction) is ast.Return and type(self._instruction.value) is ast.Call: self._operates_on = get_function_name_strings(self._instruction.value) elif type(self._instruction) is ast.Raise: - self._operates_on = [self._instruction.type.func.id] + if type(self._instruction.type) is ast.Call: + if type(self._instruction.type.func) is ast.Attribute: + self._operates_on = [get_attr_name_string(self._instruction.type.func)] + else: + self._operates_on = [self._instruction.type.func.id] + else: + self._operates_on = [] + elif type(self._instruction) is ast.Pass: self._operates_on = ["pass"] else: @@ -402,9 +424,9 @@ def process_block(self, block, starting_vertices=None, condition=[], closest_loo for vertex in current_vertices: vertex.add_outgoing_edge(loop_ending_edge) - # direct all new edges to this new vertex + """# direct all new edges to this new vertex for edge in new_edges: - edge.set_target_state(new_vertex) + edge.set_target_state(new_vertex)""" # set the current_vertices to empty so no constructs can make an edge # from the preceding statement @@ -757,7 +779,7 @@ def process_block(self, block, starting_vertices=None, condition=[], closest_loo path_length = 0 elif ast_is_while(entry): - # needs work - but while loops haven't been a thing we've needed to handle so far + """# needs work - but while loops haven't been a thing we've needed to handle so far # need to add code to deal with branching vertices path_length += 1 @@ -773,7 +795,76 @@ def process_block(self, block, starting_vertices=None, condition=[], closest_loo final_vertex.add_outgoing_edge(new_positive_edge) new_positive_edge.set_target_state(base_vertex) - current_vertices = final_vertices + current_vertices = final_vertices""" + + entry._parent_body = block + path_length += 1 + + empty_pre_loop_vertex = CFGVertex(structure_obj=entry) + empty_pre_loop_vertex._name_changed = ['while'] + empty_post_loop_vertex = CFGVertex() + empty_post_loop_vertex._name_changed = ['post-while'] + self.vertices.append(empty_pre_loop_vertex) + self.vertices.append(empty_post_loop_vertex) + + # link current_vertices to the pre-loop vertex + for vertex in current_vertices: + new_edge = CFGEdge(entry.test, "while") + self.edges.append(new_edge) + vertex.add_outgoing_edge(new_edge) + new_edge.set_target_state(empty_pre_loop_vertex) + + current_vertices = [empty_pre_loop_vertex] + + # process loop body + final_vertices = self.process_block( + entry.body, + current_vertices, + ['enter-while'], + empty_post_loop_vertex + ) + + # for a for loop, we add a path recording instrument at the beginning of the loop body + # and after the loop body + self.branch_initial_statements.append(["while", entry.body[0], "enter-while", entry, "end-while"]) + + # add 2 edges from the final_vertex - one going back to the pre-loop vertex + # with the positive condition, and one going to the post loop vertex. + + for final_vertex in final_vertices: + # there will probably only ever be one final vertex, but we register a branching vertex + # self.branching_vertices.append(final_vertex) + for base_vertex in current_vertices: + new_positive_edge = CFGEdge('while-jump', 'while-jump') + self.edges.append(new_positive_edge) + final_vertex.add_outgoing_edge(new_positive_edge) + new_positive_edge.set_target_state(base_vertex) + + new_post_edge = CFGEdge("post-while", "post-while") + self.edges.append(new_post_edge) + final_vertex.add_outgoing_edge(new_post_edge) + new_post_edge.set_target_state(empty_post_loop_vertex) + + # process all of the continue vertices on the stack + for continue_vertex in self.continue_vertex_stack: + new_edge = CFGEdge("post-while", "post-while") + self.edges.append(new_edge) + continue_vertex.add_outgoing_edge(new_edge) + new_edge.set_target_state(empty_pre_loop_vertex) + self.continue_vertex_stack.remove(continue_vertex) + + skip_edge = CFGEdge(formula_tree.lnot(entry.test), "while-skip") + empty_pre_loop_vertex.add_outgoing_edge(skip_edge) + # skip_edge.set_target_state(final_vertices[0]) + skip_edge.set_target_state(empty_post_loop_vertex) + + current_vertices = [empty_post_loop_vertex] + # current_vertices = final_vertices + + condition.append("skip-while-loop") + + # reset path length for instructions after loop + path_length = 0 return current_vertices diff --git a/init_verification.py b/init_verification.py index 8d4e926..37a1bd5 100644 --- a/init_verification.py +++ b/init_verification.py @@ -8,6 +8,8 @@ import threading import flask import traceback +import requests +import base64 from Queue import Queue import requests @@ -17,8 +19,11 @@ from VyPR.verdict_reports import VerdictReport VERDICT_SERVER_URL = None -VYPR_OUTPUT_VERBOSE = True +VYPR_OUTPUT_VERBOSE = False PROJECT_ROOT = None +TEST_FRAMEWORK = 'no' +TEST_DIR = '' + class MonitoringLog(object): @@ -53,6 +58,7 @@ def log(self, message): print(message) + def to_timestamp(obj): if type(obj) is datetime.datetime: return obj.isoformat() @@ -72,14 +78,12 @@ def vypr_output(string): vypr_logger.log(string) -def send_verdict_report(function_name, time_of_call, end_time_of_call, program_path, verdict_report, - binding_to_line_numbers, transaction_time, property_hash): +def send_function_call_data(function_name, time_of_call, end_time_of_call, program_path, transaction_time): """ - Send verdict data for a given function call (function name + time of call). + Send a function call to the verdict server. """ global VERDICT_SERVER_URL - verdicts = verdict_report.get_final_verdict_report() - vypr_output("Sending verdicts to server...") + vypr_output("Sending function call data to server...") # first, send function call data - this will also insert program path data vypr_output("Function start time was %s" % time_of_call) @@ -90,7 +94,6 @@ def send_verdict_report(function_name, time_of_call, end_time_of_call, program_p "time_of_call": time_of_call.isoformat(), "end_time_of_call": end_time_of_call.isoformat(), "function_name": function_name, - "property_hash": property_hash, "program_path": program_path } insertion_result = json.loads(requests.post( @@ -98,6 +101,19 @@ def send_verdict_report(function_name, time_of_call, end_time_of_call, program_p data=json.dumps(call_data) ).text) + vypr_output("Function call data sent.") + + return insertion_result + + +def send_verdict_report(verdict_report, property_hash, function_id, function_call_id): + """ + Send verdict data for a given function call. + """ + global VERDICT_SERVER_URL + verdicts = verdict_report.get_final_verdict_report() + vypr_output("Sending verdicts to server...") + # second, send verdict data - all data in one request # for this, we first build the structure # that we'll send over HTTP @@ -118,15 +134,15 @@ def send_verdict_report(function_name, time_of_call, end_time_of_call, program_p verdict[4], verdict[5], verdict[6] - ], - "line_numbers": json.dumps(binding_to_line_numbers[bind_space_index]), + ] } verdict_dict_list.append(verdict_dict) request_body_dict = { - "function_call_id": insertion_result["function_call_id"], - "function_id": insertion_result["function_id"], - "verdicts": verdict_dict_list + "function_call_id": function_call_id, + "function_id": function_id, + "verdicts": verdict_dict_list, + "property_hash": property_hash } # send request @@ -143,19 +159,26 @@ def send_verdict_report(function_name, time_of_call, end_time_of_call, program_p vypr_output("Verdicts sent.") + + def consumption_thread_function(verification_obj): # the web service has to be considered as running forever, so the monitoring loop for now should also run forever # this needs to be changed for a clean exit INACTIVE_MONITORING = False + transaction = -1 continue_monitoring = True while continue_monitoring: # take top element from the queue try: top_pair = verification_obj.consumption_queue.get(timeout=1) + ## In case of flask testing except: + # Changing flag to false here because in normal testing, end-monitoring does not change to False. + # If exception is raised we just terminate the monitoring continue + if top_pair[0] == "end-monitoring": # return from the monitoring function to end the monitoring thread vypr_output("Returning from monitoring thread.") @@ -179,259 +202,368 @@ def consumption_thread_function(verification_obj): continue # if inactive monitoring is off (so monitoring is running), process what we consumed - vypr_output("Consuming: %s" % str(top_pair)) - property_hash = top_pair[0] + if top_pair[0] == "test_transaction": + transaction = top_pair[1] + vypr_output("Test Transaction >> %s" %str(top_pair)) + continue - # remove the property hash and just deal with the rest of the data - top_pair = top_pair[1:] - instrument_type = top_pair[0] - function_name = top_pair[1] + vypr_output("Consuming: %s" % str(top_pair)) - # get the maps we need for this function - maps = verification_obj.function_to_maps[function_name][property_hash] - static_qd_to_monitors = maps.static_qd_to_monitors - formula_structure = maps.formula_structure - bindings = maps.binding_space - program_path = maps.program_path + first_element = top_pair[0] - verdict_report = maps.verdict_report + if first_element == "function": - atoms = formula_structure._formula_atoms + # we have a function start/end instrument - if instrument_type == "function": - # we've received a point telling us that a function has started or ended - # for now, we can just process "end" - we reset the contents of the maps - # that are updated at runtime - scope_event = top_pair[2] + property_hash_list = top_pair[1] + function_name = top_pair[2] + scope_event = top_pair[3] if scope_event == "end": - vypr_output("*" * 50) + # first, send the function call data independently of any property + # the latest time of call and program path are the same everywhere + latest_time_of_call = verification_obj.function_to_maps[function_name][ + verification_obj.function_to_maps[function_name].keys()[0] + ].latest_time_of_call + program_path = verification_obj.function_to_maps[function_name][ + verification_obj.function_to_maps[function_name].keys()[0] + ].program_path - vypr_output("Function '%s' started at time %s has ended at %s." - % (function_name, str(maps.latest_time_of_call), str(top_pair[-1]))) - # before resetting the qd -> monitor map, go through it to find monitors - # that reached a verdict, and register those in the verdict report + if 'yes' in TEST_FRAMEWORK : + transaction_time = transaction + else: + transaction_time = top_pair[3] - for static_qd_index in static_qd_to_monitors: - for monitor in static_qd_to_monitors[static_qd_index]: - # check if the monitor has a collapsing atom - only then do we register a verdict - if monitor.collapsing_atom: - verdict_report.add_verdict( - static_qd_index, - monitor._formula.verdict, - monitor.atom_to_observation, - monitor.atom_to_program_path, - atoms.index(monitor.collapsing_atom), - monitor.collapsing_atom_sub_index, - monitor.atom_to_state_dict - ) + insertion_data = send_function_call_data( + function_name, + latest_time_of_call, + top_pair[-1], + program_path, + transaction_time + ) - # everything not here is static data that we need, and should be left - maps.static_qd_to_monitors = {} + # now handle the verdict data we have for each property + for property_hash in property_hash_list: + + maps = verification_obj.function_to_maps[function_name][property_hash] + static_qd_to_monitors = maps.static_qd_to_monitors + verdict_report = maps.verdict_report + + vypr_output("*" * 50) + + # before resetting the qd -> monitor map, go through it to find monitors + # that reached a verdict, and register those in the verdict report + + for static_qd_index in static_qd_to_monitors: + for monitor in static_qd_to_monitors[static_qd_index]: + # check if the monitor has a collapsing atom - only then do we register a verdict + if monitor.collapsing_atom_index is not None: + verdict_report.add_verdict( + static_qd_index, + monitor._formula.verdict, + monitor.atom_to_observation, + monitor.atom_to_program_path, + monitor.collapsing_atom_index, + monitor.collapsing_atom_sub_index, + monitor.atom_to_state_dict + ) + + # reset the monitors + maps.static_qd_to_monitors = {} + + # send the verdict data + send_verdict_report( + verdict_report, + property_hash, + insertion_data["function_id"], + insertion_data["function_call_id"] + ) + + # reset the verdict report + maps.verdict_report.reset() + + # reset the function start time for the next time + maps.latest_time_of_call = None - # generate the verdict report + elif scope_event == "start": + vypr_output("Function '%s' has started." % function_name) - report_map = verdict_report.get_final_verdict_report() + for property_hash in property_hash_list: + # reset anything that might have been left over from the previous call, + # especially if an unhandled exception caused the function to end without + # vypr instruments sending an end signal - binding_to_line_numbers = {} + maps = verification_obj.function_to_maps[function_name][property_hash] + maps.static_qd_to_monitors = {} + maps.verdict_report.reset() - for bind_space_index in report_map.keys(): + # remember when the function call started + maps.latest_time_of_call = top_pair[4] - binding = bindings[bind_space_index] + vypr_output("Set start time to %s" % maps.latest_time_of_call) - binding_to_line_numbers[bind_space_index] = [] + # reset the program path + maps.program_path = [] - # for each element of the binding, print the appropriate representation - for bind_var in binding: + vypr_output("*" * 50) + else: + + # we have another kind of instrument that is specific to a property + + property_hash = top_pair[0] + + # remove the property hash and just deal with the rest of the data + top_pair = top_pair[1:] + instrument_type = top_pair[0] + function_name = top_pair[1] + + # get the maps we need for this function + maps = verification_obj.function_to_maps[function_name][property_hash] + static_qd_to_monitors = maps.static_qd_to_monitors + formula_structure = maps.formula_structure + program_path = maps.program_path + + verdict_report = maps.verdict_report + + atoms = formula_structure._formula_atoms - if type(bind_var) is CFGVertex: - if bind_var._name_changed == ["loop"]: - binding_to_line_numbers[bind_space_index].append(bind_var._structure_obj.lineno) + if instrument_type == "trigger": + # we've received a trigger instrument + + vypr_output("Processing trigger - dealing with monitor instantiation") + + static_qd_index = top_pair[2] + bind_variable_index = top_pair[3] + + vypr_output("Trigger is for bind variable %i" % bind_variable_index) + if bind_variable_index == 0: + vypr_output("Instantiating new, clean monitor") + # we've encountered a trigger for the first bind variable, so we simply instantiate a new monitor + new_monitor = formula_tree.new_monitor(formula_structure.get_formula_instance()) + try: + static_qd_to_monitors[static_qd_index].append(new_monitor) + except: + static_qd_to_monitors[static_qd_index] = [new_monitor] + else: + vypr_output("Processing existing monitors") + # we look at the monitors' timestamps, and decide whether to generate a new monitor + # and copy over existing information, or update timestamps of existing monitors + new_monitors = [] + subsequences_processed = [] + for monitor in static_qd_to_monitors[static_qd_index]: + # check if the monitor's timestamp sequence includes a timestamp for this bind variable + vypr_output( + " Processing monitor with timestamp sequence %s" % str(monitor._monitor_instantiation_time)) + if len(monitor._monitor_instantiation_time) == bind_variable_index + 1: + if monitor._monitor_instantiation_time[:bind_variable_index] in subsequences_processed: + # the same subsequence might have been copied and extended multiple times + # we only care about one + continue else: - binding_to_line_numbers[bind_space_index].append( - bind_var._previous_edge._instruction.lineno) - elif type(bind_var) is CFGEdge: - binding_to_line_numbers[bind_space_index].append(bind_var._instruction.lineno) - - # send the verdict we send the function name, the time of the function call, the verdict report - # object, the map of bindings to their line numbers and the date/time of the request the identify it - # (single threaded...) - send_verdict_report( - function_name, - maps.latest_time_of_call, - top_pair[-1], - maps.program_path, - verdict_report, - binding_to_line_numbers, - top_pair[3], - top_pair[4] - ) + subsequences_processed.append(monitor._monitor_instantiation_time[:bind_variable_index]) + # construct new monitor + vypr_output(" Instantiating new monitor with modified timestamp sequence") + # instantiate a new monitor using the timestamp subsequence excluding the current bind + # variable and copy over all observation, path and state information + + old_instantiation_time = list(monitor._monitor_instantiation_time) + updated_instantiation_time = tuple( + old_instantiation_time[:bind_variable_index] + [datetime.datetime.now()]) + new_monitor = formula_tree.new_monitor(formula_structure.get_formula_instance()) + new_monitors.append(new_monitor) + + # copy timestamp sequence, observation, path and state information + new_monitor._monitor_instantiation_time = updated_instantiation_time + + # iterate through the observations stored by the previous monitor + # for bind variables before the current one and use them to update the new monitor + for atom_index in monitor._state._state: + + atom = atoms[atom_index] + + if not (type(atom) is formula_tree.LogicalNot): + + # the copy we do for the information related to the atom + # depends on whether the atom is mixed or not + + if formula_tree.is_mixed_atom(atom): + + # for mixed atoms, the return value here is a list + base_variables = get_base_variable(atom) + # determine the base variables which are before the current bind variable + relevant_base_variables = filter( + lambda var : ( + formula_structure._bind_variables.index(var) < bind_variable_index + ), + base_variables + ) + # determine the base variables' sub-indices in the current atom + relevant_sub_indices = map( + lambda var : base_variables.index(var), + relevant_base_variables + ) + + # copy over relevant information for the sub indices + # whose base variables had positions less than the current variable index + # relevant_sub_indices can contain at most 0 and 1. + for sub_index in relevant_sub_indices: + # set up keys in new monitor state if they aren't already there + if not(new_monitor.atom_to_observation.get(atom_index)): + new_monitor.atom_to_observation[atom_index] = {} + new_monitor.atom_to_program_path[atom_index] = {} + new_monitor.atom_to_state_dict[atom_index] = {} + + # copy over observation, program path and state information + new_monitor.atom_to_observation[atom_index][sub_index] = \ + monitor.atom_to_observation[atom_index][sub_index] + new_monitor.atom_to_program_path[atom_index][sub_index] = \ + monitor.atom_to_program_path[atom_index][sub_index] + new_monitor.atom_to_state_dict[atom_index][sub_index] = \ + monitor.atom_to_state_dict[atom_index][sub_index] + + # update the state of the monitor + new_monitor.check_atom_truth_value(atom, atom_index, atom_sub_index) + else: + + # the atom is not mixed, so copying over information is simpler + + if (formula_structure._bind_variables.index( + get_base_variable(atom)) < bind_variable_index + and not (monitor._state._state[atom] is None)): + + # decide how to update the new monitor based on the existing monitor's truth + # value for it + if monitor._state._state[atom_index] == True: + new_monitor.check_optimised(atom) + elif monitor._state._state[atom_index] == False: + new_monitor.check_optimised(formula_tree.lnot(atom)) + + # copy over observation, program path and state information + new_monitor.atom_to_observation[atom_index][0] = \ + monitor.atom_to_observation[atom_index][0] + new_monitor.atom_to_program_path[atom_index][0] = \ + monitor.atom_to_program_path[atom_index][0] + new_monitor.atom_to_state_dict[atom_index][0] = \ + monitor.atom_to_state_dict[atom_index][0] + + vypr_output(" New monitor construction finished.") + + elif len(monitor._monitor_instantiation_time) == bind_variable_index: + vypr_output(" Updating existing monitor timestamp sequence") + # extend the monitor's timestamp sequence + tmp_sequence = list(monitor._monitor_instantiation_time) + tmp_sequence.append(datetime.datetime.now()) + monitor._monitor_instantiation_time = tuple(tmp_sequence) + + # add the new monitors + static_qd_to_monitors[static_qd_index] += new_monitors + + if instrument_type == "path": + # we've received a path recording instrument + # append the branching condition to the program path encountered so far for this function. + program_path.append(top_pair[2]) + + if instrument_type == "instrument": + + static_qd_indices = top_pair[2] + atom_index = top_pair[3] + atom_sub_index = top_pair[4] + instrumentation_point_db_ids = top_pair[5] + observation_time = top_pair[6] + observation_end_time = top_pair[7] + observed_value = top_pair[8] + thread_id = top_pair[9] + try: + state_dict = top_pair[10] + except: + # instrument isn't from a transition measurement + state_dict = None - # reset the verdict report - maps.verdict_report.reset() + vypr_output("Consuming data from an instrument in thread %i" % thread_id) - # reset the function start time for the next time - maps.latest_time_of_call = None + lists = zip(static_qd_indices, instrumentation_point_db_ids) - # reset the program path - maps.program_path = [] + for values in lists: - elif scope_event == "start": - vypr_output("Function '%s' has started." % function_name) + static_qd_index = values[0] + instrumentation_point_db_id = values[1] - # remember when the function call started - maps.latest_time_of_call = top_pair[3] + vypr_output("Binding space index : %i" % static_qd_index) + vypr_output("Atom index : %i" % atom_index) + vypr_output("Atom sub index : %i" % atom_sub_index) + vypr_output("Instrumentation point db id : %i" % instrumentation_point_db_id) + vypr_output("Observation time : %s" % str(observation_time)) + vypr_output("Observation end time : %s" % str(observation_end_time)) + vypr_output("Observed value : %s" % observed_value) + vypr_output("State dictionary : %s" % str(state_dict)) - vypr_output("Set start time to %s" % maps.latest_time_of_call) + instrumentation_atom = atoms[atom_index] - vypr_output("*" * 50) + # update all monitors associated with static_qd_index + if static_qd_to_monitors.get(static_qd_index): + for (n, monitor) in enumerate(static_qd_to_monitors[static_qd_index]): + # checking for previous observation of the atom is done by the monitor's internal logic + monitor.process_atom_and_value(instrumentation_atom, observation_time, observation_end_time, + observed_value, atom_index, atom_sub_index, + inst_point_id=instrumentation_point_db_id, + program_path=len(program_path), state_dict=state_dict) - if instrument_type == "trigger": - # we've received a trigger instrument - vypr_output("Processing trigger - dealing with monitor instantiation") + if instrument_type == "test_status": - static_qd_index = top_pair[2] - bind_variable_index = top_pair[3] - vypr_output("Trigger is for bind variable %i" % bind_variable_index) - if bind_variable_index == 0: - vypr_output("Instantiating new, clean monitor") - # we've encountered a trigger for the first bind variable, so we simply instantiate a new monitor - new_monitor = formula_tree.new_monitor(formula_structure.get_formula_instance()) - try: - static_qd_to_monitors[static_qd_index].append(new_monitor) - except: - static_qd_to_monitors[static_qd_index] = [new_monitor] - else: - vypr_output("Processing existing monitors") - # we look at the monitors' timestamps, and decide whether to generate a new monitor - # and copy over existing information, or update timestamps of existing monitors - new_monitors = [] - subsequences_processed = [] - for monitor in static_qd_to_monitors[static_qd_index]: - # check if the monitor's timestamp sequence includes a timestamp for this bind variable - vypr_output( - " Processing monitor with timestamp sequence %s" % str(monitor._monitor_instantiation_time)) - if len(monitor._monitor_instantiation_time) == bind_variable_index + 1: - if monitor._monitor_instantiation_time[:bind_variable_index] in subsequences_processed: - # the same subsequence might have been copied and extended multiple times - # we only care about one - continue - else: - subsequences_processed.append(monitor._monitor_instantiation_time[:bind_variable_index]) - # construct new monitor - vypr_output(" Instantiating new monitor with modified timestamp sequence") - # instantiate a new monitor using the timestamp subsequence excluding the current bind - # variable and copy over all observation, path and state information - - old_instantiation_time = list(monitor._monitor_instantiation_time) - updated_instantiation_time = tuple( - old_instantiation_time[:bind_variable_index] + [datetime.datetime.now()]) - new_monitor = formula_tree.new_monitor(formula_structure.get_formula_instance()) - new_monitors.append(new_monitor) - - # copy timestamp sequence, observation, path and state information - new_monitor._monitor_instantiation_time = updated_instantiation_time - - # iterate through the observations stored by the previous monitor - # for bind variables before the current one and use them to update the new monitor - for atom in monitor._state._state: - if not (type(atom) is formula_tree.LogicalNot): - if (formula_structure._bind_variables.index( - get_base_variable(atom)) < bind_variable_index - and not (monitor._state._state[atom] is None)): - if monitor._state._state[atom] == True: - new_monitor.check_optimised(atom) - elif monitor._state._state[atom] == False: - new_monitor.check_optimised(formula_tree.lnot(atom)) - - atom_index = atoms.index(atom) - - for sub_index in monitor.atom_to_observation[atom_index].keys(): - new_monitor.atom_to_observation[atom_index][sub_index] = \ - monitor.atom_to_observation[atom_index][sub_index] - - for sub_index in monitor.atom_to_program_path[atom_index].keys(): - new_monitor.atom_to_program_path[atom_index][sub_index] = \ - monitor.atom_to_program_path[atom_index][sub_index] - - for sub_index in monitor.atom_to_state_dict[atom_index].keys(): - new_monitor.atom_to_state_dict[atom_index][sub_index] = \ - monitor.atom_to_state_dict[atom_index][sub_index] - - elif len(monitor._monitor_instantiation_time) == bind_variable_index: - vypr_output(" Updating existing monitor timestamp sequence") - # extend the monitor's timestamp sequence - tmp_sequence = list(monitor._monitor_instantiation_time) - tmp_sequence.append(datetime.datetime.now()) - monitor._monitor_instantiation_time = tuple(tmp_sequence) - - # add the new monitors - static_qd_to_monitors[static_qd_index] += new_monitors - - if instrument_type == "path": - # we've received a path recording instrument - # append the branching condition to the program path encountered so far for this function. - program_path.append(top_pair[2]) - - if instrument_type == "instrument": - - static_qd_indices = top_pair[2] - atom_index = top_pair[3] - atom_sub_index = top_pair[4] - instrumentation_point_db_ids = top_pair[5] - observation_time = top_pair[6] - observation_end_time = top_pair[7] - observed_value = top_pair[8] - thread_id = top_pair[9] - try: - state_dict = top_pair[10] - except: - # instrument isn't from a transition measurement - state_dict = None - vypr_output("Consuming data from an instrument in thread %i" % thread_id) + # verified_function = top_pair[1] + status = top_pair[2] + start_test_time = top_pair[3] + end_test_time = top_pair[4] + test_name = top_pair[6] + + # # We are trying to empty all the test cases in order to terminate the monitoring + # if test_name in list_test_cases: + # list_test_cases.remove(test_name) + # + # if len(list_test_cases) == 0: + # continue_monitoring = False + + if status.failures: + test_result = "Fail" + elif status.errors: + test_result = "Error" + else: + test_result = "Success" - lists = zip(static_qd_indices, instrumentation_point_db_ids) - for values in lists: + # If test data exists. - static_qd_index = values[0] - instrumentation_point_db_id = values[1] - vypr_output("Binding space index : %i" % static_qd_index) - vypr_output("Atom index : %i" % atom_index) - vypr_output("Atom sub index : %i" % atom_sub_index) - vypr_output("Instrumentation point db id : %i" % instrumentation_point_db_id) - vypr_output("Observation time : %s" % str(observation_time)) - vypr_output("Observation end time : %s" % str(observation_end_time)) - vypr_output("Observed value : %s" % observed_value) - vypr_output("State dictionary : %s" % str(state_dict)) + test_data = { + "test_name" : test_name, + "test_result" : test_result, + "start_time" : start_test_time.isoformat(), + "end_time" : end_test_time.isoformat() + + } + + json.loads(requests.post( + os.path.join(VERDICT_SERVER_URL, "insert_test_data/"), + data=json.dumps(test_data) + ).text) - instrumentation_atom = atoms[atom_index] - # update all monitors associated with static_qd_index - if static_qd_to_monitors.get(static_qd_index): - for (n, monitor) in enumerate(static_qd_to_monitors[static_qd_index]): - # checking for previous observation of the atom is done by the monitor's internal logic - monitor.process_atom_and_value(instrumentation_atom, observation_time, observation_end_time, - observed_value, atom_index, atom_sub_index, - inst_point_id=instrumentation_point_db_id, - program_path=len(program_path), state_dict=state_dict) # set the task as done - verification_obj.consumption_queue.task_done() + verification_obj.consumption_queue.task_done() - vypr_output("Consumption finished.") + vypr_output("Consumption finished.") - vypr_output("=" * 100) + vypr_output("=" * 100) # if we reach this point, the monitoring thread is ending - vypr_logger.end_logging() + #vypr_logger.end_logging() class PropertyMapGroup(object): @@ -448,56 +580,90 @@ def __init__(self, module_name, function_name, property_hash): (module_name.replace(".", "-"), function_name.replace(":", "-"), property_hash), "rb") as h: binding_space_dump = h.read() - # read in index hash map - with open(os.path.join(PROJECT_ROOT, "index_hash/module-%s-function-%s.dump") % \ - (module_name.replace(".", "-"), function_name.replace(":", "-")), "rb") as h: - index_to_hash_dump = h.read() - - inst_configuration = read_configuration("vypr.config") - - # get the specification file name - verification_conf_file = inst_configuration.get("specification_file") \ - if inst_configuration.get("specification_file") else "verification_conf.py" - - # reconstruct formula structure - # there's probably a better way to do this - # exec("".join(open(verification_conf_file, "r").readlines())) - try: from VyPR_queries_with_imports import verification_conf except ImportError: print("Query file generated by instrumentation couldn't be found. Run VyPR instrumentation first.") exit() - index_to_hash = pickle.loads(index_to_hash_dump) - property_index = index_to_hash.index(property_hash) + # to get the property structure, + property_data = json.loads( + requests.get( + os.path.join(VERDICT_SERVER_URL, "get_property_from_hash/%s/" % property_hash) + ).text + ) + property_index = property_data["index_in_specification_file"] vypr_output("Queries imported.") - # might just change the syntax in the verification conf file at some point to use : instead of . + # store all the data we have self.formula_structure = verification_conf[module_name][function_name.replace(":", ".")][property_index] self.binding_space = pickle.loads(binding_space_dump) self.static_qd_to_monitors = {} self.static_bindings_to_monitor_states = {} - self.static_bindings_to_trigger_points = {} self.verdict_report = VerdictReport() self.latest_time_of_call = None self.program_path = [] + def read_configuration(file): """ Read in 'file', parse into an object and return. """ - with open(file, "r") as h: - contents = h.read() + content = "" + skip = False + for line in open(file): + li = line.strip() + + # Handle multi-line comments + if li.startswith("/*"): + skip = True + if li.endswith("*/"): + skip = False + continue + + if not (li.startswith("#") or li.startswith("//")) and not skip: + content += line + + return json.loads(content) + + +def total_test_cases(): + + from os.path import dirname, abspath + import re + + global TEST_DIR + + ROOT_DIR = dirname(dirname(abspath(__file__))) + + test_cases = [] + + path = ROOT_DIR+'/' + TEST_DIR + + total_tests = [] + + #for r, d, f in os.walk(os.environ('PATH')): + for r, d, f in os.walk(path): + + for file in f: + + if file.startswith("test_") and (file.endswith('.py') or file.endswith('.py.inst')): + + readfile = open(os.path.join(r, file), "r") + + for line in readfile: + if re.search('(def)\s(test.*)', line): + test_cases.append( line[5:line.index('(')]) + return test_cases - return json.loads(contents) class Verification(object): def __init__(self): + """ Sets up the consumption thread for events from instruments. """ @@ -510,11 +676,24 @@ def __init__(self): # read configuration file inst_configuration = read_configuration("vypr.config") - global VERDICT_SERVER_URL, VYPR_OUTPUT_VERBOSE, PROJECT_ROOT + global VERDICT_SERVER_URL, VYPR_OUTPUT_VERBOSE, PROJECT_ROOT, VYPR_MODULE, TOTAL_TEST_RUN, TEST_FRAMEWORK VERDICT_SERVER_URL = inst_configuration.get("verdict_server_url") if inst_configuration.get( "verdict_server_url") else "http://localhost:9001/" VYPR_OUTPUT_VERBOSE = inst_configuration.get("verbose") if inst_configuration.get("verbose") else True PROJECT_ROOT = inst_configuration.get("project_root") if inst_configuration.get("project_root") else "" + VYPR_MODULE = inst_configuration.get("vypr_module") if inst_configuration.get("vypr_module") else "" + + TEST_FRAMEWORK = inst_configuration.get("test") \ + if inst_configuration.get("test") else "" + + # If testing is set then we should specify the test module + if TEST_FRAMEWORK in ['yes']: + TEST_DIR = inst_configuration.get("test_module") \ + if inst_configuration.get("test_module") else '' + + if TEST_DIR == '': + print ('Specify test module. Ending instrumentation - nothing has been done') + exit() # try to connect to the verdict server before we set anything up try: @@ -525,19 +704,8 @@ def __init__(self): self.initialisation_failure = True return - def initialise(self, flask_object): - - vypr_output("Initialising VyPR alongside service.") - - # read configuration file - inst_configuration = read_configuration("vypr.config") - global VERDICT_SERVER_URL, VYPR_OUTPUT_VERBOSE, PROJECT_ROOT - VERDICT_SERVER_URL = inst_configuration.get("verdict_server_url") if inst_configuration.get( - "verdict_server_url") else "http://localhost:9001/" - VYPR_OUTPUT_VERBOSE = inst_configuration.get("verbose") if inst_configuration.get("verbose") else True - PROJECT_ROOT = inst_configuration.get("project_root") if inst_configuration.get("project_root") else "" - - self.machine_id = ("%s-" % inst_configuration.get("machine_id")) if inst_configuration.get("machine_id") else "" + self.machine_id = ("%s-" % inst_configuration.get("machine_id")) if inst_configuration.get( + "machine_id") else "" # check if there's an NTP server given that we should use for time self.ntp_server = inst_configuration.get("ntp_server") @@ -563,45 +731,14 @@ def initialise(self, flask_object): print("Couldn't set time based on NTP server '%s'." % self.ntp_server) exit() - if flask_object: - def prepare_vypr(): - import datetime - # this function runs inside a request, so flask.g exists - # we store just the request time - flask.g.request_time = datetime.datetime.now() - - flask_object.before_request(prepare_vypr) - - # add VyPR end points - we may use this for statistics collection on the server - # add the safe exist end point - @flask_object.route("/vypr/stop-monitoring/") - def endpoint_stop_monitoring(): - from app import vypr - # send end-monitoring message - vypr.end_monitoring() - # wait for the thread to end - vypr.consumption_thread.join() - return "VyPR monitoring thread exited. The server must be restarted to turn monitoring back on.\n" - - @flask_object.route("/vypr/pause-monitoring/") - def endpoint_pause_monitoring(): - from app import vypr - vypr.pause_monitoring() - return "VyPR monitoring paused - thread is still running.\n" - - @flask_object.route("/vypr/resume-monitoring/") - def endpoint_resume_monitoring(): - from app import vypr - vypr.resume_monitoring() - return "VyPR monitoring resumed.\n" - # set up the maps that the monitoring algorithm that the consumption thread runs # we need the list of functions that we have instrumentation data from, so read the instrumentation maps # directory dump_files = filter(lambda filename: ".dump" in filename, os.listdir(os.path.join(PROJECT_ROOT, "binding_spaces"))) - functions_and_properties = map(lambda function_dump_file: function_dump_file.replace(".dump", ""), dump_files) + functions_and_properties = map(lambda function_dump_file: function_dump_file.replace(".dump", ""), + dump_files) tokens = map(lambda string: string.split("-"), functions_and_properties) self.function_to_maps = {} @@ -631,20 +768,93 @@ def endpoint_resume_monitoring(): vypr_output(self.function_to_maps) - vypr_output("Setting up monitoring thread.") + def initialise(self, flask_object=None): + + vypr_output("Initialising VyPR alongside service.") + + if flask_object: + if VYPR_MODULE != "": + # if a VyPR module is given, this means VyPR will be running between requests + + def prepare_vypr(): + import datetime + from app import vypr + # this function runs inside a request, so flask.g exists + # we store just the request time + flask.g.request_time = vypr.get_time() + + if flask_object != None: + flask_object.before_request(prepare_vypr) + + # add VyPR end points - we may use this for statistics collection on the server + # add the safe exist end point + @flask_object.route("/vypr/stop-monitoring/") + def endpoint_stop_monitoring(): + from app import vypr + # send end-monitoring message + vypr.end_monitoring() + # wait for the thread to end + vypr.consumption_thread.join() + return "VyPR monitoring thread exited. The server must be restarted to turn monitoring back on.\n" + + @flask_object.route("/vypr/pause-monitoring/") + def endpoint_pause_monitoring(): + from app import vypr + vypr.pause_monitoring() + return "VyPR monitoring paused - thread is still running.\n" + + @flask_object.route("/vypr/resume-monitoring/") + def endpoint_resume_monitoring(): + from app import vypr + vypr.resume_monitoring() + return "VyPR monitoring resumed.\n" + + + # setup consumption queue and store it globally across requests + + else: + # if no VyPR module is given, this means VyPR will have to run per request + + def start_vypr(): + # setup consumption queue and store it within the request context + from flask import g + self.consumption_queue = Queue() + # setup consumption thread + self.consumption_thread = threading.Thread( + target=consumption_thread_function, + args=[self] + ) + # store vypr object in request context + g.vypr = self + self.consumption_thread.start() + g.request_time = g.vypr.get_time() + + if flask_object != None: + flask_object.before_request(start_vypr) + + # set up tear down function + + def stop_vypr(e): + # send kill message to consumption thread + # for now, we don't wait for the thread to end + from flask import g + g.vypr.end_monitoring() + + if flask_object != None: + flask_object.teardown_request(stop_vypr) - # setup consumption queue and store it globally across requests self.consumption_queue = Queue() # setup consumption thread self.consumption_thread = threading.Thread( target=consumption_thread_function, args=[self] - ) + ) self.consumption_thread.start() vypr_output("VyPR monitoring initialisation finished.") - def get_time(self): + + def get_time(self, callee=""): """ Returns either the machine local time, or the NTP time (using the initial NTP time obtained when VyPR started up, so we don't query an NTP server everytime we want to measure time). @@ -660,7 +870,7 @@ def get_time(self): current_ntp_time = self.ntp_start_time + difference return current_ntp_time else: - vypr_output("Getting time based on local machine.") + vypr_output("Getting time based on local machine - %s" % callee) return datetime.datetime.utcnow() def send_event(self, event_description): @@ -669,6 +879,7 @@ def send_event(self, event_description): def end_monitoring(self): if not (self.initialisation_failure): + print ("End monitoring signal") vypr_output("Ending VyPR monitoring thread.") self.consumption_queue.put(("end-monitoring",)) @@ -681,3 +892,9 @@ def resume_monitoring(self): if not (self.initialisation_failure): vypr_output("Sending monitoring resume message.") self.consumption_queue.put(("inactive-monitoring-stop",)) + + def get_test_result_in_flask(self,className, methodName, result): + print("Got the name and the status of the test {} {} {}".format(className, methodName, result)) + + + diff --git a/instrument.py b/instrument.py index c076e61..04dcead 100644 --- a/instrument.py +++ b/instrument.py @@ -17,6 +17,8 @@ import py_compile import time +from os.path import dirname, abspath + # for now, we remove the final occurrence of VyPR from the first path to look in for modules rindex = sys.path[0].rfind("/VyPR") sys.path[0] = sys.path[0][:rindex] + sys.path[0][rindex + len("/VyPR"):] @@ -32,8 +34,150 @@ BYTECODE_EXTENSION = ".pyc" vypr_module = "." VERIFICATION_INSTRUCTION = "verification.send_event" +TEST_FRAMEWORK = False LOGS_TO_STDOUT = False +""" +Specification compilation. +""" + + +def get_function_asts_in_module(module_ast): + """ + Given a Module AST object, traverse it and find all the functions. + :param module_ast: + :return: List of function names. + """ + all_function_names = [] + # map elements of ast to pairs - left hand side is module path, right hand side is ast object + stack = list(map(lambda item : ("", item), module_ast.body)) + while len(stack) > 0: + top = stack.pop() + module_path = top[0] + ast_obj = top[1] + if type(ast_obj) is ast.FunctionDef: + all_function_names.append(("%s%s" % (top[0], top[1].name), top[1])) + elif hasattr(ast_obj, "body"): + if type(ast_obj) is ast.If: + stack += map( + lambda item : (module_path, item), + ast_obj.body + ) + elif type(ast_obj) is ast.ClassDef: + stack += map( + lambda item: ("%s%s%s:" % + (module_path, "." if (module_path != "" and module_path[-1] != ":") else "", + ast_obj.name), item), + ast_obj.body + ) + return all_function_names + +def compile_queries(specification_file): + """ + Given a specification file, complete the syntax and add imports, then inspect the objects + used as keys to build the final dictionary structure. + :param specification_file: + :return: fully-expanded dictionary structure + """ + logger.log("Compiling queries...") + + # load in verification config file + # to do this, we read in the existing one, write a temporary one with imports added and import that one + # this is to allow users to write specifications without caring about importing anything from QueryBuilding + # when we read in the original specification code, we add verification_conf = {} to turn it into valid specification + # syntax + specification_code = "verification_conf = %s" % open(specification_file, "r").read() + # replace empty lists with a fake property + fake_property = "[Forall(q = changes('fake_vypr_var')).Check(lambda q : q('fake_vypr_var').equals(True))]" + specification_code = specification_code.replace("[]", fake_property) + with_imports = "from VyPR.QueryBuilding import *\n%s" % specification_code + with open("VyPR_queries_with_imports.py", "w") as h: + h.write(with_imports) + + # we now import the specification file + try: + from VyPR_queries_with_imports import verification_conf + except AttributeError: + print("Cannot continue with instrumentation - " + "looks like you tried to call a non-existent method on an object!\n") + print(traceback.format_exc()) + exit() + except: + # check for errors in the specification + print(traceback.format_exc()) + exit() + + + # this hierarchy will be populated as functions are found in the project that satisfy requirements + compiled_hierarchy = {} + + # finally, we process the keys of the verification_conf dictionary + # these keys are objects representing searches we should perform to generate the final expanded specification + # with fully-qualified module names + # we have this initial step to enable developers to write more sophisticated selection criteria the functions + # to which they want to apply a query + + # we go through each function in the project we're instrumenting, check if there's a key in the initial + # configuration file whose criteria are fulfilled by the function and, if so, add to the hierarchy + for (root, directories, files) in os.walk("."): + for file in files: + # read in the file, traverse its AST structure to find all the functions and then determine + # whether it satisfies a function selector + # only consider Python files + filename = os.path.join(root, file) + module_name = "%s.%s" % (root[1:].replace("/", ""), file.replace(".py", "")) + if (filename[-3:] == ".py" + and "VyPR" not in filename + and "venv" not in filename): + # traverse the AST structure + code = open(filename, "r").read() + module_asts = ast.parse(code) + function_asts = get_function_asts_in_module(module_asts) + # process each function + for (function_name, function_ast) in function_asts: + # construct the SCFG + scfg = CFG() + scfg.process_block(function_ast.body) + # process each function selector + for function_selector in verification_conf: + if type(function_selector) is Functions: + if function_selector.is_satisfied_by(function_ast, scfg): + # add to the compiled hierarchy + if not(compiled_hierarchy.get(module_name)): + compiled_hierarchy[module_name] = {} + if not(compiled_hierarchy[module_name].get(function_name)): + compiled_hierarchy[module_name][function_name] = verification_conf[function_selector] + else: + compiled_hierarchy[module_name][function_name] += verification_conf[function_selector] + elif type(function_selector) is Module: + if (module_name == function_selector._module_name + and function_name == function_selector._function_name): + # add to the final hierarchy + if not (compiled_hierarchy.get(module_name)): + compiled_hierarchy[module_name] = {} + if not (compiled_hierarchy[module_name].get(function_name)): + compiled_hierarchy[module_name][function_name] = verification_conf[function_selector] + else: + compiled_hierarchy[module_name][function_name] += verification_conf[function_selector] + + # now merge the specifications written for specific functions with the compiled specifications + for top_level in verification_conf: + if type(top_level) is str: + if compiled_hierarchy.get(top_level): + for bottom_level in verification_conf[top_level]: + # if top_level was a string, for now bottom_level will be as well + # check whether the compiled part of the specification has already assigned a property here + if compiled_hierarchy.get(top_level) and compiled_hierarchy[top_level].get(bottom_level): + compiled_hierarchy[top_level][bottom_level] += verification_conf[top_level][bottom_level] + else: + compiled_hierarchy[top_level][bottom_level] = verification_conf[top_level][bottom_level] + else: + compiled_hierarchy[top_level] = {} + for bottom_level in verification_conf[top_level]: + compiled_hierarchy[top_level][bottom_level] = verification_conf[top_level][bottom_level] + + return compiled_hierarchy + class InstrumentationLog(object): """ @@ -159,7 +303,6 @@ def compute_binding_space(quantifier_sequence, scfg, reachability_map, current_b vertex._structure_obj.target.id == variable_changed): # the variable we're looking for was found as a simple loop variable qd.append(vertex) - print("adding loop vertex to static binding") elif (type(vertex._structure_obj.target) is ast.Tuple and variable_changed in list(map(lambda item: item.id, vertex._structure_obj.target))): # the loop variable we're looking for was found inside a tuple @@ -339,10 +482,23 @@ def read_configuration(file): """ Read in 'file', parse into an object and return. """ - with open(file, "r") as h: - contents = h.read() + content = "" + skip = False + for line in open(file): + li = line.strip() + + # Handle multi-line comments + if li.startswith("/*"): + skip = True + if li.endswith("*/"): + skip = False + continue + + if not (li.startswith("#") or li.startswith("//")) and not skip: + content += line + + return json.loads(content) - return json.loads(contents) def get_instrumentation_points_from_comp_sequence(value_from_binding, moves): @@ -373,7 +529,6 @@ def get_instrumentation_points_from_comp_sequence(value_from_binding, moves): return instrumentation_points - def instrument_point_state(state, name, point, binding_space_indices, atom_index, atom_sub_index, instrumentation_point_db_ids, measure_attribute=None): @@ -387,21 +542,29 @@ def instrument_point_state(state, name, point, binding_space_indices, if measure_attribute == "length": state_variable_alias = name.replace(".", "_").replace("(", "__").replace(")", "__") state_recording_instrument = "record_state_%s = len(%s); " % (state_variable_alias, name) - time_attained_instrument = "time_attained_%s = vypr.get_time();" % state_variable_alias + time_attained_instrument = "time_attained_%s = %s.get_time('point instrument');" %\ + (state_variable_alias, VYPR_OBJ) + time_attained_variable = "time_attained_%s" % state_variable_alias elif measure_attribute == "type": state_variable_alias = name.replace(".", "_").replace("(", "__").replace(")", "__") state_recording_instrument = "record_state_%s = type(%s).__name__; " % (state_variable_alias, name) - time_attained_instrument = "time_attained_%s = vypr.get_time();" % state_variable_alias + time_attained_instrument = "time_attained_%s = %s.get_time('point instrument');" %\ + (state_variable_alias, VYPR_OBJ) + time_attained_variable = "time_attained_%s" % state_variable_alias elif measure_attribute == "time_attained": state_variable_alias = "time_attained_%i" % atom_sub_index - state_recording_instrument = "record_state_%s = vypr.get_time(); " % state_variable_alias + state_recording_instrument = "record_state_%s = %s.get_time('point instrument'); " %\ + (state_variable_alias, VYPR_OBJ) time_attained_instrument = state_recording_instrument + time_attained_variable = "record_state_%s" % state_variable_alias # the only purpose here is to match what is expected in the monitoring algorithm name = "time" else: state_variable_alias = name.replace(".", "_").replace("(", "__").replace(")", "__") state_recording_instrument = "record_state_%s = %s; " % (state_variable_alias, name) - time_attained_instrument = "time_attained_%s = vypr.get_time();" % state_variable_alias + time_attained_instrument = "time_attained_%s = %s.get_time('point instrument');" %\ + (state_variable_alias, VYPR_OBJ) + time_attained_variable = "time_attained_%s" % state_variable_alias # note that observed_value is used three times: # 1) to capture the time attained by the state for checking of a property - this is duplicated @@ -419,7 +582,7 @@ def instrument_point_state(state, name, point, binding_space_indices, atom_sub_index=atom_sub_index, instrumentation_point_db_id=instrumentation_point_db_ids, atom_program_variable=name, - time_attained = ("time_attained_%s" % state_variable_alias), + time_attained=time_attained_variable, observed_value=("record_state_%s" % state_variable_alias) ) state_recording_instrument += "%s((%s))" % (VERIFICATION_INSTRUCTION, instrument_tuple) @@ -518,8 +681,8 @@ def instrument_point_transition(atom, point, binding_space_indices, atom_index, else: state_dict = "{}" - timer_start_statement = "__timer_s = vypr.get_time()" - timer_end_statement = "__timer_e = vypr.get_time()" + timer_start_statement = "__timer_s = %s.get_time('transition instrument')" % VYPR_OBJ + timer_end_statement = "__timer_e = %s.get_time('transition instrument')" % VYPR_OBJ time_difference_statement = "__duration = __timer_e - __timer_s; " instrument_tuple = ("'{formula_hash}', 'instrument', '{function_qualifier}', {binding_space_index}," + @@ -741,38 +904,55 @@ def place_path_recording_instruments(scfg, instrument_function_qualifier, formul logger.log("=" * 100) -def place_function_begin_instruments(function_def, formula_hash, instrument_function_qualifier): +def place_function_begin_instruments(function_def, formula_hashes, instrument_function_qualifier): # NOTE: only problem with this is that the "end" instrument is inserted before the return, # so a function call in the return statement maybe missed if it's part of verification... thread_id_capture = "import threading; __thread_id = threading.current_thread().ident;" - vypr_start_time_instrument = "vypr_start_time = vypr.get_time();" + vypr_start_time_instrument = "vypr_start_time = %s.get_time('begin instrument');" % VYPR_OBJ + verification_test_start_code = "start_test_time = vypr_dt.now()" + formula_hashes = ",".join(map(lambda hash : "'%s'" % hash, formula_hashes)) + formula_hashes_as_list = "[%s]" % formula_hashes start_instrument = \ - "%s((\"%s\", \"function\", \"%s\", \"start\", vypr_start_time, \"%s\", __thread_id))" \ - % (VERIFICATION_INSTRUCTION, formula_hash, instrument_function_qualifier, formula_hash) + "%s((\"function\", %s, \"%s\", \"start\", vypr_start_time, \"%s\", __thread_id))" \ + % (VERIFICATION_INSTRUCTION, formula_hashes_as_list, instrument_function_qualifier, formula_hash) + verfication_test_start_time_ast = ast.parse(verification_test_start_code).body[0] threading_import_ast = ast.parse(thread_id_capture).body[0] thread_id_capture_ast = ast.parse(thread_id_capture).body[1] vypr_start_time_ast = ast.parse(vypr_start_time_instrument).body[0] start_ast = ast.parse(start_instrument).body[0] + verfication_test_start_time_ast.lineno = function_def.body[0].lineno threading_import_ast.lineno = function_def.body[0].lineno thread_id_capture_ast.lineno = function_def.body[0].lineno vypr_start_time_ast.lineno = function_def.body[0].lineno start_ast.lineno = function_def.body[0].lineno + function_def.body.insert(0,verfication_test_start_time_ast) function_def.body.insert(0, start_ast) function_def.body.insert(0, thread_id_capture_ast) function_def.body.insert(0, threading_import_ast) function_def.body.insert(0, vypr_start_time_ast) -def place_function_end_instruments(function_def, scfg, formula_hash, instrument_function_qualifier): +def place_function_end_instruments(function_def, scfg, formula_hashes, instrument_function_qualifier, is_flask): # insert the end instrument before every return statement + formula_hashes = ",".join(map(lambda hash : "'%s'" % hash, formula_hashes)) + formula_hashes_as_list = "[%s]" % formula_hashes + for end_vertex in scfg.return_statements: + end_instrument = \ - "%s((\"%s\", \"function\", \"%s\", \"end\", flask.g.request_time, \"%s\", __thread_id, " \ - "vypr.get_time()))" \ - % (VERIFICATION_INSTRUCTION, formula_hash, instrument_function_qualifier, formula_hash) + "%s((\"function\", %s, \"%s\", \"end\", flask.g.request_time, \"%s\", __thread_id, " \ + "%s.get_time('end instrument')))" \ + % ( + VERIFICATION_INSTRUCTION, + formula_hashes_as_list, + instrument_function_qualifier, + formula_hash, + VYPR_OBJ + ) + end_ast = ast.parse(end_instrument).body[0] end_ast.lineno = end_vertex._previous_edge._instruction._parent_body[-1].lineno @@ -787,19 +967,236 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ # if the last instruction in the ast is not a return statement, add an end instrument at the end if not (type(function_def.body[-1]) is ast.Return): - end_instrument = "%s((\"%s\", \"function\", \"%s\", \"end\", flask.g.request_time, \"%s\", __thread_id, " \ - "vypr.get_time()))" \ - % (VERIFICATION_INSTRUCTION, formula_hash, instrument_function_qualifier, - formula_hash) + end_instrument = "%s((\"function\", %s, \"%s\", \"end\", flask.g.request_time, \"%s\", __thread_id, " \ + "%s.get_time('end instrument')))" \ + % (VERIFICATION_INSTRUCTION, formula_hashes_as_list, instrument_function_qualifier, + formula_hash, VYPR_OBJ) + + end_ast = ast.parse(end_instrument).body[0] + + # In case of test, there is no return instruction therefore we add the test_status instruction after the end instruction + logger.log("Placing end instrument at the end of the function body.") function_def.body.insert(len(function_def.body), end_ast) + + + +def instrument_modules(module_list, formula_hash, instrument_function_qualifier): + + for module in module_list: + + + if module.endswith('.py'): + ext = '.py' + elif module.endswith('.inst'): + ext = '.py.inst' + + file_name = module + + file_name_without_extension = module.replace(ext, "") + + + # extract asts from the code in the file + code = "".join(open(file_name, "r").readlines()) + + asts = ast.parse(code) + + for node in asts.body: + if type(node) == ast.ClassDef: + class_name = node.name + + create_test_setclass_method(asts.body, class_name) + + instrument_test_cases(asts, class_name, formula_hash, instrument_function_qualifier) + + + # compile bytecode + compile_bytecode_and_write(asts,file_name_without_extension) + + + +def instrument_test_cases(test_ast, class_name, formula_hash, instrument_function_qualifier): + + ## Adding imports first to the test cases + + import_code = "from %s import vypr" % VYPR_MODULE + vypr_add_import = 'from %s import vypr' % VYPR_MODULE +# datetime_import = 'from datetime import datetime as vypr_dt' + + import_vypr_add_ast = ast.parse(vypr_add_import).body[0] + import_vypr_add_ast.lineno = test_ast.body[0].lineno + import_vypr_add_ast.col_offset = test_ast.body[0].col_offset + + +# datetime_import_ast = ast.parse(datetime_import).body[0] +# datetime_import_ast.lineno = test_ast.body[0].lineno +# datetime_import_ast.col_offset = test_ast.body[0].col_offset + + test_ast.body.insert(0, import_vypr_add_ast) + test_ast.body.insert(0, datetime_import_ast) + + + + start_test_time_statement = "test_start_time = vypr.get_time()" + end_test_time_statement = \ + "%s((\"%s\",\"test_status\", \"%s\",self._resultForDoCleanups, test_start_time, vypr.get_time(), \"%s\", self._testMethodName, ))" % \ + (VERIFICATION_INSTRUCTION, formula_hash, instrument_function_qualifier, formula_hash + ) + + + ## Finding the test class. + current_step = filter( lambda entry: (type(entry) is ast.ClassDef and + entry.name == class_name), test_ast.body)[0] + + + test_class_body = current_step.body + + + + ## Traversing the body of the class in order to look for setUpClass method + + for test_function in test_class_body: + + + + + # We only want to instrument test cases + if not (type(test_function) is ast.FunctionDef) or test_function.name in ['setUpClass', 'setUp', 'tearDown']: + continue + + + setup_transaction = ast.parse(start_test_time_statement).body[0] + test_function.body.insert(0,setup_transaction) + + + test_status_ast = ast.parse(end_test_time_statement).body[0] + logger.log("Placing test_status instrument at the end of the function body.") + test_function.body.insert(len(function_def.body), test_status_ast) + + + + + +def get_test_modules(is_test_module , module = None): + + + from os.path import dirname, abspath + + ROOT_DIR = dirname(dirname(abspath(__file__))) + + module_path = [] + + path = ROOT_DIR+'/' + TEST_DIR + + + + #for r, d, f in os.walk(os.environ('PATH')): + for r, d, f in os.walk(path): + + for file in f: + + if file.startswith("test_") and (file.endswith('.py') or file.endswith('.py.inst')): + + if file == module[module.rindex('.')+1:]+'.py' and is_test_module: + continue + + module_path.append(os.path.join(r, file)) + + + return module_path + + +def create_test_setclass_method(current_step, class_name): + """ + :param enable_normal_testing: Checks whether the testing is "normal" of "flask" based. + :param current_step: Contains the AST for the code + :param class_name: Name of the test class + """ + + setUp_found = False + + ## Finding the test class. + current_step = filter( lambda entry: (type(entry) is ast.ClassDef and + entry.name == class_name), current_step)[0] + + + test_class_body = current_step.body + + transaction_time_statement = "%s((\"test_transaction\", vypr.get_time() ))" % \ + (VERIFICATION_INSTRUCTION) + + + ## Traversing the body of the class in order to look for setUpClass method + + for test_function in test_class_body: + + if not (type(test_function) is ast.FunctionDef): + continue + + if test_function.name == 'setUpClass': + + setUp_found = True + + setup_transaction = ast.parse(transaction_time_statement).body[0] + test_function.body.insert(0,setup_transaction) + + # If there is no setUpClass method, then we need to add setUp method in the class. + if not setUp_found: + + setUp_method = "@classmethod\ndef setUpClass(cls):\n\t" + transaction_time_statement + + method_inst = ast.parse(setUp_method).body[0] + test_class_body.insert(0,method_inst) + + + +def if_file_is_test(name): + + test_path = dirname(dirname(abspath(__file__))) + '/' + TEST_DIR + + + for root, dirs, files in os.walk(test_path): + + test_file = name[name.rindex('/')+1:] + + if test_file in files: + return True + + return False + + +def if_file_is_flask(name): + + file = open(name, 'r') + + data = file.readlines() + + for line in data: + + stripped_line = line.strip() + + + + if 'from flask' in stripped_line: + return True + + + return False + + + if __name__ == "__main__": + + + # import pdb; pdb.set_trace() + + parser = argparse.ArgumentParser(description='Instrumentation for VyPR.') parser.add_argument('--verbose', action='store_true', help='If given, output will be turned on for the instrumentation module.', required=False) @@ -825,10 +1222,41 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ EXPLANATION = inst_configuration.get("explanation") == "on" BYTECODE_EXTENSION = inst_configuration.get("bytecode_extension") \ if inst_configuration.get("bytecode_extension") else ".pyc" + PROJECT_ROOT = inst_configuration.get("project_root") \ + if inst_configuration.get("project_root") else "" + USE_FLASK = inst_configuration.get("use_flask") \ + if inst_configuration.get("use_flask") else "no" + VERIFICATION_INSTRUCTION = inst_configuration.get("verification_instruction") \ + if inst_configuration.get("verification_instruction") else "verification.send_event" + TEST_FRAMEWORK = inst_configuration.get("test") \ + if inst_configuration.get("test") else "" + + + VYPR_MODULE = inst_configuration.get("vypr_module") \ if inst_configuration.get("vypr_module") else "" + + # if VYPR_MODULE is empty, we assume that the central object + # will be accessible in the request context + if VYPR_MODULE == "": + VYPR_OBJECT = "g.vypr" + else: + VYPR_OBJECT = "vypr" + VERIFICATION_INSTRUCTION = "vypr.send_event" - # VERIFICATION_INSTRUCTION = "print" + + + # If testing is set then we should specify the test module + if TEST_FRAMEWORK in ['yes']: + TEST_DIR = inst_configuration.get("test_module") \ + if inst_configuration.get("test_module") else '' + + if TEST_DIR != '': + VYPR_MODULE = TEST_DIR + else: + print ('Specify test module. Ending instrumentation - nothing has been done') + exit() + machine_id = ("%s-" % inst_configuration.get("machine_id")) if inst_configuration.get("machine_id") else "" @@ -837,6 +1265,9 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ print("Verdict server is not reachable. Ending instrumentation - nothing has been done.") exit() + SETUP_ONCE = False + + # initialise instrumentation logger logger = InstrumentationLog(LOGS_TO_STDOUT) # set up the file handle @@ -854,18 +1285,23 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ os.remove(f.replace(".py.inst", BYTECODE_EXTENSION)) logger.log("Reset file %s to uninstrumented version." % f) + for directory in os.walk("."): + if directory == "binding_spaces": + for file in directory[2]: + try: + os.remove(file) + except: + print("Could not remove file '%s' from dump directories. Stopping instrumentation." % file) + exit() + + + + logger.log("Importing PyCFTL queries...") # load in verification config file # to do this, we read in the existing one, write a temporary one with imports added and import that one # this is to allow users to write specifications without caring about importing anything from QueryBuilding - specification_code = open("VyPR_queries.py", "r").read() - # replace empty lists with a fake property - fake_property = "[Forall(q = changes('fake_vypr_var')).Check(lambda q : q('fake_vypr_var').equals(True))]" - specification_code = specification_code.replace("[]", fake_property) - with_imports = "from VyPR.QueryBuilding import *\n%s" % specification_code - with open("VyPR_queries_with_imports.py", "w") as h: - h.write(with_imports) - from VyPR_queries_with_imports import verification_conf + verification_conf = compile_queries("VyPR_queries.py") verified_modules = verification_conf.keys() @@ -873,6 +1309,20 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ for module in verified_modules: + # If we are writing specification over tests + is_test_module = False + + # Check if the file is flask or not to select the appropriate timestamp for flask + is_flask = False + + + # Reset the instructions + VERIFICATION_INSTRUCTION = "vypr.send_event" + + # VERIFICATION_INSTRUCTION = "print" + VYPR_OBJ = "vypr" + + logger.log("Processing module '%s'." % module) verified_functions = verification_conf[module].keys() @@ -880,16 +1330,24 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ file_name = module.replace(".", "/") + ".py" file_name_without_extension = module.replace(".", "/") + + # Instrument test cases with 'test_status' instrumentation type + + if if_file_is_test(file_name): + is_test_module = True + + + + if if_file_is_flask(file_name): + is_flask = True + # extract asts from the code in the file code = "".join(open(file_name, "r").readlines()) asts = ast.parse(code) + # add import for init_vypr module - import_code = "from %s import vypr" % VYPR_MODULE - import_ast = ast.parse(import_code).body[0] - import_ast.lineno = asts.body[0].lineno - import_ast.col_offset = asts.body[0].col_offset - asts.body.insert(0, import_ast) + # For normal testing we don't need to add this to the test class file # add vypr datetime import vypr_datetime_import = "from datetime import datetime as vypr_dt" @@ -898,16 +1356,31 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ datetime_import_ast.col_offset = asts.body[0].col_offset asts.body.insert(0, datetime_import_ast) - # if we're using flask, we assume a certain architecture + + import_code = "from %s import vypr" % VYPR_MODULE + #import_code = "from test import vypr" + import_ast = ast.parse(import_code).body[0] + import_ast.lineno = asts.body[0].lineno + import_ast.col_offset = asts.body[0].col_offset + asts.body.insert(0, import_ast) + import_code = "import flask" import_asts = ast.parse(import_code) flask_import = import_asts.body[0] asts.body.insert(0, flask_import) + + + + # if we're using flask, we assume a certain architecture + + for function in verified_functions: logger.log("Processing function '%s'." % function) + + # we replace . with : in function definitions to make sure we can distinguish between module # and class navigation later on instrument_function_qualifier = "%s%s.%s" % (machine_id, module, function.replace(".", ":")) @@ -953,6 +1426,9 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ scfg = CFG(reference_variables=reference_variables) scfg_vertices = scfg.process_block(function_def.body) + import pprint + pprint.pprint(scfg.branch_initial_statements) + top_level_block = function_def.body logger.log("SCFG constructed.") @@ -964,6 +1440,8 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ # for each property, instrument the function for that property + property_hashes = [] + for (formula_index, formula_structure) in enumerate(verification_conf[module][function]): logger.log("Instrumenting for PyCFTL formula %s" % formula_structure) @@ -987,6 +1465,8 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ map(lambda item: base64.encodestring(pickle.dumps(item)).decode('ascii'), atoms) ) + property_hashes.append(formula_hash) + # note that this also means giving an empty list [] will result in path instrumentation # without property instrumentation if EXPLANATION: @@ -1004,7 +1484,6 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ reachability_map = construct_reachability_map(scfg) bindings = compute_binding_space(formula_structure, scfg, reachability_map) - print(bindings) logger.log("Set of static bindings computed is") logger.log(str(bindings)) @@ -1023,7 +1502,8 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ "function": instrument_function_qualifier, "serialised_formula_structure": serialised_formula_structure, "serialised_bind_variables": serialised_bind_variables, - "serialised_atom_list": list(enumerate(serialised_atom_list)) + "serialised_atom_list": list(enumerate(serialised_atom_list)), + "formula_index": formula_index } # send instrumentation data to the verdict database @@ -1064,7 +1544,8 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ binding_dictionary = { "binding_space_index": m, "function": function_id, - "binding_statement_lines": line_numbers + "binding_statement_lines": line_numbers, + "property_hash": formula_hash } serialised_binding_dictionary = json.dumps(binding_dictionary) try: @@ -1086,12 +1567,7 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ static_qd_to_point_map[m][atom_index] = {} - if type(atom) in [formula_tree.StateValueEqualToMixed, - formula_tree.TransitionDurationLessThanTransitionDurationMixed, - formula_tree.TransitionDurationLessThanStateValueMixed, - formula_tree.TransitionDurationLessThanStateValueLengthMixed, - formula_tree.TimeBetweenInInterval, - formula_tree.TimeBetweenInOpenInterval]: + if formula_tree.is_mixed_atom(atom): # there may be multiple bind variables composition_sequences = derive_composition_sequence(atom) @@ -1256,28 +1732,31 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ binding_space_indices = list_of_lists[0] instrumentation_point_db_ids = list_of_lists[1] - if type(atom) is formula_tree.TransitionDurationInInterval: + if type(atom) in [formula_tree.TransitionDurationInInterval, + formula_tree.TransitionDurationInOpenInterval]: instrument_point_transition(atom, point, binding_space_indices, atom_index, - atom_sub_index, instrumentation_point_db_ids) + atom_sub_index, instrumentation_point_db_ids) - elif type(atom) in [formula_tree.StateValueInInterval, formula_tree.StateValueEqualTo, - formula_tree.StateValueInOpenInterval]: + elif type(atom) in [formula_tree.StateValueInInterval, + formula_tree.StateValueEqualTo, + formula_tree.StateValueInOpenInterval]: instrument_point_state(atom._state, atom._name, point, binding_space_indices, - atom_index, atom_sub_index, instrumentation_point_db_ids) + atom_index, atom_sub_index, instrumentation_point_db_ids) elif type(atom) is formula_tree.StateValueTypeEqualTo: instrument_point_state(atom._state, atom._name, point, binding_space_indices, - atom_index, atom_sub_index, instrumentation_point_db_ids, - measure_attribute="type") + atom_index, atom_sub_index, instrumentation_point_db_ids, + measure_attribute="type") - elif type(atom) in [formula_tree.StateValueLengthInInterval]: - """ - Instrumentation for the length of a value given is different - because we have to add len() to the instrument. + elif type(atom) in [formula_tree.StateValueLengthInInterval, + formula_tree.StateValueLengthInOpenInterval]: """ + Instrumentation for the length of a value given is different + because we have to add len() to the instrument. + """ instrument_point_state(atom._state, atom._name, point, binding_space_indices, atom_index, atom_sub_index, instrumentation_point_db_ids, @@ -1285,7 +1764,7 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ elif type(atom) in [formula_tree.StateValueEqualToMixed]: """We're instrumenting multiple states, so we need to perform instrumentation on two - separate points. """ + separate points. """ # for each side of the atom (LHS and RHS), instrument the necessary points @@ -1304,30 +1783,32 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ instrument_point_state(atom._rhs, atom._rhs_name, point, binding_space_indices, atom_index, atom_sub_index, instrumentation_point_db_ids) - elif type(atom) is formula_tree.TransitionDurationLessThanTransitionDurationMixed: - """We're instrumenting multiple transitions, so we need to perform instrumentation on - two separate points. """ + elif type(atom) in [formula_tree.StateValueLengthLessThanStateValueLengthMixed, + formula_tree.StateValueLengthLessThanEqualStateValueLengthMixed]: + """We're instrumenting multiple states, so we need to perform instrumentation on two + separate points. """ # for each side of the atom (LHS and RHS), instrument the necessary points logger.log( - "Instrumenting for a mixed atom %s with sub atom index %i." % (atom, atom_sub_index) + "instrumenting for a mixed atom %s with sub atom index %i" % (atom, atom_sub_index) ) if atom_sub_index == 0: # we're instrumenting for the lhs - logger.log("placing lhs instrument for scfg object %s" % atom._lhs) - instrument_point_transition(atom, point, binding_space_indices, - atom_index, atom_sub_index, - instrumentation_point_db_ids) + logger.log("Placing left-hand-side instrument for SCFG object %s." % atom._lhs) + instrument_point_state(atom._lhs, atom._lhs_name, point, binding_space_indices, + atom_index, atom_sub_index, instrumentation_point_db_ids, + measure_attribute="length") else: # we're instrumenting for the rhs - logger.log("placing rhs instrument for scfg object %s" % atom._rhs) - instrument_point_transition(atom, point, binding_space_indices, - atom_index, atom_sub_index, - instrumentation_point_db_ids) + logger.log("Placing right-hand-side instrument for SCFG object %s." % atom._rhs) + instrument_point_state(atom._rhs, atom._rhs_name, point, binding_space_indices, + atom_index, atom_sub_index, instrumentation_point_db_ids, + measure_attribute="length") - elif type(atom) is formula_tree.TransitionDurationLessThanStateValueMixed: + elif type(atom) in [formula_tree.TransitionDurationLessThanTransitionDurationMixed, + formula_tree.TransitionDurationLessThanEqualTransitionDurationMixed]: """We're instrumenting multiple transitions, so we need to perform instrumentation on two separate points. """ @@ -1349,9 +1830,10 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ instrument_point_state(atom._rhs, atom._rhs_name, point, binding_space_indices, atom_index, atom_sub_index, instrumentation_point_db_ids) - elif type(atom) is formula_tree.TransitionDurationLessThanStateValueLengthMixed: + elif type(atom) in [formula_tree.TransitionDurationLessThanStateValueLengthMixed, + formula_tree.TransitionDurationLessThanEqualStateValueLengthMixed]: """We're instrumenting multiple transitions, so we need to perform instrumentation on - two separate points. """ + two separate points. """ # for each side of the atom (LHS and RHS), instrument the necessary points @@ -1375,7 +1857,7 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ elif type(atom) in [formula_tree.TimeBetweenInInterval, formula_tree.TimeBetweenInOpenInterval]: """We're instrumenting multiple transitions, so we need to perform instrumentation on - two separate points. """ + two separate points. """ # for each side of the atom (LHS and RHS), instrument the necessary points @@ -1398,22 +1880,35 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ # finally, insert an instrument at the beginning to tell the monitoring thread that a new call of the # function has started and insert one at the end to signal a return - place_function_begin_instruments(function_def, formula_hash, instrument_function_qualifier) + place_function_begin_instruments(function_def, property_hashes, instrument_function_qualifier) # also insert instruments at the end(s) of the function - place_function_end_instruments(function_def, scfg, formula_hash, instrument_function_qualifier) + place_function_end_instruments(function_def, scfg, property_hashes, instrument_function_qualifier, is_flask) + + if not SETUP_ONCE: + test_modules = get_test_modules(is_test_module, module) + instrument_modules(test_modules, formula_hash, instrument_function_qualifier) + SETUP_ONCE = True + + if is_test_module: + for node in asts.body: + if type(node) == ast.ClassDef: + class_name = node.name + + instrument_test_cases(asts, class_name, formula_hash, instrument_function_qualifier) + + # write the instrumented scfg to a file instrumented_scfg = CFG() instrumented_scfg.process_block(top_level_block) write_scfg_to_file(instrumented_scfg, "%s-%s-%s-instrumented.gv" % - (file_name_without_extension.replace(".", ""), module.replace(".", "-"), - function.replace(".", "-"))) + (file_name_without_extension.replace(".", ""), module.replace(".", "-"), + function.replace(".", "-"))) # check for existence of directories for intermediate data and create them if not found if not (os.path.isdir("binding_spaces")): os.mkdir("binding_spaces") - if not (os.path.isdir("index_hash")): - os.mkdir("index_hash") + # pickle binding space pickled_binding_space = pickle.dumps(bindings) @@ -1433,6 +1928,10 @@ def place_function_end_instruments(function_def, scfg, formula_hash, instrument_ compile_bytecode_and_write(asts, file_name_without_extension) + # Generate a bytecode file only in case of flask-based testing + # if flask_status_dict['flask_status']: + # compile_bytecode_and_write(flask_test_file_ast,flask_test_file_without_extension) + logger.log("Instrumentation complete. If VyPR is imported and activated, monitoring will now work.") # close instrumentation log diff --git a/monitor_synthesis/formula_tree.py b/monitor_synthesis/formula_tree.py index 2dd4d2f..88bc7fe 100644 --- a/monitor_synthesis/formula_tree.py +++ b/monitor_synthesis/formula_tree.py @@ -120,11 +120,12 @@ def __init__(self, state, name, interval): self.verdict = None def __repr__(self): - return "(%s)(%s) in %s" % (self._state, self._name, self._interval) + return "(%s)(%s) in %s" % (self._state, self._name, self.d_interval) def __eq__(self, other_atom): - if type(other_atom) is StateValueInInterval: - return self._state == other_atom._state and self._name == other_atom._name and self._interval == other_atom._interval + if type(other_atom) is StateValueInOpenInterval: + return (self._state == other_atom._state and self._name == other_atom._name + and self._interval == other_atom._interval) else: return False @@ -151,7 +152,7 @@ def __repr__(self): def __eq__(self, other_atom): if type(other_atom) is StateValueEqualTo: - return (self._state == other_atom._state and self._name == other_atom._name \ + return (self._state == other_atom._state and self._name == other_atom._name and self._value == other_atom._value) else: return False @@ -176,7 +177,7 @@ def __repr__(self): def __eq__(self, other_atom): if type(other_atom) is StateValueTypeEqualTo: - return (self._state == other_atom._state and self._name == other_atom._name \ + return (self._state == other_atom._state and self._name == other_atom._name and self._value == other_atom._value) else: return False @@ -203,7 +204,9 @@ def __repr__(self): def __eq__(self, other_atom): if type(other_atom) is StateValueEqualToMixed: return (self._lhs == other_atom._lhs - and self._lhs_name == self._rhs_name) + and self._lhs_name == other_atom._lhs_name + and self._rhs == other_atom._rhs + and self._rhs_name == other_atom._rhs_name) else: return False @@ -216,15 +219,185 @@ def check(self, cummulative_state): return None else: lhs_with_arithmetic = apply_arithmetic_stack( - self._lhs.arithmetic_stack, - cummulative_state[0][0] + self._lhs._arithmetic_stack, + cummulative_state[0][0][self._lhs_name] ) rhs_with_arithmetic = apply_arithmetic_stack( - self._rhs.arithmetic_stack, - cummulative_state[1][0] + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] ) return lhs_with_arithmetic == rhs_with_arithmetic +class StateValueLessThanStateValueMixed(Atom): + """ + This class models the atom (s1(x) < s2(y)). + """ + + def __init__(self, lhs, lhs_name, rhs, rhs_name): + self._lhs = lhs + self._rhs = rhs + self._lhs_name = lhs_name + self._rhs_name = rhs_name + self.verdict = None + + def __repr__(self): + return "(%s)(%s) < (%s)(%s)" % (self._lhs, self._lhs_name, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is StateValueLessThanStateValueMixed: + return (self._lhs == other_atom._lhs + and self._lhs_name == other_atom._lhs_name + and self._rhs == other_atom._rhs + and self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + lhs_with_arithmetic = apply_arithmetic_stack( + self._lhs._arithmetic_stack, + cummulative_state[0][0][self._lhs_name] + ) + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return lhs_with_arithmetic < rhs_with_arithmetic + +class StateValueLessThanEqualStateValueMixed(Atom): + """ + This class models the atom (s1(x) <= s2(y)). + """ + + def __init__(self, lhs, lhs_name, rhs, rhs_name): + self._lhs = lhs + self._rhs = rhs + self._lhs_name = lhs_name + self._rhs_name = rhs_name + self.verdict = None + + def __repr__(self): + return "(%s)(%s) <= (%s)(%s)" % (self._lhs, self._lhs_name, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is StateValueLessThanEqualStateValueMixed: + return (self._lhs == other_atom._lhs + and self._lhs_name == other_atom._lhs_name + and self._rhs == other_atom._rhs + and self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + lhs_with_arithmetic = apply_arithmetic_stack( + self._lhs._arithmetic_stack, + cummulative_state[0][0][self._lhs_name] + ) + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return lhs_with_arithmetic <= rhs_with_arithmetic + + +class StateValueLengthLessThanStateValueLengthMixed(Atom): + """ + This class models the atom (s1(x).length() < s2(y).length()). + """ + + def __init__(self, lhs, lhs_name, rhs, rhs_name): + self._lhs = lhs + self._rhs = rhs + self._lhs_name = lhs_name + self._rhs_name = rhs_name + self.verdict = None + + def __repr__(self): + return "(%s)(%s).length() < (%s)(%s).length()" % (self._lhs, self._lhs_name, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is StateValueLengthLessThanStateValueLengthMixed: + return (self._lhs == other_atom._lhs + and self._lhs_name == other_atom._lhs_name + and self._rhs == other_atom._rhs + and self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + lhs_with_arithmetic = apply_arithmetic_stack( + self._lhs._arithmetic_stack, + cummulative_state[0][0][self._lhs_name] + ) + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return lhs_with_arithmetic < rhs_with_arithmetic + + +class StateValueLengthLessThanEqualStateValueLengthMixed(Atom): + """ + This class models the atom (s1(x).length() < s2(y).length()). + """ + + def __init__(self, lhs, lhs_name, rhs, rhs_name): + self._lhs = lhs + self._rhs = rhs + self._lhs_name = lhs_name + self._rhs_name = rhs_name + self.verdict = None + + def __repr__(self): + return "(%s)(%s).length() <= (%s)(%s).length()" % (self._lhs, self._lhs_name, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is StateValueLengthLessThanEqualStateValueLengthMixed: + return (self._lhs == other_atom._lhs + and self._lhs_name == other_atom._lhs_name + and self._rhs == other_atom._rhs + and self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + lhs_with_arithmetic = apply_arithmetic_stack( + self._lhs._arithmetic_stack, + cummulative_state[0][0][self._lhs_name] + ) + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return lhs_with_arithmetic <= rhs_with_arithmetic + class StateValueLengthInInterval(Atom): """ @@ -253,6 +426,33 @@ def check(self, value): """ return self._interval[0] <= value[0][0][self._name] <= self._interval[1] +class StateValueLengthInOpenInterval(Atom): + """ + This class models the atom (len(s(x)) in I) for open I. + """ + + def __init__(self, state, name, interval): + self._state = state + self._name = name + self._interval = interval + self.verdict = None + + def __repr__(self): + return "(%s(%s)).length() in %s" % (self._state, self._name, self._interval) + + def __eq__(self, other_atom): + if type(other_atom) is StateValueLengthInOpenInterval: + return (self._state == other_atom._state and self._name == other_atom._name + and self._interval == other_atom._interval) + else: + return False + + def check(self, value): + """ + Mandatory check method used by formula trees to compute truth values. + """ + return self._interval[0] < value[0][0][self._name] < self._interval[1] + class TransitionDurationInInterval(Atom): """ @@ -269,7 +469,7 @@ def __repr__(self): def __eq__(self, other_atom): if type(other_atom) is TransitionDurationInInterval: - return (self._transition == other_atom._transition and self._interval == other_atom._interval) + return self._transition == other_atom._transition and self._interval == other_atom._interval else: return False @@ -277,6 +477,29 @@ def check(self, value): return self._interval[0] <= value[0][0].total_seconds() <= self._interval[1] +class TransitionDurationInOpenInterval(Atom): + """ + This class models the atom (d(delta t) in I). + """ + + def __init__(self, transition, interval): + self._transition = transition + self._interval = interval + self.verdict = None + + def __repr__(self): + return "d(%s) in %s" % (self._transition, self._interval) + + def __eq__(self, other_atom): + if type(other_atom) is TransitionDurationInOpenInterval: + return self._transition == other_atom._transition and self._interval == other_atom._interval + else: + return False + + def check(self, value): + return self._interval[0] < value[0][0].total_seconds() < self._interval[1] + + class TransitionDurationLessThanTransitionDurationMixed(Atom): """ This class models the atom (duration(t1) < duration(t2)) @@ -293,6 +516,37 @@ def __repr__(self): def __eq__(self, other_atom): if type(other_atom) is TransitionDurationLessThanTransitionDurationMixed: + return self._lhs == other_atom._lhs and self._rhs == other_atom._rhs + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + return cummulative_state[0][0] < cummulative_state[1][0] + + +class TransitionDurationLessThanEqualTransitionDurationMixed(Atom): + """ + This class models the atom (duration(t1) < duration(t2)) + for v the duration of another transition. + """ + + def __init__(self, lhs_transition, rhs_transition): + self._lhs = lhs_transition + self._rhs = rhs_transition + self.verdict = None + + def __repr__(self): + return "d(%s) <= d(%s)" % (self._lhs, self._rhs) + + def __eq__(self, other_atom): + if type(other_atom) is TransitionDurationLessThanEqualTransitionDurationMixed: return (self._lhs == other_atom._lhs and self._rhs == other_atom._rhs) else: @@ -306,7 +560,7 @@ def check(self, cummulative_state): if cummulative_state.get(0) is None or cummulative_state.get(1) is None: return None else: - return cummulative_state[0][0] < cummulative_state[1][0] + return cummulative_state[0][0] <= cummulative_state[1][0] class TransitionDurationLessThanStateValueMixed(Atom): @@ -347,6 +601,44 @@ def check(self, cummulative_state): return cummulative_state[0][0].total_seconds() < rhs_with_arithmetic +class TransitionDurationLessThanEqualStateValueMixed(Atom): + """ + This class models the atom (duration(t) <= v) + for v a value given by a state. + """ + + def __init__(self, transition, state, name): + self._lhs = transition + self._rhs = state + self._rhs_name = name + self.verdict = None + + def __repr__(self): + return "d(%s) <= (%s)(%s)" % (self._lhs, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is TransitionDurationLessThanEqualStateValueMixed: + return (self._lhs == other_atom._lhs and + self._rhs == other_atom._rhs and + self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return cummulative_state[0][0].total_seconds() <= rhs_with_arithmetic + + class TransitionDurationLessThanStateValueLengthMixed(Atom): """ This class models the atom (duration(t) < v.length()) @@ -385,6 +677,44 @@ def check(self, cummulative_state): return cummulative_state[0][0].total_seconds() < rhs_with_arithmetic +class TransitionDurationLessThanEqualStateValueLengthMixed(Atom): + """ + This class models the atom (duration(t) < v.length()) + for v a value given by a state. + """ + + def __init__(self, transition, state, name): + self._lhs = transition + self._rhs = state + self._rhs_name = name + self.verdict = None + + def __repr__(self): + return "d(%s) <= (%s)(%s).length()" % (self._lhs, self._rhs, self._rhs_name) + + def __eq__(self, other_atom): + if type(other_atom) is TransitionDurationLessThanEqualStateValueLengthMixed: + return (self._lhs == other_atom._lhs and + self._rhs == other_atom._rhs and + self._rhs_name == other_atom._rhs_name) + else: + return False + + def check(self, cummulative_state): + """ + If either the RHS or LHS are None, we don't try to reach a truth value. + But if they are both not equal to None, we check for equality. + """ + if cummulative_state.get(0) is None or cummulative_state.get(1) is None: + return None + else: + rhs_with_arithmetic = apply_arithmetic_stack( + self._rhs._arithmetic_stack, + cummulative_state[1][0][self._rhs_name] + ) + return cummulative_state[0][0].total_seconds() <= rhs_with_arithmetic + + class TimeBetweenInInterval(Atom): """ This class models the atom (timeBetween(q1, q2)._in([n, m])) @@ -454,6 +784,29 @@ def check(self, cummulative_state): result = self._interval[0] < duration < self._interval[1] return result +def is_mixed_atom(atom): + """ + Given an atom, check if its class is in the list of mixed atom classes. + :param atom: + :return: True or False. + """ + mixed_atom_class_list = [ + StateValueEqualToMixed, + StateValueLessThanStateValueMixed, + StateValueLessThanEqualStateValueMixed, + StateValueLengthLessThanStateValueLengthMixed, + StateValueLengthLessThanEqualStateValueLengthMixed, + TransitionDurationLessThanTransitionDurationMixed, + TransitionDurationLessThanEqualTransitionDurationMixed, + TransitionDurationLessThanStateValueMixed, + TransitionDurationLessThanEqualStateValueMixed, + TransitionDurationLessThanStateValueLengthMixed, + TransitionDurationLessThanEqualStateValueLengthMixed, + TimeBetweenInOpenInterval, + TimeBetweenInInterval + ] + return type(atom) in mixed_atom_class_list + """ Classes for propositional logical connectives. @@ -735,7 +1088,7 @@ def __init__(self, formula, optimised=False): self.atom_to_observation = {} self.atom_to_program_path = {} self.atom_to_state_dict = {} - self.collapsing_atom = None + self.collapsing_atom_index = None self.collapsing_atom_sub_index = None self.sub_formulas = [] # we use a tuple to record the instantiation time for each encountered bind variable @@ -797,10 +1150,10 @@ def construct_atom_formula_occurrence_map(self, formula): self.construct_atom_formula_occurrence_map(formula.operands[n]) elif formula_is_atom(formula): if not(formula in self.sub_formulas): - self.sub_formulas.append(formula) - formula_index_in_sub_formulas = len(self.sub_formulas)-1 + self.sub_formulas.append(formula) + formula_index_in_sub_formulas = len(self.sub_formulas)-1 else: - formula_index_in_sub_formulas = self.sub_formulas.index(formula) + formula_index_in_sub_formulas = self.sub_formulas.index(formula) if formula in self.atom_to_occurrence_map.keys(): self.atom_to_occurrence_map[formula_index_in_sub_formulas].append(formula) @@ -811,20 +1164,32 @@ def __repr__(self): return "Monitor for formula %s:\n timestamps: %s\n state: %s\n verdict: %s" % ( self._original_formula, str(self._monitor_instantiation_time), str(self._formula), self._formula.verdict) - def check_atom_truth_value(self, atom, value): + def check_atom_truth_value(self, atom, atom_index, atom_sub_index): """ - Given an atom, an observation and, if the atom is mixed, + Given an atom (with index and sub-index), an observation and, if the atom is mixed, an indication of whether the observation is for the lhs or rhs """ - check_value = atom.check(value) + # take the initial verdict so we can check the difference after update + initial_verdict = self._formula.verdict + # check the value of the atom given the value observed + check_value = atom.check(self.atom_to_observation[atom_index]) + # update the monitor accordingly based on the truth value given by the check if check_value == True: result = self.check(self._formula, atom) elif check_value == False: result = self.check(self._formula, lnot(atom)) elif check_value == None: - # mixed atoms can still be unconclusive if only part of them has been given an observation + # mixed atoms can still be inconclusive if only part of them has been given an observation # in this case, the atom maintains state so no changes are required to the formula tree result = None + # record the new truth value for comparison + final_verdict = self._formula.verdict + # if the verdict has changed, then the atom/sub-atom indices we just used for the update + # are the collapsing ones + if initial_verdict != final_verdict: + # for each monitor, this branch can only ever be traversed once + self.collapsing_atom_index = atom_index + self.collapsing_atom_sub_index = atom_sub_index return result def process_atom_and_value(self, atom, observation_time, observation_end_time, value, atom_index, atom_sub_index, @@ -843,114 +1208,17 @@ def process_atom_and_value(self, atom, observation_time, observation_end_time, v if not (self.atom_to_observation[atom_index].get(atom_sub_index)): self.atom_to_observation[atom_index][atom_sub_index] =\ (value, inst_point_id, observation_time, observation_end_time) - # self.atom_to_program_path[atom_index][atom_sub_index] = [v for v in program_path] - # we deal with integer indices now, so no need to copy a list self.atom_to_program_path[atom_index][atom_sub_index] = program_path self.atom_to_state_dict[atom_index][atom_sub_index] = state_dict else: # the observation has already been processed - no need to do anything return - initial_verdict = self._formula.verdict - - result = self.check_atom_truth_value(atom, self.atom_to_observation[atom_index]) - - final_verdict = self._formula.verdict - - if initial_verdict != final_verdict: - # for each monitor, this branch can only ever be traversed once - self.collapsing_atom = atom - self.collapsing_atom_sub_index = atom_sub_index + # check the truth value of the relevant atom based on the state that we've built up so far + result = self.check_atom_truth_value(atom, atom_index, atom_sub_index) return result - def check_optimised(self, symbol, force_monitor_update=False): - """ - Given a symbol, find the formula occurrences that contain this symbol. - For each of the occurrences, replace the atom with the appropriate value (T or F). - Then loop up through the parents while each successive parent can be collapsed to a truth value. - """ - - if not (force_monitor_update) and not (self._formula.verdict is None): - return self._formula.verdict - - if symbol in self.observed_atoms or lnot(symbol) in self.observed_atoms: - return - else: - self.observed_atoms.append(symbol) - - # NOTE: BE AWARE THAT THE ALPHABET USED TO INITIALLY POPULATE _STATE DOES NOT INCLUDE NEGATIVES - # OF EVERY ATOM - - # update state for the monitoring algorithm to use - self._state.set_state(symbol) - - # temporary fix for Python 3 - the long term solution needs to be more robust - index_of_symbol_in_sub_formulas = self.sub_formulas.index(symbol) - if index_of_symbol_in_sub_formulas in self.atom_to_occurrence_map.keys(): - positives = self.atom_to_occurrence_map.get(index_of_symbol_in_sub_formulas) - else: - positives = [] - - negatives = [] - - all_occurences = positives + negatives - - for occurrence in all_occurences: - # find the position of the atom in the subformula - index_in_formula = 0 - # if the formula to which this atom belongs is an atom, - # this can only happen when a formula consists of only an atom - if formula_is_atom(occurrence): - if formula_is_derived_from_atom(symbol): - if formula_is_derived_from_atom(occurrence): - self._formula.verdict = True - return True - else: - self._formula.verdict = False - return False - else: - if formula_is_derived_from_atom(occurrence): - self._formula.verdict = False - return False - else: - self._formula.verdict = True - return True - else: - for n in range(len(occurrence.operands)): - if occurrence.operands[n] in [symbol, lnot(symbol)]: - index_in_formula = n - - # replace the atom we've observed accordingly - if formula_is_derived_from_atom(symbol): - if formula_is_derived_from_atom(occurrence.operands[index_in_formula]): - occurrence.operands[index_in_formula] = 'T' - else: - occurrence.operands[index_in_formula] = 'F' - else: - if formula_is_derived_from_atom(occurrence.operands[index_in_formula]): - occurrence.operands[index_in_formula] = 'F' - else: - occurrence.operands[index_in_formula] = 'T' - - # iterate up through the tree, collapsing sub-formulas to truth values as far as we can - current_formula = occurrence - current_collapsed_value = collapsed_formula(current_formula) - # iterate while the current formula is collapsible to a truth value - while not (current_collapsed_value is None): - if not (current_formula.parent_formula is None): - current_formula.parent_formula.operands[ - current_formula.index_in_parent] = current_collapsed_value - current_formula = current_formula.parent_formula - current_collapsed_value = collapsed_formula(current_formula) - else: - # we have collapsed the root to a truth value - truth_value_to_boolean = {'T': True, 'F': False, '?': None} - self._formula.verdict = truth_value_to_boolean[current_collapsed_value] - return self._formula.verdict - - return None - def check(self, formula, symbol, level=0): """ Given a formula and a symbol that is true, @@ -973,86 +1241,96 @@ def check(self, formula, symbol, level=0): sub_verdict = None - indent = " " * level - + # we go through the possible forms of the formula if type(formula) is LogicalAnd or type(formula) is LogicalOr: - # first check if the disjunction or conjunction can be immediately - # collapsed to a truth value - if type(formula) is LogicalAnd: - if 'F' in formula.operands: - if level == 0: - self._formula.verdict = False - return False - elif type(formula) is LogicalOr: - if 'T' in formula.operands: - if level == 0: - self._formula.verdict = True - return True - - if len(set(formula.operands)) == 1: - if formula.operands[0] == 'T': - if level == 0: - self._formula.verdict = True - return True - elif formula.operands[0] == 'F': - if level == 0: - self._formula.verdict = False - return False # if not, iterate through the operands for n in range(len(formula.operands)): if not (formula.operands[n] in ['T', 'F']): + + # recursive base case - we have an atom if formula_is_atom(formula.operands[n]): + + # deal with negation + if ((formula_is_derived_from_atom(formula.operands[n]) and formula_is_derived_from_atom( symbol) and formula.operands[n] == symbol) or (type(formula.operands[n]) is LogicalNot and type(symbol) is LogicalNot and formula.operands[n] == symbol)): formula.operands[n] = 'T' if type(formula) is LogicalOr: - formula = 'T' + # we have at least one true subformula, so we can return true if level == 0: self._formula.verdict = True return True elif type(formula) is LogicalAnd: formula.true_clauses += 1 if formula.true_clauses == len(formula.operands): - formula = 'T' + # all subformulas are true, so we can return true if level == 0: self._formula.verdict = True return True + elif ((formula_is_derived_from_atom(formula.operands[n]) and type(symbol) is LogicalNot and formula.operands[n] == symbol.operand) or (type(formula.operands[n]) is LogicalNot and formula.operands[n].operand == symbol)): formula.operands[n] = 'F' if type(formula) is LogicalAnd: - formula = 'F' + # at least one subformula is false, so return false if level == 0: self._formula.verdict = False return False + elif type(formula) is LogicalOr: + if len(set(formula.operands)) == 1: + # for disjunction, we only care about false + if formula.operands[0] == 'F': + if level == 0: + self._formula.verdict = False + return False + else: + + # recursive on the subformula + sub_verdict = self.check(formula.operands[n], symbol, level + 1) + + # in the cases here, we don't care about None, since that means no truth value + # has been reached in the subformula + if sub_verdict: + formula.operands[n] = 'T' if type(formula) is LogicalOr: - formula = 'T' + # we have at least one true subformula, so we can return true if level == 0: self._formula.verdict = True return True elif type(formula) is LogicalAnd: + # if all subformulas are true, we can return true formula.true_clauses += 1 if formula.true_clauses == len(formula.operands): - formula = 'T' if level == 0: self._formula.verdict = True return True - elif sub_verdict == False: # explicitly not including None + + elif sub_verdict is False: # explicitly not including None + formula.operands[n] = 'F' - if type(formula) is LogicalAnd: - formula = 'F' + if type(formula) is LogicalOr: + # check for all false + if len(set(formula.operands)) == 1: + if formula.operands[0] == 'F': + if level == 0: + self._formula.verdict = False + return False + elif type(formula) is LogicalAnd: if level == 0: self._formula.verdict = False return False + + # we couldn't make any decisions based on subformulas, so return sub_verdict return sub_verdict + elif type(formula) is LogicalNot: if formula_is_derived_from_atom(formula.operand) and formula.operand == symbol: if level == 0: @@ -1062,6 +1340,7 @@ def check(self, formula, symbol, level=0): if level == 0: self._formula.verdict = True return True + elif formula_is_derived_from_atom(formula): if formula == symbol: if level == 0: diff --git a/requirements.txt b/requirements.txt index 4d95609..d0547ff 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1,3 @@ graphviz +flask +requests diff --git a/stopService.sh b/stopService.sh new file mode 100755 index 0000000..ee71348 --- /dev/null +++ b/stopService.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +## +# Script to cleanup the hanging python process. +# + +# This command does four things +# 1) Get the running process information +# 2) Gets only python process +# 3) Excludes the output which will show grep in it +# 4) List python process id +# 5) Loop through each python process, and send a kill signal + +PID=`ps aux | grep Python | grep -v grep | awk '{print $2}'` + +# Loop for process ids to kill python processes. +for pid in $PID +do + kill -9 $pid +done