Additional String Support is Needed

[sohah]

Additional support to string support is needed for functions included in these tests

jbmc-regression/StaticCharMethods03.yml
jbmc-regression/StaticCharMethods05.yml
jbmc-regression/StaticCharMethods06.yml
jbmc-regression/StringBuilderAppend02.yml
jbmc-regression/StringBuilderCapLen04.yml
jbmc-regression/StringBuilderChars03.yml
jbmc-regression/StringBuilderChars04.yml
jbmc-regression/StringBuilderChars05.yml
jbmc-regression/StringBuilderChars06.yml
jbmc-regression/StringBuilderConstructors02.yml
jbmc-regression/StringBuilderInsertDelete02.yml
jbmc-regression/StringBuilderInsertDelete03.yml
jbmc-regression/StringCompare02.yml
jbmc-regression/StringCompare03.yml
jbmc-regression/StringCompare04.yml
jbmc-regression/StringIndexMethods03.yml
jbmc-regression/StringIndexMethods05.yml
jbmc-regression/StringValueOf07.yml
jbmc-regression/StringValueOf08.yml
jbmc-regression/StringValueOf09.yml
jbmc-regression/TokenTest02.yml
jbmc-regression/Validate02.yml

Source code of all methods can be found in here

To run use a configuration similar to the one below, assume that the program under test is located under examples/svcomp

target=svcomp.BellmanFord_FunUnsat01.Main

classpath=${jpf-symbc}/build/examples

symbolic.dp=z3bitvector
symbolic.min_int=-2147483648
symbolic.max_int=2147483647
symbolic.min_double=-10000.0
symbolic.max_double=10000.0
symbolic.bvlength=64
search.depth_limit=13
symbolic.strings=true
symbolic.string_dp=z3str3
symbolic.lazy=on
symbolic.jrarrays=true
listener = .symbc.SymbolicListener

symbolic.optimizechoices=true
symbolic.debug=true

[RehanChalana]

Hi @sohah

As we discussed on Discord, I have successfully compiled and run both SPF and JPF.

Any guidance would be greatly helpful. Thanks!
I’d like to contribute to this issue, but since I’m still new to the project and codebase, I would appreciate any guidance on how to get started. Could you suggest any steps or areas I should focus on while researching this issue?

Any guidance would be greatly helpful. Thanks!

[sohah]

@RehanChalana, I am not sure which of them to try out first. I know there is a partial support for most of them. So may be you can start by first finding which of these have a partial support. Then, identify a small addition that you can contribute, take these tests as examples, but they are not comprehensive.

[RehanChalana]

Thanks! @sohah

While investigating StringBuilderAppend02.yaml and looking into the gov.nasa.jpf.symbc.bytecode.SymbolicStringHandler class, I noticed that the method handleStringBuilderAppend3(JVMInvokeInstruction invInst, ThreadInfo th) is currently unimplemented.

It appears to handle the case for StringBuilder.append(CharSequence, int, int). I’m currently working on implementing this method and aligning it with the way handleStringAppend3 is handled for String.