Integrate goto-synthesizer into Kani

[qinheping]

Description of changes:

This PR integrate goto-synthesizer into Kani, and add an option to synthesize loop contracts for all loops.

Resolved issues:

Resolves #2156

Call-outs:

The purpose of this PR is to allow us to experiment the loop-contracts synthesizer on Kani benchmarks. However, there are still a few issues we need to address with later PRs:

• The synthesizer may not terminate. When there is no loop invariants in the candidate space, the enumerator in the synthesizer will run forever trying to find a solution. To address this problem, we might want to allow users to limit the resource used by the synthesizer. On the goto-synthesizer side, we will add an option to limit the size of candidates we enumerate, so that it will not keep enumerating when there is no solution in the candidate space. On the Kani side, we can also add an option to limit the running time of the synthesizer.
• The synthesizer is not compatible with unwinding numbers. Now the synthesizer ignores unwinding numbers, and will synthesize loop-contracts for all loops no mater if there are loop numbers specified for them. However, we might sometimes want to unwind some loops while synthesize loop contracts for other loops. We will allow users to specify unwinding numbers in goto-synthesizer. Then users can choose to synthesize loop contracts only for those loops without unwinding number specified.

Testing:

• How is this change tested?

This PR include a regression test.

• Is this a refactor change?

No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

That's awesome! Thanks for adding this. I have a few questions:

1. How does the loop synthesizer interacts with loop unwind argument?
2. Is there anyway we can avoid the non-termination? Even if that means failing the synthesis?
3. We need to add some documentation around this. I would suggest writing an RFC explaining the user experience, the value it adds and and its limitations.

[qinheping]

Yes, in the Call-outs part of the PR description I introduced my plan to handle non-termination and how to deal with unwinding numbers. More comments about them are appropriated.

And yes, I will create a RFC about it.

[celinval]

I think an RFC will help. From what you described, there is a conflict between unwind and loop synthesis, at least for now. In this case, we should figure out what the message should be and how we handle a harness that is annotated with unwind. There's also a question whether this should be applied to the entire system or to specific harnesses.

[zhassan-aws]

Is it possible to add tests?

[qinheping]

Is it possible to add tests?

I added two simple tests to check the synthesizer is correctly called and enumerates required loop invariants. More experiments are needed to see how the synthesizer works on more complicated tests.

[celinval]

Awesome! Are you planning to add more tests to this feature? I think it would be nice to at least add tests where there are assertions inside the loop and test cases where the proof fails. I'm OK if you want to just create an issue for now and work on it later.

[qinheping]

Thank you Celina! Yes, I plan to add more tests. I am doing the experiment of running the synthesizer on all current Kani benchmarks, which will provide us better insight about what we can and cannot synthesize. I will create an issue and add tests when the experiment is done.

[zhassan-aws]

Thanks @qinheping!

[zhassan-aws]

Thanks @qinheping! Please address any remaining comments from @celinval and wait for her approval before merging.