msv-lab / symlog

Symbolic executor of Datalog
Universal Permissive License v1.0
3 stars 0 forks source link

Some questions #7

Open rainLiuplus opened 1 year ago

rainLiuplus commented 1 year ago
  1. What is the method for selecting the EDBs that will be symbolized to generate target tuples (see this issue)?

  2. After identifying 1-minial set of facts that are required for target tuples, which of those facts should be removed to prevent the generation of the target tuples (see this issue)?

  3. When creating positive queries using symbolic facts, there may be multiple options for the symbolic facts. However, many of these options will not be valid. For instance, an assignment like "IfVar(goto/6, , r#123)" is incorrect because the first argument should be an 'if' expression. In addition to these obvious incorrect assignments, there may also be other, less obvious invalid assignments that appear in inappropriate positions. E.g., use if(var != null) to surround if(var != null)...else... block. How can we filter out these incorrect tuples? For the remaining valid tuples, how can we decide which one to return?

    Currently, we use semantics checkers to filter out invalid tuples. The semantics checkers are python functions that take the tuples as inputs. We do not modify the Datalog program. For the valid tuples, we simply return the first one we find. Is this approach ok?

  4. In order to generate patches in various forms, it is necessary to encode patch components into the Datalog program. However, this approach will make the Datalog program more complex. Is it possible to use a simple Datalog program to generate rough patches first, and then use a post-processing python function to convert the raw patches to different forms? Or, should we just include one patch template in the Datalog program, which means our repair method can only generate one kind of patch?

  5. Is it possible to use traditional delta-debugging methods, such as directly removing facts, to identify the input tuples that lead to the target tuples? Our current method involves adding 0 or 1 to Datalog rules in order to record the facts that generate the head tuple. However, this causes the program to change during delta-debugging, making it necessary to recompile the program periodically. This can be time-consuming. Additionally, we cannot use interpreter mode as Souffle does not support rules with more than 20 arguments in this mode.

  6. Do we need to run delta-debugging multiple times to find all 1-minimal sets for target tuples?