K-user mailing list

[Alex <alexdba AT gmail.com>]

Once again, thanks!

I already tried something similar, but we decided to avoid changing too much the semantics to add features that are not part of the formal operational semantics.

All my implementation is based in symbolic values, I have no explicit/exact inputs.
What I need is to add the symbolic execution path-condition,
exactly what Dorel meant in his message.

Kind regards to all.

Alex

Le mer. 15 févr. 2017 à 04:53, Dorel Lucanu <dorel.lucanu AT gmail.com> a écrit :

Is it possible to add a condition to the initial configuration? For instance to run only the branch with "V0 >Int 0"?

Thanks.

Dorel

On Tue, Feb 14, 2017 at 11:00 PM, Saxena, Manasvi <msaxena2 AT illinois.edu> wrote:

Hi Alex, 

Here’s an example of how you can control execution in symbolic execution, and use the “requires” clause to control the execution. Here’s an example definition - 

module A-SYNTAX

syntax Exp ::= "symInt"

             | Int

             | String

syntax Exp ::= if(Exp) [strict]

endmodule

module A

imports A-SYNTAX

syntax KResult ::= Int

                 | String

rule symInt => ?_:Int \\rule a

rule if(X) => "positive" requires X >Int 0 [transition]  \\rule b

rule if(X) => "negative" requires X <Int 0 [transition] \\rule c

endmodule

When you run krun —search on the program "if(symInt)", you should see something like - 

<k> "negative" </k>

 AND ( V0 <Int 0 ) ==K true

Solution 2

<k> "postive" </k>

 AND ( V0 >Int 0 ) ==K true

Notice that the “symInt" is converted using rule a to a symbolic Int by "rule a". Both "rule b" and "rule c", which have conditions in their requires clauses, then apply on the symbolic variable. The execution then splits, and constraints are introduced. You should  be able to guide you execution using the requires clause.

Hope this helps. Let me know if you have any questions.

-Manasvi

On Feb 14, 2017, at 1:34 PM, Alex <alexdba AT gmail.com> wrote:

Thanks for the explanation!

I had figured out that I could match parts of the final configuration, and that is also useful.

Unfortunately that is not what I'm looking for: by guiding the execution path, I mean that

I'm looking for a way to specify a path condition, as in symbolic execution.

I guess that --pattern parameter is not the way to go.

I've saw mentions of using k-framework to perform symbolic execution, but I didn't find

a way to drive the execution path.

I would appreciate any suggestion.

Thanks again,

Alex

Le mar. 14 févr. 2017 à 11:15, Saxena, Manasvi <msaxena2 AT illinois.edu> a écrit :

Hi Alex,

The pattern specified by the —pattern option is matched on the final configuration, and the substitution is displayed, instead of the entire configuration.

For e.g., suppose the result of a krun execution is

<T> <result> 10 </result> *other stuff* </T>

then, you can filter your output by running giving krun the —pattern flag. You could call run with —pattern ‘<result> X </result>, and the result would be -
Solution 1
X ==K 10

> Is it possible to guide the execution path using such parametere, or is there another way?

I don’t think you’ll be able to use the —pattern flag to guide the execution. By guiding, do you mean you only want certain, but not all rules from the definition, to be considered during application? Or are you looking for a way to specify rewrite rules in the command line during krun?

-Manasvi


> On Feb 14, 2017, at 5:43 AM, Alex <alexdba AT gmail.com> wrote:
>
> Cheers!
>
> Do someone have a nice example of how to use the --pattern parameter in the krun tool?
>
> Is it possible to guide the execution path using such parametere, or is there another way?
>
> Thanks!
> Alex Alberto