Dear Ridwan,
Sorry for the late reply!
We are still working on making the tool, however in our previous version
of the tool, we essentially had CNF formulae in human readable format.
For instance, the condition k==20 was essentially just that, instead of
being represented as a bit vector.
So a more complicated expression, like p =/= 5 /\ k == 20 was
represented as a list containing the two conditions.
On 23/03/2021 12:11, Ridwan Shariffdeen wrote:
I'm not much familiar with the kquery format, but you can use smt2 or
cvc formats which will give you the constraints you are looking for.
What is the format your tool expects the constraints in?
On Tue, Mar 23, 2021 at 6:58 PM Bharat Garhewal <[email protected]
<mailto:[email protected]>> wrote:
Ah, so if I want the constraints while referring to the variable
and not just the value, we will have to parse the smt2 file?
If so, that will pose a problem for our use-case, since we want to
parse the constraints and then feed them to our tool.
I suppose I should start digging around in the KLEE source then,
any tips? :)
Thank you,
Bharat
On 23/03/2021 11:51, Ridwan Shariffdeen wrote:
The current format supported is in smt2, so use --write-smt2s
which will produce a smt2 file
On Tue, Mar 23, 2021 at 6:46 PM Bharat Garhewal
<[email protected] <mailto:[email protected]>> wrote:
I used:
klee -write-kqueries --libc=uclibc --posix-runtime
--external-calls=all --seed-out=file.bout example.bc
On 23/03/2021 11:43, Ridwan Shariffdeen wrote:
Hi
What's the Klee command you used
On Tue, Mar 23, 2021, 6:40 PM Bharat Garhewal
<[email protected] <mailto:[email protected]>> wrote:
Dear Ridwan,
Thank you for the link! I'm trying to use your KLEE fork
(from GitHub, not the DockerHub), but I'm unable to
capture the information that I want.
For instance, I've consider the following code:
#include <stdio.h>
#include <stdlib.h>
#include </klee/source/include/klee/klee.h>
int main(){
int k;
klee_make_symbolic(&k, sizeof(k), "k");
if (k == 20)
printf("Statement Five\n");
else
printf("Statement Six\n");
printf("\nk=%d\n", k);
return 0;
}
I generate the seed file with: gen-bout --second-var
model_version 4 01 --second-var k 4 20
However, the kquery file I get is:
array k[4] : w32 -> w8 = symbolic
array model_version[4] : w32 -> w8 = symbolic
(query [(Eq 1
(ReadLSB w32 0 ))
(Eq 20 <---------- I would expect 'k' here
(ReadLSB w32 0 ))]
false)
Is this the expected behaviour, or perhaps I am doing
something wrong?
Regards,
Bharat
On 13/03/2021 12:33, Ridwan Shariffdeen wrote:
Hi,
What you are looking for is for a concolic execution. I
have a modified version of KLEE to get what you want.
You can refer to the repo
https://github.com/rshariffdeen/klee/tree/concolic
<https://github.com/rshariffdeen/klee/tree/concolic>
and build KLEE. There is also a docker image hosted at
dockerhub rshariffdeen/klee:concolic which is already
built.
Then using seed-file, you can feed the concrete input
and it willl be executed concretely but capturing the
symbolic constraints you need. If you are not familiar
with see-file setting, I can let you know how to use
for one example.
Let me know, if you have any questions or if this works
for you
Regards
On Fri, Mar 12, 2021 at 9:42 PM Bharat Garhewal
<[email protected] <mailto:[email protected]>> wrote:
Dear all,
I'm working on (white-box/grey-box) Active Automata
Learning for programs with data parameters
(i.e., our automata contain data parameters in
guards and in i/o).
We require that for each concrete query, we can
extract data (i.e., path) constraints for that query.
For instance, consider that we have a one-element
FIFO buffer with two actions: PUSH(p) and POP(p):
Given a query of the form ``PUSH(p1=5) POP(p2=3)''
(where p1 and p2 are the "markers"/"names" given
to 5 and 3), we want to retrieve the constraint "p1
=/= p2" from the path followed by the program
(assuming that the comparison between 5 and 3
actually happens in the program). We're trying
to obtain these PC using KLEE.
I've been trying to get concrete inputs working
with KLEE (latest docker build) and Zesti (docker,
from https://github.com/rshariffdeen/zesti
<https://github.com/rshariffdeen/zesti>), but I
guess I'm doing something wrong.
For instance, consider the "Tutorial One" example,
get_sign, with no changes to the source code.
If I run it with klee-zesti, as "klee-zesti
-posix-runtime -libc=uclibc get_sign.bc 22", It
would expect to explore only one branch, but I
somehow end up exploring 10?
With Zesti (if anyone has any idea), I still end up
exploring all 3 branches of the function.
Does anyone have any clues on how to get this
working? (Either KLEE or Zesti would be fine :))
Thank you,
Regards,
Bharat Garhewal,
ICIS - SWS,
Radboud University
_______________________________________________
klee-dev mailing list
[email protected]
<mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
