Non terminating STP

Guancio

unread,

May 15, 2012, 4:30:13 AM5/15/12

to stp-users

Dear all,
I'm starting to experimenting the usage of STP as component for
assembly verification.
I'm running STP with the following input file, but it not terminates.
There is some problem in my input program?

Regards

Roberto Guanciale

% free variables:
R_EBP_0 : BITVECTOR(32);
mem_296 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
% end free variables.

ASSERT(
(LET yvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000000)])|
(((0bin000000000000000000000000 @ mem_296[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hexfffffff8),
0hex00000001)])
<< 8)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hexfffffff8),

0hex00000003)]) << 24)[31:0])) IN
(LET xvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000000)])|
(((0bin000000000000000000000000 @ mem_296[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
0hex00000001)])
<< 8)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000003)]) << 24)[31:0])) IN
(LET sqvalue =((((0bin000000000000000000000000 @ mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000000)])|
(((0bin000000000000000000000000 @ mem_296[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

~0hex00000003),
0hex00000001)])
<< 8)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
mem_296[BVPLUS(32,

BVPLUS(32,

R_EBP_0,

~0hex00000003),

0hex00000003)]) << 24)[31:0])) IN
(LET y1 = BVPLUS(32, yvalue, 0hex00000001) IN
BVSLE(sqvalue, xvalue)
AND
sqvalue = BVMULT(32, y1, y1)
AND
BVSLE(BVMULT(32, yvalue, yvalue), xvalue)
)
))));

QUERY(
0bin1 =
(LET temp_82_0 = BVPLUS(32, R_EBP_0,0hexfffffff8) IN
(LET t_78_83_1 =
(LET loadnorm_297_2 = mem_296 IN
((((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000000)])|
(((0bin000000000000000000000000 @ loadnorm_297_2[
BVPLUS(32,
temp_82_0,
0hex00000001)])
<< 8)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_297_2[BVPLUS(32,

temp_82_0,

0hex00000003)]) << 24)[31:0])))
IN
(LET mem_300_3 =
(LET tempval_299_4 = BVPLUS(32,
t_78_83_1,0hex00000001) IN
(LET tempmem_298_5 =
(mem_296 WITH [BVPLUS(32,
temp_82_0,

0hex00000003)] :=
(tempval_299_4 >> 24)[7:0]) IN
(LET tempmem_298_6 =
(tempmem_298_5 WITH
[BVPLUS(32,

temp_82_0,

0hex00000002)] :=
(tempval_299_4 >> 16)[7:0]) IN
(LET tempmem_298_7 =
(tempmem_298_6 WITH
[BVPLUS(32,

temp_82_0,

0hex00000001)] :=
(tempval_299_4 >> 8)[7:0]) IN
(LET tempmem_298_8 =
(tempmem_298_7 WITH
[BVPLUS(32,

temp_82_0,

0hex00000000)] :=
tempval_299_4[7:0]) IN
tempmem_298_8))))) IN
(LET R_EDX_161_9 =
BVPLUS(32, (LET loadnorm_301_10 = mem_300_3 IN
((((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000000)])|
(((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000001)]) << 8)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_301_10[

BVPLUS(32,

temp_82_0,

0hex00000003)]) << 24)[31:0]))),
0hex00000001) IN
(LET T_32t2_82_197_11 = BVMULT(32, R_EDX_161_9,R_EDX_161_9) IN
(LET temp_231_12 = BVPLUS(32, R_EBP_0,0hexfffffffc) IN
(LET mem_304_13 =
(LET tempval_303_14 = T_32t2_82_197_11 IN
(LET tempmem_302_15 =
(mem_300_3 WITH [BVPLUS(32,

temp_231_12,

0hex00000003)] :=
(tempval_303_14 >> 24)[7:0])
IN
(LET tempmem_302_16 =
(tempmem_302_15 WITH
[BVPLUS(32,

temp_231_12,

0hex00000002)] :=
(tempval_303_14 >> 16)[7:0])
IN
(LET tempmem_302_17 =
(tempmem_302_16 WITH
[BVPLUS(32,

temp_231_12,

0hex00000001)] :=
(tempval_303_14 >> 8)[7:0])
IN
(LET tempmem_302_18 =
(tempmem_302_17 WITH
[BVPLUS(32,

temp_231_12,

0hex00000000)] :=
tempval_303_14[7:0]) IN
tempmem_302_18))))) IN
(LET R_EAX_235_19 =
(LET loadnorm_305_20 = mem_304_13 IN
((((0bin000000000000000000000000 @
loadnorm_305_20[
BVPLUS(32,
temp_231_12,

0hex00000000)])|
(((0bin000000000000000000000000 @
loadnorm_305_20[
BVPLUS(32,
temp_231_12,

0hex00000001)]) << 8)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_305_20[
BVPLUS(32,
temp_231_12,

0hex00000002)]) << 16)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_305_20[
BVPLUS(32,
temp_231_12,
0hex00000003)])
<< 24)[31:0])))
IN
(LET temp_277_21 =
(LET loadnorm_306_22 = mem_304_13 IN
((((0bin000000000000000000000000 @
loadnorm_306_22[
BVPLUS(32,
temp_82_0,

0hex00000000)])|
(((0bin000000000000000000000000 @
loadnorm_306_22[
BVPLUS(32,
temp_82_0,

0hex00000001)]) << 8)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_306_22[
BVPLUS(32,
temp_82_0,
0hex00000002)])
<< 16)[31:0]))|
(((0bin000000000000000000000000 @ loadnorm_306_22[
BVPLUS(32,
temp_82_0,
0hex00000003)])
<< 24)[31:0])))
IN
(LET temp_278_23 = BVPLUS(32, temp_277_21,0hex00000001) IN
(LET goal_295_24 =
(IF (R_EAX_235_19=
BVMULT(32, temp_278_23,temp_278_23)) THEN 0bin1
ELSE 0bin0 ENDIF&
IF (BVSLE(BVMULT(32, temp_277_21,temp_277_21),
(LET loadnorm_307_25 = mem_304_13 IN
((((0bin000000000000000000000000 @
loadnorm_307_25[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000000)])|
(((0bin000000000000000000000000 @
loadnorm_307_25[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),

0hex00000001)]) << 8)[31:0]))|
(((0bin000000000000000000000000 @
loadnorm_307_25[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
0hex00000002)])
<< 16)[31:0]))|
(((0bin000000000000000000000000 @ loadnorm_307_25[
BVPLUS(32,
BVPLUS(32,

R_EBP_0,

0hex00000010),
0hex00000003)])
<< 24)[31:0]))))) THEN 0bin1 ELSE 0bin0 ENDIF)
IN
goal_295_24)))))))))))
);
COUNTEREXAMPLE;

