How to use specific symbol to represent calls to some functions.

[idiomaticrefactoring]

Hi,

Recently I use SPF, I want to represent some functions calls as specific symbols to add into PathCondition ,in order to I can handle path Condition later on.
For example express arrlist.get(x) as Arraylist_Get(X) But I don't know how to do it.

[corinus]

you can take a look at the following for inspiration:
jpf-symbc/src/main/gov/nasa/jpf/symbc/concolic

[idiomaticrefactoring]

Thank you! @corinus

I run the example TestMain.java in jpf-symbc/src/main/gov/nasa/jpf/symbc/concolic ,But it don't occur uninterpreted functions .I have added annotation @Concrete("true") public static double hash_java(double x) .

this is TestMain.jpf:

target=gov.nasa.jpf.symbc.concolic.TestMain
classpath=${jpf-symbc}/build/main
symbolic.method=gov.nasa.jpf.symbc.concolic.TestMain.test_concolic(sym#sym)
symbolic.concolic=true
Actually I run the src/examples/conclic,it seems occured the same problems
when I print Annotations.len is 0(is in method checkConcreteAnnotation(MethodInfo mi) )I'm so confused.

[corinus]

Hi:
The code that I indicated is not exactly what you want but you can use it for inspiration.
FunctionExpression would allow you to model some methods in your code with uninterpreted functions.

[dah-fari7009]

Hello,
I am facing the same problem, I am trying to leave some functions uninterpreted in the final summary. Did you ever figure out how to do this ?

[corinus]

Hi: java.lang.Math functions are handled like that. You can take a look in classes and peers.

[dah-fari7009]

Thank you !

[dah-fari7009]

From what I am seeing, I will need to define a separate function to obtain a FunctionExpression object for each method. I am having trouble to understand how and when this operation (generating a FunctionExpression) is triggered.
Also, do you have any idea if there is way for me to obtain this result for any method without having to define a new separate function ? I am working without user-defined procedures, so I don't know before hand the information about the function that should be left uninterpreted

[corinus]

You can define a listener that monitors for each method call and perform your calculation for the particular methods that you have in mind.

[dah-fari7009]

Thank for this answer ! Is this any different from using the concolic listener, since it performs the transformation of a method to a FunctionExpression ?

[corinus]

no it is not pls look at that listener

[dah-fari7009]

Thank you for your help. Sorry for asking you so many questions, I am very confused since I have not changed the original code and this has been bugging me for a while now :

For a few days now, I have been running tests with the concolic listener, on a simple file where I annoted one of the function @concrete("true"). I keep on getting an exception when it tries generating the FunctionExpression, where apparently the number of arguments returned by getArgumentAttr is not the expected value. Do you have any idea what could be causing this behavior or could let me know if my understanding of what this value represents is correct?

Here I meant MethodInfo.getArgumentTypeNames instead

[dah-fari7009]

Shouldn't getArgumentAttrs, getArgumentValues and getArgumentTypeNames all be the same length ? I don't understand why there are not in this case

[dah-fari7009]

Hi again,

Sorry to bug you but I would just like to know what getArgumentAttrs, getArgumentValues and getArgumentTypeNames are supposed to return. I have looked through the code but could not figure it out

[corinus]

they return argument attributes, values and types (as he names suggest)

[dah-fari7009]

Hi,
Thank you for the answer. This was my understanding but then it goes back to my issue where the length of these objects are not the same when I try running the concolic listener (on the example above)

Since I did not modify the code for the listener, I figured you might have more insight on what is causing this behavior

[dah-fari7009]

Hello,

I just wanted to let you know that I found the problem and fixed the issue that I was having and was wondering if you considered I should make a pull request for it (it is just one line of code to change)

[corinus]

thank you yes please

[dah-fari7009]

That's noted. Thank you for your help