From 2337c138d235d943d27ec114511531fd5f072276 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 9 Mar 2023 03:31:16 +0000 Subject: [PATCH] =?UTF-8?q?=E5=A2=9E=E5=8A=A0=E6=B5=8B=E8=AF=95=E8=84=9A?= =?UTF-8?q?=E6=9C=AC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- atpg | Bin 77680 -> 77680 bytes bench_test/c1355.bench | 623 + bench_test/c1908.bench | 942 ++ bench_test/c3540.bench | 1745 +++ bench_test/c499.bench | 279 + bench_test/c6288.bench | 2484 ++++ bench_test/c880.bench | 473 + benchmark/b01.bench | 59 + benchmark/b02.bench | 35 + benchmark/b03.bench | 187 + benchmark/b04.bench | 662 + benchmark/b06.bench | 72 + benchmark/b07.bench | 477 + benchmark/b08.bench | 193 + benchmark/b09.bench | 172 + benchmark/b10.bench | 206 + benchmark/b11.bench | 467 + benchmark/b12.bench | 1167 ++ benchmark/b13.bench | 386 + benchmark/b17.bench | 25223 +++++++++++++++++++++++++++++++++++++++ benchmark/b20.bench | 9247 ++++++++++++++ benchmark/b21.bench | 9508 +++++++++++++++ benchmark/b22.bench | 14479 ++++++++++++++++++++++ benchmark/c1355.bench | 623 + benchmark/c17.bench | 17 + benchmark/c1908.bench | 942 ++ benchmark/c2670.bench | 1570 +++ benchmark/c3540.bench | 1745 +++ benchmark/c432.bench | 207 + benchmark/c499.bench | 279 + benchmark/c5315.bench | 2612 ++++ benchmark/c6288.bench | 2484 ++++ benchmark/c7552.bench | 3831 ++++++ benchmark/c880.bench | 473 + check.log | 6 + circuit.cpp | 1 - ls.cpp | 10 +- run_exp.py | 225 + 38 files changed, 84104 insertions(+), 7 deletions(-) create mode 100644 bench_test/c1355.bench create mode 100644 bench_test/c1908.bench create mode 100644 bench_test/c3540.bench create mode 100644 bench_test/c499.bench create mode 100644 bench_test/c6288.bench create mode 100644 bench_test/c880.bench create mode 100644 benchmark/b01.bench create mode 100644 benchmark/b02.bench create mode 100644 benchmark/b03.bench create mode 100644 benchmark/b04.bench create mode 100644 benchmark/b06.bench create mode 100644 benchmark/b07.bench create mode 100644 benchmark/b08.bench create mode 100644 benchmark/b09.bench create mode 100644 benchmark/b10.bench create mode 100644 benchmark/b11.bench create mode 100644 benchmark/b12.bench create mode 100644 benchmark/b13.bench create mode 100644 benchmark/b17.bench create mode 100644 benchmark/b20.bench create mode 100644 benchmark/b21.bench create mode 100644 benchmark/b22.bench create mode 100644 benchmark/c1355.bench create mode 100644 benchmark/c17.bench create mode 100644 benchmark/c1908.bench create mode 100644 benchmark/c2670.bench create mode 100644 benchmark/c3540.bench create mode 100644 benchmark/c432.bench create mode 100644 benchmark/c499.bench create mode 100644 benchmark/c5315.bench create mode 100644 benchmark/c6288.bench create mode 100644 benchmark/c7552.bench create mode 100644 benchmark/c880.bench create mode 100644 check.log create mode 100644 run_exp.py diff --git a/atpg b/atpg index 2978293d3c049955aafe470d34a749e9047abf1f..1dcbd2962928a435df105da7f84338c6a8735cf8 100755 GIT binary patch delta 5961 zcmY*d3tUvy)<65eC=^YPO*2|`Vt3*(;TJS)k089*gP zcWV=shb6Pjjp2P?{IEn2j&X^|O11H>ra{HszmSe`lJcU96w)KIQmXph3H+t)e07I| zYmh=-^yy&Fq$T10EP*WHz9FMJL`@J?$iN-2M1_GIS!p+`4s{q^Md!lvSPD&x2=p13 z1gX3eE(y`M()ODyQ42{BOqMaLsVHK)xO*zKM1-((Td&ATo!N2QypgRUTV_ifJ<2HF znQJS2J<~f%lCPTNCu&S9oR_bvB~LU>9}p*)l!=K5Mp~f1)hN}B&*6E|2X9)eX<9<` zIhveq3LdM(e37rEo|TlZBS4m-pXkl8BHWQXNqHw-B>6}N$gKw#P<8r1mPak=3&YsM ziAw4(g7n~f7-N;D;3}yUf{73`Sz?$nIW)2|zgAyTDaVJZpVOL*V1Ed(2Ib{YNzRub z27Y53e;J+5DDE*{nH_49?~l*F4Dwh$ub$ppZeZTDVfi$l(vLN*`T0M2P{`)j+&@M$Wkqk_0n%I-Nug3qQHHI{zn|7~QuG78`IbQa zRvJ95CS`unr0DB<^KxfFQ2SESO7C9El+Xkju03%?{{q6js#a0X%0T8z`&JHcGb{+x z2bj4rfr^&*%AS<}?^F-OZIZ8>f`3)l?$fkM`8W0Eus;xRJpx|PE-qO%rSPyVnMHi1 z$21_!r^A8N?vipO0_IHeEmQDs>g~O-tmFrQk~e1EGC{y7(I>5w z?3IOqqH) z!afnnn#V24KSbV_rp7>Ei_R{vuA$`1Br*>pT@t5*1r#_b;*EvKk zQ%h!|_@_WIS^d~~nw>R5-?Q~=N%55AlM-sqe3}kq#jwfLoE6MYQ;+NcL!aSsDo5gY z2uj+%$VO?dZsZbVDf%Rw&~G~K=n+5!Ik;~Z+a&?z%+PV+d*=3qx z3^_wOO+f*u@6q&}pdQ2O+LwBMk$t&6{~*fQ$_`U_ZZCF(;&TTv3oXnIW=&L@8^k`R zs$B2HZ9AdB8_wtha(Hr8e-Q5K`~Hs9H}Atrx8rL&@S0|82VUL$4e+PcT11A`jY!zt z)nTIBP72KXw5#8ab|oj8x6{?UF`~7Cew)}=^sFEc(_l7_-ZCe37b|!bwb&OlLHWve)_R zhm>jB(UC~5B;Qg8l+j1)0-2S*U6;YWqj)95`)DcDEAGbT`7qnAC#0M%C@+QEws22$ z|DKJ;(8#l6HX8V`tLUPW?PpZw0=dK}IB`c@6HW+Ok~cn0Kg#zZxZ zf-F15A*EDjG4}2~f^)8_O`9|=zcRH5jVy4OgH%QC>(fIl!#jGZ30YmNo+{BaN0(c; z*?xFoOK=T|o9W>C=;4DPuU>-;+{n-28_u#a8Ct_RozLa;wqx!Z=>6eP336AtuQgBd)iY>~qZXc%IP6+q_%hAm{tpmwTlFtXiBOjqG?GtMbaS{Y*b)|XR@*$s^2DiWGylvXwNobg-CMNLi(RgAauAh{qX&(1*TQ2R~Z>%Uw4ctq7ZEY$V^YC)M5- zI$k=El~8kOJji|+*xhhS_czO` zf7_HCC%3Ks!Lu=`J&l74AT{eQVwQhE*tX!OMWZjEDO-cHOF?RvzO)w7Zje@I!=3iS z%7*G{JDQtYI`Hb|n}5N#{{?qLv9!-U|CDY&9GbJA5}JJ>*sEPK_b-fq4b*j;i7lg7 zxAhZ~3T&C%<}e($S3mrS-6MJXDA9Edo!I^w!>2&Gk!_*)a)a0_pHj-lMa1Rv^&MmD zk4jH9w>wg!O2BzL#-%0|rHfBRE%Rs z=~%@w)iXV?ai#~YG^IZeQJ0c@Q!A73*2@yfl$NEjLsw4 zIY~6Frk{6iWs4|lmkDkC%&ukZ3O&2~Sur+;a&{M>ue`hFK z$AEhk3(hPasRPo!T=(^n27t5WXCZdPQBi^yOeol^?P`ewEF4Um43* zaj6va`D?gDaKlO6C5#!rgj-S=?jNSPH%+oCRjIfDE=5`=T_5qHm;Kn_%f1^NC&EP=`7b zq!W~MmjtD=q>PD;r^JsVME7`F{qYC5B=p|z!wM*B{|UE^P>u_;q(l{w?tn=gz0>yM zfq3Tf$8&b0H)zKv2VKY52hYSlN7D~3WcR7&;0Q77{f(a<@bFA~S{o|Sm!Fm~9Cy~` zD4=?4FLs@NwZ6=XXw0EL><+zlC`^2Q87YTG_3gY2K}WYPZQ%!10UXCcDOrX&ZiX%N zuR{shaZ9m+XO=+D(zUqY`TtRZ*pxbMdugX-opf58vizBwGzl?=YghbwQ0ZKcs|WG>FP?(xI6D+(*tF^-vEQkyn&x>;(~|L8@e2Rcv_!lW z`~~j|T5?j!u9yKTj^V{KH7x@$2e1e*?sZLj2v`CbgOhbPhn)oBSHPD#3qoqLrp37m z!V17Tz}<5+?Nk>*sCYxu4!8-z5kRB6AUv6id0hpe|2)Wf2*PB*aeB<34?UhjwqRYL zX$_cg?QKm<0mJhhO&bZr!n;t&9Rlo$PEhflrmf-~0a7my zU<6=dHjqRs3%}9MxL3Yh!Ck1s*wStP&ffTV8jKKBW#4{#ny*09F7BAD{}H>#6a~8(k7#MNMzv4#WjgcOYA(?^o zU&m=fX=h!mo97};+luTvYh9?dE}=^@>U}KNaF1fY^>dTfv}w59#i0QeB%xx;xQ5SZ z=eMz4tm&Gz5%uAWe`mgZW9qu;nzo)Rn1ChnC=&BJujy2%vpBDJ+8}b*W}>z{aX07& zoIlw9!eY>RgBH!}+R0D!fM5{N0?@~;qwQx0BL}r-C*tbnRX>sC(46`ySc60LJ%Z~t zYT6)(@`tPc2A-&(owHNmEZ`;3{*P|fPZUF6p-~Ne-6VV+n6c8%FSsCRf68izcl+DR znl_k6rFEwI2H#%NZd?)Clnet@QQ|M{rY8-DYHNP`)e4g`4T0Z8`_9}@BA9AKj-70sSEQI>%#=6e6b5^W2~FKER2}eM78Gvbxpv0=s)MebveLNX+Yy> zU8S8nzwvpU3vAt>PZ|Ssp};QDxyC8F9AGjHI3M5}3NzPEX&S8BAMR@$Xg|`d^Fwuf zV;O1F`6;?_pxvfsV5Pvmq%lnay03s;qB%_yb?(?lr|3}AXkC*X`%lvdT>-FF^vs2c zx=VH}^TNbVLD)Z&r_tF9eLI`x+oXWF^!yD6Rc-t?Jfd-=Nx7U6>v)JbtZ z;w6;1e#EN0gkm=x27BF6A=lieee1=pdg{LS5^B2Zz%2K&4g9`;H*|&!o76H=WGS}X z8*l2w%3Nys&-=W7?rab%_uB5;MS)9FX=vt%0k`(ClK zoLYWA3jRlbq%-_^_c&dw+-fU(oW;2u z%r)h(!&u4|IfT8ya<-fc!C&7U|8Z||4P_&`Rh)7NwZoZPl0sQ{m&X?!YLU-m-wnA_`W#q%cJ!}EakEkVR{C3;(UH0lk?~V2@9)k_yC&TQ^gD0_8hR+2-Qsx=GRbK~o)L06Il9FJIlVZ-K zFEGi^)z{P_B#<4j$A!EU-S?~p+Zz2N#fOEkOqv|#=RXysGg8(C6U+>>IL%Hx1ccD{6wMLI&=DHF^`skwp%(Y6qv$hjckSi~13blij4O)9#XdXcowo`^cWrn$4hF z8B@ZN74t6wdm%l)$%;(DCzJ)D(pt!+aJAN07Fm?Tz0$8Nl6!@!J80&t-~gpBmtm!n zoFhRDB4?}lW9i7Oc?7@DyyEUz%=YKR!AB5;0 zLNDYxGa7HH4mK1YApZzJ_n$s+xjWpI>QfMuvBq;Ur5_8U`H|i7f zT%Y|uBmG>1_kNQy&ekX9H+}XcS3ywg(Fb#z_$4U4Lz859_Xa`bE9@Q06SR-g=C;%| z*9XN3WSiT{xvnM_CF?M>ONx@ofi-$c@9G4?ZX8G^C94o1MakmJNl8!?2@r*R_n(^f z(TF}d|2BIeY9{$NQ}C~9=bf6?C+Cqq`|&G;%Z6}`57P%_^QA%gs);;m*7-Knj{4{l zQl(htuQe&@1r^_+d=eBp*PWR2OrO)+Sx)9&Z_8;i4E|qlKds^af8Iu5a{RFPkKvrT zfutPbb!L(un*xJ>S95m2DT~AsfwkEwr}RDbCG1P`t;lDRd`6u| zZu48z%LnhcH(qMdKdHm~_Wlhj`{{!cFi#1Pa&DV@B*_!)zjY#g7jVBhog5q(T_Nxrc$KEPyBW}C0qPi5RJFA zVzVjV62iLCVM}|rmq@m%qbf_=h8NCrdpxP*u=SDHBd;hVbA#Uzl!BCV*6c4S@$T^A z`SYZhGJW|H8ac!hmNv?xs6vxSNm9jJe#pl0%^ zitc2|>L#WX(C^8CV&P`;GPPr_ZU>-OUm?VF%zPFk7rVJMoHdEdHgQKjQ z;GG{{PA|@=&44EnK*3h}FrG(UF)i>Eue{+&;+=YdT%`bo-sp<;|%21qcFL%7oS`cpPdC{mRqwiv_Z~d-6<$9K!0VOrhV5LL6zjk>Zx^< zl-H7_(B!;XEQ5Z{o7H5*TAq`7#)@$;TchXvCQ4TZg%4ZiAU0!`rxk50DHz+1PX zyE)R?=*G({je-j&)xS8BUMSHFPUSc8=)|>Jb%i6SZ+^R!?a+fh!aaBi^oYB|opOEz zCvg+XN~7aoQ|729hEgihX9qzh@|pUfLr=DmcS#-rIl-8sHl~vNt>Tq6lx8(H3+==? z_f+#LO~W~3Lz^q^;3SQvz1ED7FFMw?8I#p)oTg4(scFum(`z+)m~&e~L)9wkyELX_ zC&;UrkbxUHnY>i3b4Nkz2b|95a(Z>MyAOJMIH0D`v89(i21N5i;jucC)+~$d-v}e_ zStL2;WT)~tS)*O5$^K4qj=v+_a}8kKjDjk$nl3u&-1G%ZQ6H=zqirp6cg$vB;Z$y$ zC|)O$mItxHG;w*EcxgF(up+?w;BrUgHw=X_Tz?FdlJDC>SImbT-UKDhMrx(2KnLI)2s%fNSyeY zio9C9xWf7l-u)eX&pY^xx45G@R0O>xRD1*6x5i3~cNoW)(!LEQ){tIpXd(Ww#NK@4 zXohxc`C=DaNx_@Ch`VxV+@_CNES=b7WS!{OO$PD5vdMjOLd5-Sp5JZ*-$SK00$%O7 zs%C+XivjL0W|S`4#%ge}m*#B_Xp#=J@@};!YVRB#u6yc8+P`@c>q-6v32X$7ESSOa z=xV_PpOcIJ_i5IHlDB*!rY^!^Hl)KsDD8|_jonz_wP)Ef%&f6e44hlJy@)z&?IS*1 zNQ<^^V0sGNW?}Wge^v)r zYP6oI^r%)}*+l&qvW|m^cT6wHsJrk=Qs(2cMKjlj20zI|?x3XsOJR#KuP=*vAO@%9$`pL=>S z_YFO;45fKK#qZniaW|e1-Y<`*7yG8L)ihy$C-GuB73|;ZRcL-&8)^p{c3?e2yE`x& z1vItLmo1^ig+o{b-7Rd+R?y#tVdBrzDdejzfjg$d`IyS-4|t=>h39CLk~PY41y=JY z>#HQo{m+rYNq9-t`Y#(I_!$sG@b3Xf@Piv6czd1fTb#{5{=qJCvWIcD)ye*rvzI&B zTb%5MoIQnGc!^ha@m6d`E^6?mAJz_vD<-{z53r{mjIDpL=%Hvxn>u!MnqkJc(bLCH zY*AO}mDD%EFtDF#@SvoAeK8j3;mP4H9}iBUrza!3q@|^X8fKWsO&&RRin)uSm18`9 zbb6ZELEvLdaXw?G&Kx&=^n`H`3yT_0LyOypxyANn#r?$=hwo{ca9`6>@GHQt3ctAj z#>X@Nfwz;`X~h!p5hQpYAFgS$0KEZifTbfe?FFE5q^8B9HAiviCI~YD2h|Y-*HO^s zAqaH=F91f3*0fT%6){HBzV<||0EX5Rgr#Hg307Ya4gy~D5`=Ou^NPxmVnjLuh2XOjNXk#}7|;gjPU}kA zuu*iPq=|TA2;C}ajlZPW*(PijH9h-Y(74uu5D-wWj=K#vgHZTt#IFdK(o8_tJv8iW z>%h{FQ6hXuFzRK0fJu67PxJn!%6j(kVM3D=RHbg$Hxez+Xq z^%~Od$bTNEccu0hx_cH((XEZ={&l`|-X!*JBTP>)f z8>pW3T+4B4|3mk>aT%Jn0yW~Q(3~H}4Dg4NrCiAXq{+)BX4P5jmantAE_GQZauvdu`cQ)-qTScp_o3L`d@CTy8}$1 z*_Xq0xenUC%UyLPz>d7aW7xq8(6YCoL`v>Ws}umWH`=+xC9-S@zXsN!m}t`VFrq?l`6b$1-t z>}#ELHejiA=vuPwz5~;hCA&pnFI^u*L&^f(1_7-)M03jey6ps-H;68l1-2T5`hGD? z(?Ym2iC*4W;xI41I{xsKo562OKGz%S@_}Vi@b%tJZvY!~Mbq$2=Xg@^PIYkQ>;2sL zb}blWFTY;EBB1qa7sd4pUtzz;FKm~u@SSH53|7=f!JMx@;E*pnA)h~i)E5Df+N;MI5F@A^9f<=f(QhG^JmU;lamgUP0E&WL?H>8CeSFtxuH z&hFb6YL`O9I@UD&>dxTn@qi^R<7(uki?FoqW8{I)!Rr>YDzc UEWEDyMoutputs.size() >= 2) { gate->stem = true; } - // gate->stem = true; if(gate->stem) { stems.push_back(gate); } diff --git a/ls.cpp b/ls.cpp index 0cfbe73..0b53b26 100644 --- a/ls.cpp +++ b/ls.cpp @@ -8,8 +8,6 @@ bool Circuit::local_search(std::unordered_set &faults) { - //STEM_INC = 0; - // 初始化并重置所有 ls 数据结构 ls_init_data_structs(); @@ -19,7 +17,7 @@ bool Circuit::local_search(std::unordered_set &faults) { // 随机生成初始电路 ls_init_circuit(); - printf("local search!\n"); + //printf("local search!\n"); while(true) { @@ -81,7 +79,7 @@ bool Circuit::local_search(std::unordered_set &faults) { } if(stem_total_cnt == stems.size() && flip_total_cnt == 0) { - printf("FIND SOLUTION!\n"); + //printf("FIND SOLUTION!\n"); printf("[SOL] flip: %lld, stem: %lld, fault:%lld. flip_cnt: %d, stem_cnt: %d, fault_cnt:%d\n", flip_total_weight, stem_total_weight, fault_total_weight, flip_total_cnt, stem_total_cnt, fault_total_cnt); break; } @@ -111,7 +109,7 @@ bool Circuit::local_search(std::unordered_set &faults) { CC[suc->id] = 1; } - printf("[UP] flip: %lld, stem: %lld, fault:%lld. flip_cnt: %lld, stem_cnt: %lld, fault_cnt:%lld\n", flip_total_weight, stem_total_weight, fault_total_weight, flip_total_cnt, stem_total_cnt, fault_total_cnt); + //printf("[UP] flip: %lld, stem: %lld, fault:%lld. flip_cnt: %lld, stem_cnt: %lld, fault_cnt:%lld\n", flip_total_weight, stem_total_weight, fault_total_weight, flip_total_cnt, stem_total_cnt, fault_total_cnt); } } @@ -131,7 +129,7 @@ bool Circuit::local_search(std::unordered_set &faults) { if(tmp.size() == faults.size()) pattern--; - printf("coverage: %.4f\tpattern: %d\tbefore: %d\tnow: %d\n", (double)(original_faults - faults.size()) / (original_faults), ++pattern, tmp.size(), faults.size()); + printf("coverage: %.3f%%\tpattern: %d\tbefore: %d\tnow: %d\n", (double)(original_faults - faults.size()) / (original_faults) * 100, ++pattern, tmp.size(), faults.size()); //if(tmp.size() == faults.size()) return false; diff --git a/run_exp.py b/run_exp.py new file mode 100644 index 0000000..b547197 --- /dev/null +++ b/run_exp.py @@ -0,0 +1,225 @@ +import os +from concurrent.futures import ThreadPoolExecutor, wait, ALL_COMPLETED, FIRST_COMPLETED, as_completed +import time +import re + +pool = ThreadPoolExecutor(max_workers=7) + +TIMEOUT = 60 + +work_dir = "." +data_dir = "./bench_test" +data_suffix = ".bench" + +res_dir = "exp_result" + +class ExitStatus: + normal = 0 + timeout = 1 + runtime_error = 2 + +def run_shell_command(command, output_file, timeout): + res = 0 + + T1 = time.time() + if timeout: res = os.system("timeout %ds stdbuf -oL %s > %s 2>&1 " % ( timeout, command, output_file )) + else: res = os.system("%s > %s 2>&1 " % (command, output_file)) + T2 = time.time() + + exec_time = T2 - T1 + exit_status = ExitStatus.normal + + # if(res == 31744): + # exit_status = ExitStatus.timeout + # if(res != 0): + # exit_status = ExitStatus.runtime_error + + return (exit_status, exec_time) + +class AtalantaSolver: + name = "Atalanta" + def run(filename, output_file, timeout): + return run_shell_command("./Atalanta/atalanta -b 10000 %s" % filename, output_file, timeout) + + def analyse(output_file): + content = open(output_file, "r").read() + p1 = re.compile(r'Fault coverage\s*:\s*(\d+\.\d+)\s*%', re.S) + coverage = p1.findall(content)[0] + p2 = re.compile(r'Number of test patterns before compaction\s*:\s*(\d+)', re.S) + cube = p2.findall(content)[0] + p3 = re.compile(r'Number of test patterns after compaction\s*:\s*(\d+)', re.S) + pattern = p3.findall(content)[0] + return (coverage, cube, pattern) + +class ATPGLS: + name = "ATPG-LS" + def run(filename, output_file, timeout): + return run_shell_command("./crun %s" % filename, output_file, timeout) + + def analyse(output_file): + content = open(output_file, "r").read() + p1 = re.compile(r'coverage\s*:\s*(\d+\.\d+)\s*%', re.S) + coverage = p1.findall(content)[-1] + p2 = re.compile(r'pattern\s*:\s*(\d+)', re.S) + cube = p2.findall(content)[-1] + p3 = re.compile(r'pattern\s*:\s*(\d+)', re.S) + pattern = p3.findall(content)[-1] + return (coverage, cube, pattern) + +class TGPro: + name = "TGPro" + def run(filename, output_file, timeout): + return run_shell_command("./tg-pro/bin/atpgSat %s" % filename, output_file, timeout) + + def analyse(output_file): + content = open(output_file, "r").read() + + total = re.compile(r'Total: (\d+)', re.S).findall(content)[1] + detectable = re.compile(r'Detectable: (\d+)', re.S).findall(content)[0] + undetectable = re.compile(r'Undetectable: (\d+)', re.S).findall(content)[0] + + print(detectable, undetectable, total) + + coverage = str((int(undetectable) + int(detectable)) / int(total) * 100) + "%" + cube = "-*-" + pattern = "-*-" + + return (coverage, cube, pattern) + +class OpenTPG: + name = "OpenTPG" + def run(filename, output_file, timeout): + (path, filename) = os.path.split(filename) + fault_file = os.path.join(res_dir,"%s_%s.txt" % (solver.name, filename)) + cube_file = os.path.join(res_dir,"%s_%s.txt" % (solver.name, filename)) + + return run_shell_command("./OpenTPG/opentpg/opentpg -n %s -f %s -c /dev/null -u %s" \ + % (filename, output_file), output_file, timeout) + + def analyse(output_file): + content = open(output_file, "r").read() + p1 = re.compile(r'coverage:\s*:\s*(\d+\.\d+)\s*%', re.S) + coverage = p1.findall(content)[-1] + p2 = re.compile(r'pattern:\s*:\s*(\d+)', re.S) + cube = p2.findall(content)[-1] + p3 = re.compile(r'pattern:\s*:\s*(\d+)', re.S) + pattern = p3.findall(content)[-1] + return (coverage, cube, pattern) + +class Table: + def __init__(self, header): + self.header = header + self.col_size = len(header) + self.lines = [] + def add_line(self, cols): + if len(cols) != self.col_size: + raise Exception("cols number error! need %d but you have %d." % (self.col_size, len(cols))) + for var in cols: var = str(var) + self.lines.append(cols) + + def print_table(self): + col_widths = [] + for var in self.header: + col_widths.append(len(var)) + + for i in range(self.col_size): + for j in range(len(self.lines)): + self.lines[j][i] = str(self.lines[j][i]) + + + for i in range(self.col_size): + for line in self.lines: + col_widths[i] = max(col_widths[i], len(line[i])) + + table_with = 1 + for width in col_widths: + table_with = table_with + width + 3 + + for i in range(table_with): print("-", end="") + print() + + def print_with_filler(str, width, filler): + print(str, end="") + for i in range(len(str), width): + print(filler, end="") + + print("| ", end="") + for i in range(self.col_size): + print_with_filler(self.header[i], col_widths[i], " ") + print(" | ", end="") + + print() + + print("| ", end="") + for i in range(self.col_size): + print_with_filler("", col_widths[i], "-") + print(" | ", end="") + + print() + + for line in self.lines: + print("| ", end="") + for i in range(self.col_size): + print_with_filler(line[i], col_widths[i], " ") + print(" | ", end="") + print() + + for i in range(table_with): print("-", end="") + print() + +class Logger: + def __init__(self, filename): + self.f = open(filename, "w") + def log(self, str): + print(str) + self.f.write(str + "\n") + self.f.flush() + +table = None + +def multiprocess_run_solver(solver, input_file): + (path, filename) = os.path.split(input_file) + out_file = os.path.join(res_dir,"%s_%s.txt" % (solver.name, filename)) + + (status, time) = solver.run(input_file, out_file, TIMEOUT) + + fault = "-*-" + cube = "-*-" + pattern = "-*-" + + if status == ExitStatus.runtime_error: + fault = "Runtime Error" + elif status == ExitStatus.timeout: + fault = "Time Out" + else: + (f, c, p) = solver.analyse(out_file) + fault = f + cube = c + pattern = p + + table.add_line([input_file, fault, time, cube, pattern]) + + return input_file + +if __name__ == '__main__': + logger = Logger("check.log") + + os.chdir(work_dir) + os.makedirs(res_dir, exist_ok=True) + all_task = [] + + solver = ATPGLS + + table = Table(["data", "fault coverage(%s)" % solver.name, "time(%s)" % solver.name, "cube(%s)" % solver.name, "pattern(%s)" % solver.name ]) + + for filename in os.listdir(data_dir): + if not filename.endswith(data_suffix): continue + all_task.append(pool.submit(multiprocess_run_solver, solver, os.path.join(data_dir, filename))) + + s = 0 + for task in as_completed(all_task): + data = task.result() + s = s + 1 + logger.log("[{}/{}] 任务 {}".format(s, len(all_task), data)) + + table.print_table() \ No newline at end of file