Updating the wp-interpolant algorithm

[rasoolmaghareh]

@ArpitaDutta @sanghu1790 The commit "Function argument mapping" is adding a lot of files in Debug+ Assert folder. These are binary files and they should be removed. Also I am seeing some .setting files being added, these files are generated during build and should not be checked in.

[ArpitaDutta]

Hii Rasool, How can I help in this?

Regards, Arpi

On Mon, Sep 6, 2021 at 10:34 AM Rasool Maghareh @.***> wrote:

@ArpitaDutta https://github.com/ArpitaDutta @sanghu1790 https://github.com/sanghu1790 The commit "Function argument mapping" is adding a lot of files in Debug+ Assert folder. These are binary files and they should be removed. Also I am seeing some .setting files being added, these files are generated during build and should not be checked in.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/tracer-x/TracerX/pull/381#issuecomment-913293915, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD22LAARI2VKGEFPKM5JOXTUAQSB3ANCNFSM5DPPAEXQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[rasoolmaghareh]

Please check the changes that are added and remove all the files which are added in the commits and are in Debug+Assert folder.

Hii Rasool, How can I help in this? Regards, Arpi

[ArpitaDutta]

Okay Rasool.

On Mon, Sep 6, 2021 at 11:15 AM Rasool Maghareh @.***> wrote:

Please check the changes that are added and remove all the files which are added in the commits and are in Debug+Assert folder.

Hii Rasool, How can I help in this? Regards, Arpi

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/tracer-x/TracerX/pull/381#issuecomment-913306894, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD22LAAQIZNRDS35O5KXKEDUAQW5RANCNFSM5DPPAEXQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[rasoolmaghareh]

Thanks @ArpitaDutta for removing Debug+Assert and Release+Assert from the main directory. However, there are still many Debug+Assert and Release+Assert folders left in the subdirectories like Core\Debug+Assert and Solver\Debug+Assert. Can you please remove those too? You can see a full list when clicking the Files Changed Tab in this pull request(PR).

[ArpitaDutta]

Sure Rasool.

On Tue, Sep 7, 2021 at 9:29 PM Rasool Maghareh @.***> wrote:

Thanks @ArpitaDutta https://github.com/ArpitaDutta for removing Debug+Assert and Release+Assert from the main directory. However, there are still many Debug+Assert and Release+Assert folders left in the subdirectories like Core\Debug+Assert and Solver\Debug+Assert. Can you please remove those too? You can see a full list when clicking the Files Changed Tab in this pull request(PR).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/tracer-x/TracerX/pull/381#issuecomment-914307433, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD22LACTNMSXEJAYBF6TVG3UAYHSXANCNFSM5DPPAEXQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[ArpitaDutta]

Hii Rasool, I have removed the files from the following folders: lib/Basic/Debug+Asserts/ lib/Basic/Release+Asserts/ lib/Core/Debug+Asserts/ lib/Core/Release+Asserts/ lib/Expr/Debug+Asserts/ lib/Expr/Release+Asserts/ lib/Module/Debug+Asserts/ lib/Module/Release+Asserts/ lib/Solver/Debug+Asserts/

Shall I also remove these few files?

.settings/language.settings.xml Makefile.config config.log config.status docs/doxygen.cfg examples/get_sign/get_sign.bc include/klee/Config/CompileTimeInfo.h include/klee/Config/config.h

Regards, Arpi

On Tue, Sep 7, 2021 at 10:55 PM Arpita Dutta @.***> wrote:

Sure Rasool.

On Tue, Sep 7, 2021 at 9:29 PM Rasool Maghareh @.***> wrote:

Thanks @ArpitaDutta https://github.com/ArpitaDutta for removing Debug+Assert and Release+Assert from the main directory. However, there are still many Debug+Assert and Release+Assert folders left in the subdirectories like Core\Debug+Assert and Solver\Debug+Assert. Can you please remove those too? You can see a full list when clicking the Files Changed Tab in this pull request(PR).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/tracer-x/TracerX/pull/381#issuecomment-914307433, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD22LACTNMSXEJAYBF6TVG3UAYHSXANCNFSM5DPPAEXQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[rasoolmaghareh]

@ArpitaDutta Please remove these files too:

.settings/language.settings.xml
Makefile.config
config.log
config.status
docs/doxygen.cfg
examples/get_sign/get_sign.bc

There are also a lot of .dir files such as lib/Basic/Debug+Asserts/.dir and also a lot of .d files in the Release+Assert folders still, such as lib/Solver/Debug+Asserts/*.d files. I think the folders are not deleted completely.

[rasoolmaghareh]

@ArpitaDutta Thanks, There are still 2175 files in this PR. Let me take a look over the weekend and try to delete the remaining extra files.

[rasoolmaghareh]

This branch fails in the instantiation of the WP interpolant (when we have a sel expression with a symbolic variable). We have to change the intantiateWP function to accomodate these three cases:

Case 1. S is concrete. Wpvar (S) >= 0 and S =5 in Mu Return: 5>=0

---

Case 2. S is symbolic. wpvar (S) >= 0 and S = S0 on Pi or Mu

Testing these solutions first:

1. Return dummy >=0 and fail subsumption.
2. Return wpvar (S) >= 0 and fail subsumption.

3. Actual solution, Retrun S0 >= 0 and all relevent constraints from Pi.

   Case 3. No information on S exists: Wpvar (S) >= 0 and No information on S.

1-Return dummy >=0 and fail subsumption.

[rasoolmaghareh]

Comment from @ArpitaDutta:

Solution 1: "returning dummy variable" For killer.c, it works perfectly fine. For killer2.c, it generates results till the constraint depends on half of the index of the array but not after that. It returns "TxWeakestPreCondition::getCastInst size not supported yet!" with Segmentation fault error.

Solution 2: "returning the WP-interpolants" For killer.c, it generates, Assertion0 && "invalid expression kind" with segmentation fault. For killer2.c, it generates results till the constraint depends on half of the index of the array but not after that. It returns " Assertion `0 && invalid expression kind " with Segmentation fault error same as for the killer.c.

[rasoolmaghareh]

A new error that @ArpitaDutta has seen in the following:

KLEE: WARNING: TxWeakestPreCondition::getConstantExpr: ConstantExpr is not support
i8* bitcast ([8 x i32]* @main.power to i8*)

This error is due to the point that our WP algorithm at the current moment does not support ConstantExpr. We can solve this by returning dummyExpr for now in the TxWeakestPreCondition::getConstantExpr function.

[rasoolmaghareh]

Summary of issues at the current moment:

1. Failure at TxWeakestPreCondition::getConstantExpr due to not supporting ConstantExpr.
2. Failure at TxWeakestPreCondition::getCastInst due to not supported type (Arpi has added a temporary fix). We need to revisit here. (PARTIALLY DONE).
3. The important missing part is Case 2. S is symbolic. from the comment on 16th Nov. (DONE)

I will explain issue 3 first:

There is an important piece of code in TxTreeNode::instantiateWPatSubsumption where we check if the Mu of the subsumed node contains a variable which we have in the WP expression and we replace the value from Mu into the wpExpr. The first place that we check if any information on the variable exists is using the following peice of code:

ref<TxAllocationContext> alc =  dependency->getStore()->getAddressofLatestCopyLLVMValue(WPVar->address);

If alc has any value then we compute an expression for it. If not @ArpitaDutta has changed the code to return a dummyExpr. This is correct since no value existed on this variable. However, in the future, we have to change this so that we look into historical values as well. The information might be there.

Issue 2 is also partially fixed. Now we should look into case 1 which is not easy to implement. This error is due to the point that our WP algorithm at the current moment does not support ConstantExpr. We can solve this by returning dummyExpr for now in the TxWeakestPreCondition::getConstantExpr function.

This would also partially fix this problem.

Next steps to do:

1- Returning dummyExpr in the TxWeakestPreCondition::getConstantExpr function. 2- Discussion on checking the historical values (next meeting).

[rasoolmaghareh]

In today's meeting, we discussed how to check historical values. We noticed that inside the function TxStore::getAddressofLatestCopyLLVMValue(llvm::Value *val), only internalStore is checked.

We know that internalStore contains references to concretelyAddressedStore and symbolicallyAddressedStore, but does not contain any reference to the historical stores:

1. LowerStateStore concretelyAddressedHistoricalStore
2. LowerStateStore symbolicallyAddressedHistoricalStore

We separately need to add two for loops to check the historical stores. These stores are LowerStateStore and in case the ref<TxAllocationContext> address inside getAddressofLatestCopyLLVMValue is empty after the first loop (meaning that a value for the variable was not found, then we will switch to the historical stores and search over there too.

[ArpitaDutta]

Initially, we are checking for the InternalStore in TopStateStore. And TopStateStore is a map. typedef std::map<ref, MiddleStateStore> TopStateStore;

Where we are returning address which is of type ref if match found.

But when I am searching inside LowerStateStore which is a map of "typedef std::map<ref, ref > LowerStateStore;", I am unable to map the values into ref type. It is because both the LowerStateStore and TopStateStore are maps of different value pairs of different data types.

Is there any way to retrieve the TxAllocationContext from either TxVariable or TxStoreEntry?

[ArpitaDutta]

In continuation to the last issue, we discussed today to add a new function inside instantiateWPatSubsumption to find the ref<TxAllocationContext> alc using the LowerStateStore when the alc is not available inside internalStore.

[rasoolmaghareh]

After fixing the previous issue, @ArpitaDutta has run an experiment and reported that out of 20 programs:

1. 6 programs report segmentation fault
2. 9 programs report oversubsumption
3. remaining 5 programs run correctly.

In the first step, we investigated the 6 programs with seg. fault. Our initial guess is that the instantiateWPatSubsumption( ) is missing loading values from Global Variables. We will first try to fix this part and in the next step, we will look at the oversubsumption case.

[ArpitaDutta]

There was a issue in the smoke-test python script. After, fixing that, we have following report on 20 selected programs for smoke-test.

1. 6 programs report segmentation fault
2. 3 programs report oversubsumption
3. remaining 11 programs run correctly.

Segmentation fault occurred in the 6 programs due to the bugs in instantiateWPatSubsumption() function. 5 out of 6 programs failed due to the null dereferencing problem. We fixed that.

However, in one program, there is an error in instantiateWPatSubsumption() function because of its call for rebuild(kids) in "return wpInterpolant->rebuild(kids);" statement for the sle kind of expr. But it happens only when it follows a particular type of expression sequence.

Also, there is a new issue. We found this error message "KLEE: ERROR: Z3Simplification::z3Expr2TxExpr does not support for this type of expr!" for some programs.

[rasoolmaghareh]

Closing this pull request, since the code got merged separately.