Trevor Hansen

unread,

May 15, 2012, 8:40:35 AM5/15/12

to stp-...@googlegroups.com

Hi Guancio,

To find out if STP is spending its time doing nothing, or working hard, run it with the command line: -s -t

If nothing happens it's probably trying to parse from the STDIN.

I hope your experiments go well,

Trevor

From: Guancio <gua...@gmail.com>
To: stp-users <stp-...@googlegroups.com>
Sent: Tuesday, 15 May 2012 6:30 PM
Subject: Non terminating STP

Guancio

unread,

May 15, 2012, 10:59:45 AM5/15/12

to stp-users

Dear Trevor,
STP is not waiting from STDIN, it consume 100% of one of my cores. I
tried the option you suggested and
I attach the corresponding output.

Roberto

[3ms:12M]Printing: input asserts and query: Node size is: 195
Difficulty Initially:28848
[1ms:12M]Printing: After Removing Unconstrained: Node size is: 195
[1ms:12M]Printing: After Establishing Intervals: Node size is: 195
[2ms:12M]Printing: After Constant Bit Propagation: Node size is: 195
[1ms:12M]Printing: after solving: Node size is: 193
Difficulty After Size reducing:28846
[0ms:12M]Printing: after pure substitution: Node size is: 193
[3ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: after pure substitution: Node size is: 136
[0ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: After Constant Bit Propagation begins: Node size
is: 136
[0ms:12M]Printing: After Establishing Intervals: Node size is: 136
[0ms:12M]Printing: Before SimplifyWrites_Inplace begins: Node size is:
136
[0ms:12M]Printing: after pure substitution: Node size is: 136
[0ms:12M]Printing: after simplification: Node size is: 136
[0ms:12M]Printing: after solving: Node size is: 136
[1ms:12M]Printing: After SimplifyWrites_Inplace: Node size is: 136
[0ms:12M]Printing: After Unconstrained Remove begins: Node size is:
136
Initial Difficulty Score:28846
Final Difficulty Score:32086
Array Sizes:12 :
[0ms:12M]Printing: after transformation: Node size is: 160
SimplifyMap:0:193
SimplifyNegMap:0:193
AlwaysTrueFormSet0:193
MultInverseMap0:193
ReadOverWrite_NewName_Map0:193
NewName_ReadOverWrite_Map0:193
substn_map0:193
[0ms:12M]Printing: Before Constant Bit Propagation begins: Node size
is: 160
Nodes before AIG rewrite:26005
advanced CNF
============================[ Search
Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT |
Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl
| |
===============================================================================
| 100 | 20555 64688 157959 | 23718 100 31 |
1.358 % |
| 250 | 20555 64688 157959 | 26090 250 26 |
1.358 % |
| 475 | 20555 64688 157959 | 28699 475 76 |
1.358 % |
| 812 | 20555 64688 157959 | 31569 812 108 |
1.358 % |
| 1318 | 20555 64688 157959 | 34726 1318 95 |
1.358 % |
| 2077 | 20555 64688 157959 | 38199 2077 99 |
1.358 % |
| 3216 | 20555 64688 157959 | 42019 3216 119 |
1.358 % |
| 4924 | 20555 64688 157959 | 46221 4924 123 |
1.358 % |
| 7486 | 20555 64688 157959 | 50843 7486 121 |
1.358 % |
| 11330 | 20555 64688 157959 | 55928 11330 129 |
1.358 % |
| 17096 | 20555 64688 157959 | 61520 17096 126 |
1.358 % |

On May 15, 2:40 pm, Trevor Hansen <trev_abr...@yahoo.com> wrote:
> Hi Guancio,
>
> To find out if STP is spending its time doing nothing, or working hard, run it with the command line: -s -t
>
> If nothing happens it's probably trying to parse from the STDIN.
>
> I hope your experiments go well,
>
> Trevor
>
>
>
>
>
>
>
> >________________________________

> > From: Guancio <guan...@gmail.com>

> ...
>
> read more »

Guancio

unread,

May 15, 2012, 3:21:53 PM5/15/12

to stp-users

Dear Trevor,
I was using the binary version of STP.
After reading the message http://www.mail-archive.com/klee...@keeda.stanford.edu/msg00154.html
I decided to compile the svn sources. The problem is now solved.

Roberto

> ...
>
> read more »

Reply all

Reply to author

Forward