goto-synthesizer: Separate front-end for loop-contracts synthesizer

[qinheping]

This introduces a new binary to handle all steps related to loop-contracts synthesis, which previously was part of goto-instrument. The main reason we want a separate front-end is to let one front-end tool to focus on one specific task. Also, there is no termination guarantee for the synthesizer which is not aligned with other functionality of goto-instrument.

No functionality is included in this PR yet. I will migrate the synthesizer into goto-synthesizer once this PR is merged.

[codecov]

Codecov Report

Base: 78.41% // Head: 78.39% // Decreases project coverage by -0.02% ⚠️

Coverage data is based on head (b03d870) compared to base (2653d78).
Patch coverage: 96.66% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7415      +/-   ##
===========================================
- Coverage    78.41%   78.39%   -0.03%     
===========================================
  Files         1655     1655              
  Lines       190264   190281      +17     
===========================================
- Hits        149201   149172      -29     
- Misses       41063    41109      +46     

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_internal_additions.cpp	90.12% <ø> (ø)
src/cpp/cpp_internal_additions.cpp	88.09% <ø> (-2.11%)	⬇️
...strument/contracts/dynamic-frames/dfcc_library.cpp	95.54% <ø> (ø)
...cts/dynamic-frames/dfcc_lift_memory_predicates.cpp	89.60% <40.00%> (ø)
src/ansi-c/c_typecheck_expr.cpp	75.68% <100.00%> (ø)
src/ansi-c/cprover_library.cpp	97.91% <100.00%> (ø)
src/cpp/cprover_library.cpp	92.30% <100.00%> (ø)
...ument/contracts/dynamic-frames/dfcc_instrument.cpp	81.44% <100.00%> (ø)
...contracts/dynamic-frames/dfcc_pointer_in_range.cpp	100.00% <100.00%> (ø)
...t/contracts/dynamic-frames/dfcc_pointer_in_range.h	100.00% <100.00%> (ø)
... and 24 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[tautschnig]

Can you please also amend CODEOWNERS to include a special rule for this new directory? (I think the rule should be the same as the existing one for the synthesizer.)

[tautschnig]

@kroening @peterschrammel Would welcome your thoughts here. @qinheping has implemented what I suggested in his other PR, and obviously I'm happy with that :-) Please speak up if you'd prefer not to add a separate binary.

[TGWDB]

Looks ok with some minor fixes. Also happy to see a modular approach.

I think CODEOWNERS should be updated to reflect who should review PS here in future.

[qinheping]

@NlightNFotis The CI failure is caused by api codes as shown below. Could you please fix it?

/home/runner/work/cbmc/cbmc/src/libcprover-cpp/api.h should remove these lines:
- #include "options.h"  // lines 15-15
Unnecessary includes found. Use '// IWYU pragma: keep' to override this.

[thomasspriggs]

@NlightNFotis The CI failure is caused by api codes as shown below. Could you please fix it?

/home/runner/work/cbmc/cbmc/src/libcprover-cpp/api.h should remove these lines:
- #include "options.h"  // lines 15-15
Unnecessary includes found. Use '// IWYU pragma: keep' to override this.

This issue in develop should now be fixed.