[TG-8623] Fix primitive wrapper types in JSON value retriever

[antlechner]

Following the format of the json-io library, the JSON input to the value retriever does not distinguish between primitive types and their corresponding wrapper types. A class Foo with a field fooField of type Integer might appear as

{
  "@type":"org.cprover.Foo",
  "fooField":100
}

To support this "primitive representation", we need a special case in the struct assignment part.

The new function is_primitive_wrapper_type_name is moved here from TG. Any changes to it should be done in future refactoring PRs.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[antlechner]

@tautschnig I had to reformat all of the test commits on this PR because clang-format complained. It seems that this is a consequence of #4926. What is the reason behind enforcing clang-format on Java source files for regression tests?

[codecov-io]

Codecov Report

Merging #4973 into develop will increase coverage by 0.07%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4973      +/-   ##
===========================================
+ Coverage    69.24%   69.31%   +0.07%     
===========================================
  Files         1309     1308       -1     
  Lines       108453   108324     -129     
===========================================
- Hits         75096    75084      -12     
+ Misses       33357    33240     -117

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/java_utils.cpp	90.78% <100%> (+0.2%)	⬆️
jbmc/src/java_bytecode/assignments_from_json.cpp	97.78% <100%> (+0.05%)	⬆️
src/statement-list/statement_list_entry_point.cpp	86.36% <0%> (-1.52%)	⬇️
src/statement-list/scanner.l	76.44% <0%> (-1.39%)	⬇️
src/goto-symex/symex_goto.cpp	94.84% <0%> (-0.05%)	⬇️
src/goto-symex/expr_skeleton.cpp	100% <0%> (ø)	⬆️
.../statement-list/converters/expr2statement_list.cpp	0% <0%> (ø)	⬆️
...rc/statement-list/converters/expr2statement_list.h
src/goto-symex/symex_builtin_functions.cpp	89.25% <0%> (+0.26%)	⬆️
src/util/std_expr.h	91.02% <0%> (+0.83%)	⬆️
... and 1 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 5d2e8b9...91e652e. Read the comment docs.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 91e652e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121647072
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

[tautschnig]

@tautschnig I had to reformat all of the test commits on this PR because clang-format complained. It seems that this is a consequence of #4926.

I'm pretty sure that the clang-format configuration for Java actually should be amended in some way, which might in many cases help avoid the need for reformatting (assuming our Java tests are actually formatted in some consistent fashion...). I was in a way hoping for this to happen so that we could figure out what the correct formatting rules should be. Maybe we can do this here and now?

What is the reason behind enforcing clang-format on Java source files for regression tests?

Previously, clang-format would abort when encountering changes to Java files, leaving the C++ files untouched even when they weren't correctly formatted.

[allredj]

tidy

[antlechner]

@tautschnig

assuming our Java tests are actually formatted in some consistent fashion...

It doesn't look like they are. No format has ever been enforced for them... Do you think specifying a format for test files is generally useful? It certainly is for source code but tests are much more isolated and slightly different formats usually don't make them less readable.

Previously, clang-format would abort when encountering changes to Java files, leaving the C++ files untouched even when they weren't correctly formatted.

That sounds like a bug? Did we report this somewhere? Are only Java files affected, or do we have other file types that could secretly silence clang-format when they are changed?

[smowton]

If we want to there's an argument to git-clang-format giving wildcard excludes (i.e. *,java would do)

[antlechner]

@smowton Let's look into that. I don't think the clang-format issue should block this PR so I'll rebase it and merge it if it (and its TG bump) passes.