bug: SMT constraints should not be dependent on the execution order of tests
Closed this issue · 7 comments
Hi,
I am curious about what's the rule for specifications collecting from runtime values.
I can see one strategy is to keep the specifications size as minimal as possible. In this case, Nopol may lose some valuable runtime values. How to balance this problem?
I wrote a test #154 to expose this. From the test case we can see the final specification is not to keep the first two consistent runtime values but return the minimal input size value even it is inconsistent value.
I would consider this test exposes two problems:
-
The inconsistent input value is considered as specifications that will be used for patch synthesizing because its value size is smaller than consistent input values. Do we need a better strategy? I suppose we should keep the first two consistent inputs and discard the inconsistent one.
-
The classification of consistent Inputs and inconsistent Inputs. Only this two categories of input values and the rule of consistentInputs is first come first be, which means other not exactly the same inputs are all considered as inconsistent inputs. Should we classified them by their inputs in a fine-grained way?
WDYT? Let me know if my explanation is not clear for you or there are other reasons to do so.
I would say you found a bug.
Interestingly, in ValuesCollectorTest, the contract in natural language were correct, but did not correspond to the assertions.
I think that your explanation #1 is correct: the inconsistent inputs should be permanently discarded. Pushed a potential patch.
WDYT?
Hi Martin,
-the inconsistent inputs should be permanently discarded.
I dont think so because the rule to classifying the consistent inputs and inconsistent inputs is based on the sequence of tests running.
For example, if c=3 is the first run time value collected from test, then c=3 will be the consistent input and the later different inputs (i.e. a= 1) are considered as inconsistent values.
So I think there should be a better rule to category this runtime values. Also, Junit tests run in a random sequence. Thus, in theory, I suppose specifications collected could be different each time we run Nopol.
@monperrus
Hi Martin,
Please also see my reply for #146 . Discarding the second runtime value that with the same input but different output should be the reason to cause non-deterministic result of Nopol.
In my humble opinion, I would consider the root cause of these two issues is lacking of consideration of the "execution sequence" and without analyzing runtime values (i.e. considering the first input is consistent input and later different one is inconsistent; discarding the second runtime value which with the same input but different output)
Back to the question of consistentInputs / inconsistentInputs. consistentInputs/inconsistentInputs are the middle storage from runtime value to specification generation. In theory, this design is not rigorous enough. However, but in practical, there are little chance that the runtime value collected are completely inconsistent. In most cases, the runtime value collected are consistent inputs.
So I would think these cases remind us we need to be care of processing the runtime values. We should completely avoid the "execution sequence" impact in runtime value collection in later work.
renamed the issue to "bug: SMT constraints should not be dependent on the execution order of tests"
Closed per f6af5fc
Now all specifications are collected and passed to SMT, which means that Nopol does not depend on the test execution order anymore.
This is much better conceptually, and probably less buggy.
The price to pay is that 1) there are more constraints (slower synthesis) and 2) we don't detect UNSAT fast, we detect after all levels of synthesis (super slow in case of UNSAT)