Safety

[Tim Hinrichs]

Hi all,

This morning I ran across some odd behavior for Hampi. (And I just
checked out the latest version.) Here's the example.

var X : 1;
reg reg131 := ['a'-'c'];
assert X not in reg131;

Hampi returns
{VAR(X)=}

The same answer shows up regardless what reg131 is defined as.

If we add something like

reg reg132 := ['a'-'z'];
assert X in reg132;

then Hampi returns
{VAR(X)=p}

This reminds me of safety in datalog: where every variable appearing
in a negative literal must also appear in a positive literal. I
didn't think Hampi had such a requirement. Am I wrong?

I'm planning to use the usual work-around, detecting unsafe variables
and adding positive guards for each, but wondered if that's already
been done somewhere.

Tim

[Devdatta]

Hi Tim,

I think the problem here are two fold :
> Hampi now takes the var's length parameter as the max length
instead of exact length
> Not in means anything other than the particular regex.

can you try :
--start--
var X : 1;

cfg len1Text := Sigma ;
cfg Sigma := ['a'-'z'] | "=" | "_";

reg reg131 := ['a' -'c'];

assert X not in reg131;

assert X in len1Text;

--end--

Regards
devdatta

2010/1/8 Tim Hinrichs <thin...@gmail.com>:

[Adam Kiezun]

Hi Tim,
This is a known problem and it stems from Hampi not having a
'universe' of allowed string values. So, Hampi does not know how to
interpret 'not in' without an 'in'. (What actually happens at the
implementation level is that Hampi forwards the encoded constraint to
STP and STP responds with 'all zeros' which Hampi decodes as character
with code 0. Which is what you see as empty string.)

This is definitely something we need to fix. The current workaround,
as Devdatta mentioned, is to explicitly specify the universe.
./adam

[Devdatta]

2010/1/8 Adam Kiezun <aki...@gmail.com>:

> Hi Tim,
> This is a known problem and it stems from Hampi not having a
> 'universe' of allowed string values. So, Hampi does not know how to
> interpret 'not in' without an 'in'. (What actually happens at the
> implementation level is that Hampi forwards the encoded constraint to
> STP and STP responds with 'all zeros' which Hampi decodes as character
> with code 0. Which is what you see as empty string.)

hmm ... I thought Hampi was returning a string of length 0. Is that
not the case here ?

cheers
devdatta

[Adam Kiezun]

> hmm ... I thought Hampi was returning a string of length 0. Is that
> not the case here ?

Actually, it seem weirder than that. Here's the hexdump of the output.

hexdump -C empty.txt
00000000 7b 56 41 52 28 58 29 3d c2 86 7d 0a |{VAR(X)=..}.|
0000000c

So, if I'm reading this correctly, Hampi returns a 2-byte string with
hex values c2 86.

Either way, it's a problem that needs to be addressed.
./adam

[Pieter Hooimeijer]

I have occasionally seen odd behavior like this in the string output
-- it doesn't necessarily mean that the correct solution wasn't found.
If you modify hampi.properties to read printOrd=yes (instead of 'no'),
there's a good chance it will output the correct decimal ASCII codes.

Adam: could you try this and confirm?

Cheers,

Pieter

[Adam Kiezun]

You're right, with printOrd=true, it returns:
{VAR(X)="\134" (1)
}

The answer is arbitrary. We should probably make the ASCII range the
default alphabet so you'd at last see something.
./adam

[Devdatta]

Hi all,

Another bug I noticed, the following gives unsat :

var string:17;
gives unsat. I don't see why.

cfg q2 := \065 \112 \112 \108 \101;
cfg q3 := [\032 - \126];
cfg q4 := (q3)*;
cfg q5 := \077 \111 \098 \105 \108 \101;
cfg q6 := [\032 - \126];
cfg q7 := (q6)*;
cfg q8 := \083 \097 \102 \097 \114 \105;
cfg q1 := q2 q4 q5 q7 q8;
cfg flax0 := q1;

assert string in flax0;
----

Regards
Devdatta

2010/1/15 Adam Kiezun <aki...@gmail.com>:

[Pieter Hooimeijer]

Shouldn't you be saying something like

reg fixedcfg = fix(flax0, 5);

somewhere?

Cheers,

Pieter

[Devdatta]

No -- afaik, new versions of hampi don't require the 'fix' declaration.

Regards
devdatta

2010/1/23 Pieter Hooimeijer <pieter.h...@gmail.com>:

[Adam Kiezun]

Devdatta,
can you enter this as an 'issue'
(http://code.google.com/p/hampi/issues/list) so that it does not get
lost?

Thanks
./adam

On Sat, Jan 23, 2010 at 7:47 PM, Devdatta <dev.a...@gmail.com> wrote:

[Devdatta]

done!
http://code.google.com/p/hampi/issues/detail?id=1

2010/1/23 Adam Kiezun <aki...@gmail.com>: