From a9ba5d9bebc446d18f2acb14f833c3275bf50655 Mon Sep 17 00:00:00 2001
From: Yassine Ettayeb <yassine.ettayeb@student-cs.fr>
Date: Fri, 28 Mar 2025 09:20:20 +0100
Subject: [PATCH] add TP3 files empty
---
Pystan/config/__pycache__/cfg.cpython-312.pyc | Bin 0 -> 8171 bytes
.../constant_propagation.cpython-312.pyc | Bin 0 -> 7298 bytes
.../__pycache__/iteration.cpython-312.pyc | Bin 0 -> 4729 bytes
.../config/__pycache__/opsem.cpython-312.pyc | Bin 0 -> 3888 bytes
.../config/__pycache__/syntax.cpython-312.pyc | Bin 0 -> 10228 bytes
Pystan/config/example_interval.py | 4 +
Pystan/config/example_interval_eval_exp.py | 32 ++
Pystan/config/example_interval_reduce.py | 39 ++
Pystan/config/example_sign.py | 4 +
Pystan/config/example_sign_eval_exp.py | 28 ++
Pystan/config/example_sign_reduce.py | 33 ++
Pystan/config/example_widen.py | 61 +++
Pystan/config/interval_analysis.py | 406 ++++++++++++++++++
Pystan/config/sign_analysis.py | 338 +++++++++++++++
14 files changed, 945 insertions(+)
create mode 100644 Pystan/config/__pycache__/cfg.cpython-312.pyc
create mode 100644 Pystan/config/__pycache__/constant_propagation.cpython-312.pyc
create mode 100644 Pystan/config/__pycache__/iteration.cpython-312.pyc
create mode 100644 Pystan/config/__pycache__/opsem.cpython-312.pyc
create mode 100644 Pystan/config/__pycache__/syntax.cpython-312.pyc
create mode 100644 Pystan/config/example_interval.py
create mode 100644 Pystan/config/example_interval_eval_exp.py
create mode 100644 Pystan/config/example_interval_reduce.py
create mode 100644 Pystan/config/example_sign.py
create mode 100644 Pystan/config/example_sign_eval_exp.py
create mode 100644 Pystan/config/example_sign_reduce.py
create mode 100644 Pystan/config/example_widen.py
create mode 100644 Pystan/config/interval_analysis.py
create mode 100644 Pystan/config/sign_analysis.py
diff --git a/Pystan/config/__pycache__/cfg.cpython-312.pyc b/Pystan/config/__pycache__/cfg.cpython-312.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..d1a918da4587190ec0ed293eb58376cf5c5ba3d9
GIT binary patch
literal 8171
zcmdT}U2GdycAj5y_%G_uvSL|dM@h^?a@LORW}V&a+Lq(kQMB2$+ya7PV#FCrv}w|w
z86_4&rAh6yjMrIH$b)D&fwkBI>%dzyed=o;ioWcNR2c|6aDgpapx8IY3J}0g{mvZ@
zMRKWin|<nqbmrcB?mhS3bIv{Ip2OcpB0&!2@QsIaD_tD-pVaUQ!=SO*%X8ccr*qSs
z&g(*!|2u)FnwS+XiPIv_8KS_Q;&kacr_1*Rcl!N0m1(Jt^#SWQr2AqUUasR6-~%1-
zzB)b#e5eE7U&n`mk95E*Y;RFuW8U7T1FWwLeep(LQ13Q^dXEv%d-30Ag!FzRkPhlQ
zu1nKlHhuu(cQ(dH76%hgX$i3AL_TMm`K+4G=HFH4OzrZ#6%3B46WXkiRkfV1W^7Bf
z7G_gf&9V$j)eS3UW@Zi5o;TDi8<o$ohM~^^pHH*KiS#K8WG3?%-<V^mIckrp?`G_I
z5LYvL(-NtaVOe>Trk$dFG)>doodI(qJ=fBoO3#g|nf=CowLZqBoyleFjFuf$)0rH7
z=pcq^=1q48Ae3InrR)s04hm|@G&CC<)mSTyVRX8=%sWO-y=>;emP^6kljsw?!#@uY
z&^23QEJ@W>g?+$JRyLuHP&$K~=An3k&QFVrLPB(8#@52{oRKrkOiE=GR9cTQ?>U#D
z)?`9*lw>leT{4nMCzwoL%IgbRs)v)wD+^k-j`1gxdOnp*e!*?hvX9?R9i2I68KyP!
z(o07U9GMw6tc!O3^32(Z<kVX;$8y?PTeD{{<)UHEr1H6RW^P8yX%>3N(m10wmKr;F
zXzbwOnYR|vne)bgMf)!=nm(+-Ko}KE0l3cnhm@#Fib*{T)tMdrK)13(7p`;D(xQly
z$`fZVW-b?Yy2@msuI|(GkVY<V&u4OTiIm4yP+>&`+>`)TxJ5o8Oga+HGDGP3f=9#1
zrY)MInh`(;Y_e=KnJh%uO8e{0Uf?Vl-~+B2>tjclOvt7mJtiH_3=kkYV$x7X-aRN$
zHDex#qhir8;>OdP0x$Qw!)QbcKWN`nHb()r_;C*QXj(KRL)L{K0Au)26RAd4Y1+Ri
zCwz`Han`U4UATmqx!ffqXS=%Mi0^2oBN<mOn=Ndjr5KxDW=j>h3;4E|J6IT)y3uRK
z-r+tM&vIaGK~j(YP)!Kt4xr5e0^I;j>}AX;glT&oXLr$vrvSj&?*5g1%lpcMl|!r2
zuLHjfRNh;Qy|AXdQ0KSOiQkS0c{#CUQp-UHG`gl1ls|CHgxxraqjnSsDVa%twrY{c
zK7v37tAX&f*Q>#vYd;~;jJl$sVVy;@7ntouql*xTZ&6CfP}?cPvI{}j4Nn#l?v&ml
z24XD}gUZM<cB9r_z;1!D`!WBc1aA%l-<i!3wy4MFr!meVae&Y9?((6P?=OG9{6gt3
z*Oc9L_WC=rS2>=~XBi(!NFABEn-BzOFBWMsF|)TC?7lWhd>nT9NF)A4K1vfOO|uYk
ztuwO$j)+DJ8;OOCjjnXIXQM7Ky%nLipt|odp8z|b!R*fL4Aa^kH=oBas}F#<*;m$A
z=9lNo)0Hc0u{~?bo<GV^>5nsWgf>9nSz5wlW?wZBxptbExz}YTjc8$}XZJSgLTxD}
zSqs;GGIf-hI!fef3kS%-dOnzW^SZMoFW%AHrkZbmo4OWZ9g<kuEpr@N-j=vUnA*vN
z;E1`5?#R|cDrLb+^kAqt24E2>wQhjn%g7;<1*Tns;coLq8c41Z9PjBbNjH^h-;R>>
zNs#fQMFZM)w!H?_FH%9Kl~hQdcC(H2>ziTD;UMjWwolUUFWW0um#>yDw8-Aq=`xvg
zh>ll?^vNW^_(4*?&i$M8$|FIL2R3~TsnduSsgv)avN;8?CG~T7sTz{bGY=sfzMa6L
z%{)ecW18UCCBv5%bQ!NcMfVv#yjgv^f)}Br2hxfjM1OEGkO(<4dto_pZZ=8cBdxKX
z#P97j0e-?H0YM#npa_jH525)7Tqjl)qHO7g4je_Frvv>E{>@Oc4mdv3uoui+%ibE+
z;IA=vg|izv+1Z!fuj7}X%~$zO-cIKWaOo*wOS{=f3FO;Kk)QL%(t%ki@?^RT-`jdb
z=8SjQJJWmUs%g`(=Dquu%i}$b>+*ZrS3+beVje-AF|B@y9Er)K<raZ#l6pNBdhJ&+
z*Ln%y1Ma_KJ>~J0H<sVnh^Zy1s)TQaZiLEL)|G)zLevW02$t<~dR^J|Nw6C0DTUZg
zbA;Rh{2z4q>}0C>)Kq77_n%Q&;m96bK&`#J!<+q#W9<mEn>g0M7KQIXM`&<<iw@se
zo}e$Lx5hX0gC2{8e`%EyJ-qh^)p|MYMlX!_s%9GW2355z!UKI#&A4$+-K-))SY$&q
zT{rY55;RJ))s$u#qnNLz=8e=vHDjrlG*~2t)0ld=p$bJB7GC;LkH$7I*jw~6REJ)B
zEOfEAmVxbcFWG*uBO$q#mu!RiLjp`ENPKiK_Zh5^zR+=-^@rLgG0b`k-~+A}=EBkP
z)XMbo^m=Hx8t%Gv=Ej-I!OF;bc=sn~s-ejCI3;*XxuKM2EAjH5mtTj5{lX0k5}`J;
z>4+JGob>W=q-+Mpml;ZCMqfdv8)p2NYV@FYT_dh1XOf9#;4muIYXBc{)ll>r_7y8j
zA0OS2`hF)p$LwoOk>%dX$R>wREgF=EDkC)xpVdR`bMG+wd^z<Eb-GIsb%&pGc*Ef{
zj-1J1XXc-wv*kumOu%l$LogRNLcGe`=yHqBS72d2{N4<jJiO%v8rfF7)WVVkJVhUE
z1-dKQ6oathjrI}`pemgOZLI3K3B2Je0#<!%2F7AZUh@4(D-+9EDau8kmo8{peY-vL
zHi^ic>GLdZ(>!n2QEyaz*L&Em{YwhZ*%U~zQY1?w6#e%}fl-zMZMZ;D@o;r+&?}e~
z(1lDs{O=j?ekr&VS_(grACd1YsfbPQMOKQz4yWFZThi7%o1&F=3U!Os#J}w*HS@j0
z4%+w@DTX}0Ek)aKQZd}X#l9m)qEFD>&ZmeyVHVRJn_^E^>YDQ#ra8f-t|#m@{sjE?
z_b|RCrT-VwjTgHb670sQJ6V_RqVQzva)$dW@|6FoEnLlHGn%=$l`XUL>g+-$i@Y6D
zai^HWvbBqpI>Vnix4<$J^;Fy_%c8k~9eGr@O*IwSCDTT3$0aatsHp|hBsa&*?gGoq
zxmi1Mk4>GFjzoHARCV8lR)YXb^to;oDaa1w*huD55)nr}O*to%`I{d@t5`P2kxnCt
z!BPk;T4U`ijvwi-Bv^q-NS5j>Dt6@KCnt?LbWP;*mlHka2_iC1fV`<m&dK4^TUirF
zPG?NZc6^pWNdkwz#G-sBWSa{{a@N#xsd*=y*0NTk#oLZxryU`kcBI+7zUT;<S+r(Z
zlv01MG=G?vH{YP;3H%iQ77w4myn3js8tJ`x?iYVijdk5Bd|dc>v2>ss3g0^V@zJtY
z;Xixk&T|h!d#l|&rI%}dF4|X9xah8%Q@75S&R4tQE5YU9r{U7EYB+N1%*SWSS1R$(
z4y}r-<9A+t5PrV3SGsfbLHOBfPjBh<S^z|9K`yG^ocby<ycQXL*tMg=SN2qnRg8_U
zk<zh;J%g14m7i9wtoCp8>{|=(tH~H$^KsFGH_v?)Ij|l%(7b%-og7~6z4OY0@N>=k
zIQ+MLtM;#++IVX0L3n>N0%<6=!H4mIN}R3z-bVa|(($c!aU(ujI^Mi&{nTb<&u1s^
zoO%!*@d!5cu=DP~zP}mZqCH<lhLDk28C)LxbXP}OS1R3~om?Hc^TvblK93r4^?$wZ
zpRGz8@n=B$4>!lQ66d13Yu#LYsJ!4t(@=*-@!lnyq^Hdx=5~olmXefM=t;>*nQA(I
z6q)wxen4eWNdz46M0&0eqezl|AfRkIOa!|bjsh#dVizaCLVq#>PLSPM*4>hY@PRn(
za1#%mmiW$l4K?Q>VCNc<80OSVC)?LF+dDtK(f;qV>#q`yvqRo`o#~*L&eB%U+jzTe
zp^Cg`yK%b4tVPbGTyethK7LQ2?i#JPsdk<K-F1^<b1(fuGHp)3una{Z4B<3_?hk3m
zn*bkh599rxQrPXQ4(z(?yY0IhyB*sYNT4TD-8po(|91b~;oHL-JD*2S^x@#1)sbI6
z`^#tV_5S_P7eim#|M>nty#G(e#^409HZfPv8qpTW(>a+W@tYeYsq++rcZwi8NnxCO
z8<D}1KyN{0s)f%5iqb(rxX_RQ=+_HI<Ne6q1R~zn_<^q|VU|=B0p-tSckay|iMu%}
z;eDz5I!lL*7V9hVy1%ou+D0iD74&wp^=%!6EJ0w>;R?dhU_nsTf~<~>y{bOugM|p)
z3D<Wa@+(A}d>OUFxI7JP!sq%LmSCaS&(#7_0F#sgzhF=n%MlSbnv`5|B-}{b5s_MD
zzjiQ};rfbRpbH^aF<27pZ_r`=1^`L0Xje(B_71GPw*1=4#PY-=P7I8d#;f62dAxk2
z(o^2G9v&*4sP5i-_rmQ9k2pRuwj3<?mQ&TPp0Zhay3$uMR>xP5-0NQJ8(r@jT^7F<
zF{UPi44g|KTw1D3-93N%{MxS3d&k!zFRm*uVnHQTdcUII&EL+i4eh@-y9O7a9B})K
zmGQf8-hQ+4qkDVTB4g{y7`kKKB{x|(nFzFnneHz)EM}xwvnk4?W4Fha6tbBF-owB3
z48TW7*6pnN>Boa8lHSOcT>DA2t9L`{eI!WooBU=tAosYTBh8ykMA?e)@QXQHyXu4*
zKM_I@q_A#aOL;)|iLsk%BLr9g%;Hb^Gz&Y~on~7i3*#<A@zrDH2kuXSubOm==&D%{
z0cs-8^Ir>oUizks<NN-d+w(g<_^lxDff@&}DRM%n#+nLh-v}b#Upl$T;ZsMU20u+G
znIA13M%>Jg)={X{q6{VR!!!$@Itn!;3}}|b@1<GzG*ElL4g2`LUvmK8b`A1FUvmJp
nm-q2QC8NgSQ`Xt1GQ~dkWcK+IF*|VIPVs$w&m#_io&J9SU|VeV
literal 0
HcmV?d00001
diff --git a/Pystan/config/__pycache__/constant_propagation.cpython-312.pyc b/Pystan/config/__pycache__/constant_propagation.cpython-312.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..81e97440258bf50a9ef41dacea62fdda37d6c587
GIT binary patch
literal 7298
zcmds6Yit|G5#GH!zF(rKhZRdQW5>2=$95z?lh}@}NO=^l;zm-OGD?UO?<7;ENagNi
ziz<~Wt&7m9TFZ?CF=&6#XaLJ_f+|3Pv_OI8UkmgPRiX`ZP|y_ZpY|6MrD>aAo!L9S
z3_3wu^iLPy?A*@I?(EF&w-5ft<8cy5Pn`U4a;BM(KjB9?*-U101DF*ekuZ^{#Kq|}
z7v?DPe4L*a!osvAY?-!(t<$!!ZQ35TGno)~OgqC)##`d9w?RYZI3iguliOy)<vi?`
zY?57aTqYCz+pe(3K_n-9yUcGde7j|j<dJ=nS9Z%y9iT7S=fS=StK_>Zg#D(xnaKln
z@+OeCaO80!`7aZxS$4`^l;7qJBf_mIdnhn}zcV&H6PKsugr)|?U^JOfH8G(DXO!fO
zI4NqeWFjag#CS@Lsm{NkYKZC%Nz}w>TvXMNMYo(0$K^O=!xv&Rx^QM#*5G4ARyFt-
zR1~OhA5p}FIw2!Z_e2c?3~GT4E!sQ;<Q4h~hyH%sHb-COCg`ga?a$B*H^E8tvR&e?
z(6^lnBwZQBFbVNG9jR*)o5Qr(2jq2VP$pptLFCSnH4^4WA%I~4cnB%FQnpC^ai}Q?
zmr2-~;$TQ#aa`3DF{(u_it$-_{@_qDAqQg#DHatqSq*CEMJ;$q4ob<yZY_8rk-P*&
zGWbl6##A}Tl!kN*%cB%+F%$9u_-%FqS%Gm(nS$Evhh&)CqC+97_@MX})df|KPpGIH
z{5%nTXlzuK6?N?3!6Us##s*~df|i^a8$J^mIXiYbAr5PzHYO#b7i47&qB#+p9E12l
zP_=y%ia0Iqi|*??w6E{**x3|Dx?HCm_()CQ_s^tsTO<Omh(zYw>V2}`Ecb#{Dw0J~
zY;IfGb8XLZXWrhu2_+<C)9sN+LY$T(5#1SyOedw;IP&gD<i%MrZc2QSh?bg>BQqk{
zr-B&zgaH5p5;2iTg6%L3L87!`tDNrMU!$P7p-|<3EG{Z7kSS;mBe=xXHX#3a1?>By
zaN+}(JEL7W_U)%OIcnLapomqxh11Bhe^O4!N-P=~7s10_C}eHpgbJQI#Tx&7*KxB}
zkl8D15Q|`PB3SR9lS&YjSpR7AKNrbHYun$6K({gSF><VX-Ca?X6Bmc-Cb9sU*!SiU
zAS*-zY9tLu%aVq549;5SaFtJRNQa5yhb$!M0!&>^=OL7AygDCCXi7K83?DGJ-HV?{
zP=~o~kz616QQ$|3w}#idd-EN=>n(kG(r4Ih!6_xz*^5>&d$GA%dnJMkt!xcto!r^`
zF3?esw8KwDzb}%dvFyOQCzvNeqfZ`Oq*Gb9DzY}KB%&2JK<$dN9sm<yY0)`ab(lo6
z@cpuH3>MJ>0J4T=vXtg-<HCY8Oeg`JibG8uFVo>EN%LuPktmilaE5bJ&=P1=91j{C
z^fEdIb}a}C7U;)ev`t{Cr!BWldl#%}>mp5YY3mf*gvxb{e9=|4PO7mkEokT!mZoru
z-;pl#U^J_`jazq->Uhz9t*P7$SkHs?e;)(iEZ7$83ywPL?G@{tb>)sqxhw5_nM=Fa
z$efKv_Od(eYE*vL5yLj1!RBnFDV$YzBsS(9b@6Q2bK`#Jp|z?v>iR-txFh|SeZfXo
z?W<-~TkhxvK3PwFjct~ACWYBk6X}0v%rFP5cHj*73i%cd3G-1Iw<}oEu-ykmC8nL9
zmbF+kD9^#RrmA=jh~ZJ70(3!Gj4>sdz@vjR2+3HKYS7#)gHb?HL`GRrl8R9S5obuj
zWf1b{meYfe0wCd3M*bO5!E7`+qdU-+h=^U|7O3-B$Uk-VELP}8o{`f713LfJ(K9+f
z@Z>Wgw*m`*C?O<<)<tNMpM~lIwxshg4xJyz_T%z|7GZ@>B{q59<hhHzI(M;;fe#L-
zoQz%N05*(dEBw^218OXilAXBRMNh}l=+&_|_ph}Uwja%JJ(?LSdfK5VT=X?BN3YE1
zcI2Wrda{ocJGx31;@wiR5^opCBbmrX^VaO6Iib+JGxI3a&U_<x2(qiGE2+FM_*VDN
zghJ><e)|b1yB=Mcyf*pjOK&FDqVLAuiLHeTyH4e|ohk;}OD<^dQ#bJj-uK*}_uRkX
zzbAVzn=1H2nSO(xFZlOl`ink)W<L9LHoPVPdv)&0T;8`W*LU;Sjbr&82RGVx=A=UV
z-h9*EVsmS;we$M$%DLCiz4^jg|GQ7T^Tf}d{^heje|G)QU}5KD`R>QQOuo^&W#!!U
zbH(<KmAPwkx!xZvtd4AK4XtkfNzbhwqs8?-#|v9e<XcXFQ`)*p0pi_P+CuzY%d-sa
z8>9PQVe;Gs-TND$I{|zzqb{H388-1#6^w^Snh7wdeC#K+s9P;fH`Igmc(is!u^qu)
zZq?ioCTn(t>dr&bLd7;~&1$aQDQsygV5-gBEgIMjm}>hE$75}z*SIyroGNOtF;;f2
z|C=%1Q$NP)ZVMyC)58%qzw8=<3rn!4S9e86+QFjaXynyJF6|g5HFK$9Eq9%dO<dkv
zJ|6~6fJP+7^JZ{7nT*Q-$cSSGLbEfKiLZ9u)<1YQF2)iJv=}5BSS$1o4!)>c`UlU*
zEE|$1O~f6Crb5mtj_MYM!OBB0Tm|n)$_XSVkvxLrK_EK4sN!TOqa|zv>^M1y6_6Z*
zpNiL@Me>o;RrG9KI(PL21Nd4C&AY!4_%;If=62i+-3YCI?Z*9uz=6E`K*>S8oh2vn
z_AHIO@7bOA>}D93b1;lEcxS=C_sj6^7el{3R5*S%fA}nRvi)Yyjh@x<pPavSetr9q
zLf~lLeH3xErv$hfS{i-d)06k~{4aY7F$Dkqa~n+^*&SJ_(6l3Sy69`lq;f5gUA=VW
zQs$ev7jt&BR=hcRV=}k55ZIr0??;DpfJ3Ut2@bEMG8S$A6pE^M;ZY*<vViAUxc^di
z|K;%hEAg@oF53b;9@tIZ0=z@A$~MUcKa^V~JCr$V%3M(9fHJq_H0ucPj3I<Q?At91
z@QC4Mx^~G6<vv#Klbg);@Ug<r$~<zjS>}hbK&m+u&|4lgpCxK<r@907_n0^ym({wh
z0s$6(oA<E+Yv%DDj^MNmVQCVnl%~u(5~nv;+KVJ7A~ARfQIxMh8zD}?JG*XSMeL?&
z&T+in#u70NuE$-COoU6aAsz*N^On5Pv3GT_(9xF>zUMVAUwc4U_eucY#t0DaSBPn$
zabd#au<;bYR+(-cPik6ndVXue{te-?sDlqJa7XtAjLo$&ekjI`k9lkan7h4743Mid
z%Ed^Odmc_~3p7ouTb5J-uGhGwCIRX!&|#pIahJ*-X5M5NWV%#&96GFXsFV4NT`lLg
zH5^j4!gHvML55-V9)7p`o$lZJPOY9^rq@sA?kfa#uQ%=ft?yLce(Il)sp!kAft`ZR
zsc_0u`=U7FazY{Vz%PKo;{^aVHw=dd$YCTgvH+LAsdDX_e1JUPkC(kPO|!)`Wga$a
zs*nXsn)?E&HEl^-*`eO2VUSpY%c2<}xONJ-JeLkvrB#1dqyqw6OUpNG-taVTREE24
zYz8aCSb#ys8?-tb*H{2_0Z!Y!jP|KG7fd8KCYUglj3wqf8pZ-eFMxtN0|cVr@?;*$
zjxVRGj6aaE7X7U&-PgK5Ay!8(Kw6-6S-f_5<>6}&X9ns&e1T={)$~T^p4CHz&IgvQ
z%P;=G@#ng)k_Xx-c}Y`S#$(Lm+9)E=qWCRfSQKfBLJaY$eYfbr;)B>y<4WH!dICg`
zUHBVHEootqF5Q<F(iS`js&r`&B`HoIDH`I3MjnHiju^tW-;ni=FfjKk=TOepD83{Z
z&NqB-k0qk<SxJ`e0xxCp1<+H!2BaJV$%uelalPQ^`V!Z#!&P8lb>PQmK4|YOIiP;Y
zNt#-ilXY5;usAcBpV40QvpMe=LY0^H7}|uZp^TL_ct%v=iFm%V;aoDMv!JnwlMu10
zDPuPv5^;jv?4r0*%L#dAhlyJhA`R9|)nc1jxBTM1AXHHcqh2|HThbP$4e?BKxZcu2
zc{Opm5KYdc*fFXcLL8kDJ-lz~wuF2sf{#-?EG6~MFj{eJvUV4YHiUD~jCvRdhR~gP
zFgsFg4y^3Dw(GT?jBUf)o~7B|?<O;R(dErN40pa_>z0gdnO<=geQg<IBhhKJ4%EIl
zOuR7{*+69M96bq>&zN}_EO_bG?j9_Zz6>f#1PQ*E{D+;R1M53Sf5D@{-Tei^%XM83
zg<2GRH&nJD!BdUym{5}QasvFW+=qpoNQRK?LUI<#(@4G!L>KTdt>BKLAfV}v)A#~1
z2q$Yr!f$&&$l2#4tIpUMR>vm|W0JNY_hgwM)~de(@*SASTe5*GFBOEYPvF`4V981?
zEm_MZfeiW6G&_hNr)kORva~IamI!27nPsa`557wG*g<D!i9nVcWZ9~;iC?7_YVl_+
zC1}8(+llS?OIDkueR;M-Aj|PamSWl3=q47Hnrn2nFx6GrR0RpDVrzmSY5f$xj4|Ty
zLTw5@f#|Nvzd*98;Ox=)=)|NV0H@$arr<hIa4jo%2-O`icq?a5`HBO-t!gTviF0g+
zGM<E4Wa6l>6A629nMMu)j@=~;|JM8bbNg}QpM{f(3iWW>t8V})@s!e!IgSc{vlF`g
z59Gk_$bk<@_XcVCh&n&x;0b<{C!DK<+-Gh=4<aXg<|Opq5=W^}vTmha%g0LuvfPs_
zTigF$V7+hf*TQ<=nN2J&J=9^;fh_k#i9oj2{hqMii*<UT4itQPq>uWu$8v*jJn}aJ
IEOX_*0K;G*DgXcg
literal 0
HcmV?d00001
diff --git a/Pystan/config/__pycache__/iteration.cpython-312.pyc b/Pystan/config/__pycache__/iteration.cpython-312.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..68239e3f063ee6b0b9390a069426261f16cd1692
GIT binary patch
literal 4729
zcmahMZEO_R@x8sh^L_e!wh1Oa!UCb-fK4!jGzd^AP!iQ8P!rL(SDlvKcV^*k_jtR9
zKXj+M5)x;G6kCEAt3Lp#m5dM-mHH#C`lFSqs#5=ix)JV5ku0@;`p?0sNFzn+%-g*?
z-vQ!D_x8P+c{B57=4R&oEs=;47~==N7=6E!kbmK(HY9(sdKeaSL?<Ier@EA<4<w4K
zKwc^YMgo*bM3=9S`#$-I4Ex}keQ+Yw*Ead5?;GPq%P<|qa2Qt|i!0V;#uZgLnmZAV
z_A6(&YT7w~7&ZXUsWwxzylUHub6$0nLdkZNb4)Qz+fhx&P#vZ#Ig3Y`s-0H=<`|ly
znreQ+HtYdlm-EGCJ#mI*Dw<U&mK=ucYuK6&T5c4%fh?ws8kd<Fb?WK}i5iRk2QS!1
zUHZm7>V{8o%ds>ould&&pAgIe_z9C;rB@|1+k>`odQHmFYg8g9NR?KloTSq$VO^T0
z526*~)H#&Nec9U#lfHmUhntv(eY(}Zz~UybW@LndSERG#AsGqibVSy1O@V#jiaZjm
z?_}78^dRE&keEHXklqHEwq^_q=R$fI;1NBthE~?20E_yt7>ns~7WXBD^#tG&KCYd$
z`|yyS1bEVi$5}@m-U0B`M5?dT4cGiWc{*>{4!WBuxss_l;IdZd7m9gSV5aYT@MDYP
zJ$DYN4nzY}hTRZnPKlcut((|ebirp8O+7~@XrDAWfI?ZJ=u8NXY?lIoXK7xPIhIl~
zFB>)llCGGR&g_%-2!w!avwY4**2*`Ub|CYi&A6S}yLbPd{h4FTzUWxR%<xe5%&E)~
zQyqo~&FGePk@1XXnK@%L1JR1=_vg4;Q2Vw1!F~OMZ)HwR0MM+_)Pr}RIN^rQS&m~B
zCX+Rj4S0YA-X;js6j=_(R$)P2dgC2<V-(L?u8MHOG~geW7neQB<G_!j4DYTy2}?JM
zG+Du5va7C71K5FwQaC|cA+BWaf#0Bpe~z`I)e$=`K#EYToZ^gGo_e-2cAl9^f$>qp
z997Q2-%>jdE)Z(n3-ESe$JgQX3QRT%P!z>eQbul*iMo2YMTrf?UaHUmFM=RDm6)fA
zh);t<I`Yg1>B=y*d`XAs0NsUM8Ms*YE!XpmTHzY~WU8)O4TP6ysOM5!tEFK;5DYe9
zGE6jcq)Z`C&`I5?<tpEy8n+;Cs><+1qo@cZ_|r0@QLu~{NAd*=E}-Ve)Cu^H)s8n}
z0{(yJRdbZ-^&`UGeUfMIG>ErRv6`jZ9G<m7+GI!lMm}T%l15;fA}dkSk*bEhh@h8U
z$}~US0oog_@vyb7Tl3XSj9O#V#AM*vxleAW#y0^suE1oY0KBpn5Fu2GIcxqw9zf7H
zqLpedjf?FsP)vdP;;gZ`ubdyJXg9tU^=gV!v>u*owjM&Z;DNegFV$+#3$;QQiy%-S
zoiWa#)(ML~M?d8m{m^W1rrB%&*w&=oNzCTitf>}QHtR;S*@C5)^0<y?vzJP0-p3@f
zS!bfivPBgVpAG1?Y!)(OHp@lQ=tia(HLiTlvhuta_pjkTU_0E69N~s@{`h#2b2N?{
z{vHsCEo$S+V!0ibeUcj=SR;tH0Z;_()Rc$@j!`M57-D`8)7MwYKjojSNK!C9Pge<i
zRzkQw(pb-)UP1W$X7RbZmZ}C4m^-?ECKyc3(-ndrbrnA=aX3GFNl@K7>Jh&qKEFvd
z<lq^gyY*x7xwpB2sU1BgFn3RXg>>Ri<=qHF9=eCbz$h~rH?%DFQhX3ED@-6l@7;HW
z4Zcwh`c#T=2ZP?s#{66R8z1KT;Gi%Nrl$W*k?WV9k~EF4;&fxjfAJ%PYk;l~G%d<m
z9f9d8t+zomM|Ik0c%~^jT9=%9lG6iDJtsJr<;0kVo(3s%p(=8auf#R!*D@r(pi9rV
z;ab$Y0qEm6cC<}d6WNHwvIA7Q3Cb9xB9-X{!Mb_6P*<b@KSqA~T|z2>asbZMm22QH
z?f}bnm&paRZp)}O#bv1+I0(4w-vK%_PRn?P?tn~2Nkx9X#0#QnZ)O2nZY3lG`d5OL
zP+7i!6}x3TpIbRt4&?&({T_*u>)T{fmif291516&&}oe_1J<mx329Qf4c$`-mqX*!
z!N0K>x^#<-)1R-)z>X5QIeMXGl*2WCm56Cjpm#6>hymv%IKM&MDq4vN9_wq^#<v_U
zN6WGM7;rFv&vC&AE3X*9hXSAV8MtF5F1TP;X&JyJe&6>$@YqU;gZWwvpTjGHLkw<$
z6{BUq`PiEC@Gy#y>%Rip%`Jqmg?I>}#mbTTi3CuB2U|xuQKPL<+Wj63<Eb2cK`a1s
zVYT*3@&&OFEVq}FO@8kcey7*JElc?RnEYA&!Q}Nk{`;-zoz!R^8a=ys*WnTIlJeen
zSc9#S1Me@TpcZXKJln9D#(IRbzAW7<OHom?(HUOf(dp7rHz=BKHzK-BTys$?Fx=dr
zUD7n$4XMQ<Gj%smw2E$U2pb@;cF04+%<(ElaOezFR#CiMdFVLj9Lt3$IilF~rTE(j
zfImHP+d$hQG@h=E0^RVK#V_JJ#SQ2%1@r1TmWRT`H8%p2*ATlAla2Yyz-5)YGJ|sE
z%GeaTacn}F?xST?+YJC4z8}QdSnBcWYll~@+|JsYweh0mKLYY$Ja-c!`)la1+R1Cm
z)QP2zuDRfBa4t3*dqU*kKviCfC1>`|9hyD#_n5Mje*JNJ_oMXg#q^%)iJ4>9ez=@|
z{q_g*A1tQ(z5PlA4gs$>2dCa!>gm0mm`^<J+4-nv=MzGMZ%xOmT~)Re?)W%4oxIg`
zd*l4Zg}}mxpY`nhJiKou02E(_Nvvz>)h)Mo&F{K%=@+}Flhr_VcxKyDckivEvqRO$
zN{A%8mr^}9)_t;GsI%))de_27i|My#BP#*YxnVh_+~}U$G_wh?sM^B&5A9EnEvAon
z_|40y^o@0My=%^XDleuFdDxBrPObao)y7F@F@4a(q?c2jOC3ERzDJp>%vSE4T^PQb
zdHBxa`a@MH^`xWcaZ-7dRPLk~#va=D%Ku0nT<YBpMmah?w7hA{?TPsbFhOE)Ha62e
zV*{tT<ZSXz*ByP~=x55CpLgtm>n8@E?1AgA>?iTAsgt5KLT`#W-whniK_Kad=D6}n
z2q$P!A_F?hsinMQdjWtUulTk3jThABX9M9dKU<50ov?sNxB>meZrb(B_ZCjy{ef8i
zRui8;=zre#SNg~Ozso;G0-@i@z7XF9=e&>)LDK{g&+$d+brcw8-ZKy%b6(>RKIpY~
qhxtbU!{T9Yfe8#i>6cQ7%3rk;+W7_PeJVqT@br`f!h`}s;{O4iqIa7B
literal 0
HcmV?d00001
diff --git a/Pystan/config/__pycache__/opsem.cpython-312.pyc b/Pystan/config/__pycache__/opsem.cpython-312.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..b416b2b688a0eff7fd24790cc3a7dd80c0147da9
GIT binary patch
literal 3888
zcmb_fOKcm*8J^{m%Qq>BQYcxbw2l)?j3v94Sj9=xG}Z&L16fu<$wplw#EKj~Y-*R;
zT`HooEaIXlm{f?RxPVx+KzUT_6tHhP_TCFs9?ULOz-W8vjfDgh@Tva{mk%j&QWPD4
z^Z4g~?acrE|L{+4w*x`Lp}!`7-i6TL$)ee8#^kUFlN}UCcTt>)n=;HFObm*%*o0YZ
zPM8K@H*Ut3xCNWz+=dmQ1Q)md%zT&o8jlrtY%Lxe@YqlA*s%k6IyE;nI)K}m=Yr0S
ze>-kvu`H-*Nfa`?f>#AmO~({IA<4X&!u*|7p3ewkGAAUl!?7q!Yw0*vc)TWLa#V^>
z<ir>eZ_B7D8Dn0_i>d%SF+P?N6a_0|juk<{ab6O6fyd%nT9(9BEUNsfkj<vWB)=xe
zX<;P;>Q#wPiz-fH8Hkx2RxUY~Qdq$q#$>GKWRYKxM9hDj!k|;+u`GkzQY@B}c|}^q
zK$kH;I-O4Pii)%C&kH*KN$w-a=*$~B3%)?Np4GXA(uJ6b>>AAsBMZO79-!_Zjag^Z
z<{sQ(3Dys|2!l`oZc;Oa5rcrErNQ9vP!1M2SPiWq*`mRW+;$k{K@KE{9oj&`1UfH9
zKu5t`urNr4IA}DGvOG3)7dVakl*yYkv)YU<bdN@0le;nAA4N!JHO^_+QeDk`u*8C;
zUq|5k3f6+HU_WNb*0SU{Mz^=<PR;Saq&cY<R@Kwgdk>=jWTReKG>7KgfUPjnI{AA}
zawF8iZz23@Uz10(K8DjKEzS}y#dGSOxkCe-%1bm@zCi;=H8?eA+)8KUtcm|{{*7Dv
z0R5B++BRM_&;Wr8K?p&trdBZte26I-D+++)cW7b5IxS@{g_oyaFyoE+?2X$mn9DM`
z&Y)AbT$`IwR5IKaWHKyES=~-lM+Fj`ELpR+78l7LsM1;5U7MZN*_+GrI;*I1&?S>F
zlHtUVZlTc8S%8(!=0Lzq{2}X%&aM#U8Jtj~l<1Jt$&@j-Q8MAOH>faGNX+mZ?L{>9
zc4S$>vJ#n`oVqd<nZ?R|Rmw)f^U<Zn$Td+2tAZMdOR@V{j>IG}kxoVgQBZ(7o{)uA
zVLUcI5gMQPZe%eJM6t;uWg!V&%I0MfO|)~uL>YrC{}erUxNGi#&E<!Yny<e&UuTi$
z%yYLN2zP7Vo~_tt8#Vu#(&YB~miM`Tux>}5{<;Hs0>BV0Mh|)hOEcx(YR`q@46qkJ
zsR0j%x_rNk?IgF8pZ}!RKe(lCIf<wbq>g%#$M?)VR&kFV`1!K0oUZ!6Q@noAf3AGK
zyix6+DBh@f{T1(U`K`+N(ASjths(iz|HVqz#aegoZ`j{je`Wo0sMe+)aj2(nEBvUx
z^rJs_U-;_$ZtU^sli2Sscd#6E_nyY!J6mSHe780@OjzIA_m5S&#)#8F<QcEOfw}`*
zxkETKbb20Jf}?y%9_w%BF_mOI+92bYT6kwQmSUX+<h@ByaBAin>BwB2ddw|7+%f&_
zjAqq1$R}26gVQML3>#e2A0s>d|7@ITd`CNn8X3Efo`p>%;YS;sL^~t4PQpb`fo1~p
z#!yEl;8!FmgGp6tWdWJw>4gU1Io&!vx0n&qA`NogJUut}k#3ouo5yrmz)1uBE1)1~
z?*ul<2eJ%~Bl#@p0;C%v-7x7$SyAlJweTwQgg(;jreLD{4LSo+gPV6Ae%L@qU$tkX
zjgFe{mD0KGtHoOcN@od_MmLw9xkoDQk^c@6HQ!(<zwaBZxJK(vkgmIsC%C!%%spCh
zkN!_8f=8gj_r;G-12ces>&@Z<adrTlB{-1J!Ds50v<TVp7#v7RrDgq9$iJt+0ZQ@%
zUj&$-WTShnFb0Cr9vkCJK+q`PrUI1wW5ttgfxxVpX`p|j_JTz-YZlG)4p`GHhOJh)
zH^9JCz;OjD*y;>du4T)n*@&%<T^p29QhA^mT2DR;F4Jd$z2GP~L9e&L3tk|t{Qz)j
zF8U2F+0~&NX^yt;V{~Vm4mw-U1minCpx<FHxWCPs()De3a?Gl`X|>?dJSWb<qjtBx
z%&xUKn-b(~D7e{;{tj@9@IHlz%F&l^1J*&iZn+V@pN2Xcld^f;d?Soi1KTkDNO#a$
zPUV1eMiS!`kuaZ^q-@aJKzI<mk^Q72Fs2~ats?$7N?xg!L|TS70;gc8sBzs3w5X6!
zu^eq|fMp;%!7&_Nkp(f9(p?Ft-mR65FhoghH?K(XyzXghAZvx(aw}^zCXL*2nK(nb
zAHq+$VpL;q&E31X{KXx}6FXP8uReOa;tG(W-1po)xViN3!=jN@j@R7UD+4>J?bM@t
z#rJE2L&f*EW<Hy*`OW}v-6YF+kcTH(X1L-WJ{TI^_3h&7P^fsT<{hedFF=_+@C8cJ
z?poD1RdG!bu=6A{O^~#5W#4_JkyheW|Hb0<MtugEzj*xzep0tTsrn}?U6cQy3$5x8
zRk}iTFNhy?(P|$!UEDVa$z^AKd;QTyrR&^5U}TrwU8)8qiVHPwpyGYqa7+9OKbhTo
zt$OJPRo{CR*L&n0F;wqur=p-sw??DzEQ&_q8p&Uzb=@3K$5ffTZ*>;__UQI&<Ow-P
zay)qi>9%R8BxFf0P0BQ*h6EtJ5*mLr(b2nlVS8s)isv%;U3nJ7;i{1G3+U=B!!Z9c
zaf}&0mFcUSgG^v6RANgrCF}P0>+o+VP|nlgNq8^x^zI>{)NeBb$Jt<6PSp_%PeOaI
wJ^kJxnbxPy1J`WHR|=Q>+c)b7mb<Uh0nWp>7vA$fz4^!4{m}IzvPGT!50lfqjsO4v
literal 0
HcmV?d00001
diff --git a/Pystan/config/__pycache__/syntax.cpython-312.pyc b/Pystan/config/__pycache__/syntax.cpython-312.pyc
new file mode 100644
index 0000000000000000000000000000000000000000..0e0cff17c20d02adfbd1992c523683af47651381
GIT binary patch
literal 10228
zcmcgyU2GfIm7ZUUq)1UBWl6SWYy2ZywEkkp)}Iq^EK5j~IEq`@iLENjj5s5iHATvI
zMz+aF+cb6nb=OE`G+U`~gUD!sSnvYtK5gDM?|m6V2Fwmzz(w~Zz&@y;7X|#(bMDOW
zM;h8`)9w}K+{=6J-<<E<bI!e^-v)zz2GX&AeLUS-&oF<)A5QYvh5XMshFNA5W}H!2
zg-fzC+&IT#nNRXF!nnXP9P>J(2sao-RJnV+)o)y+wH~OgDyj9*S})Z4?!ma2#;a6;
z*7~8gTCH+MxM#7Maj(q}06(aDxA1*7zXtdr7rx)-*8;!Jg<oy+!@!TY@B=o#9{Af_
z))%z-4Zv?ygIm^DWAmGUzuko&viUoJzte?ZYxA3dzsrSRN2RwLxGe>lhV4EQ)b3Hk
zTh<h@`FnxC&xK!a^Y;V4)rG&!<{tq5K^K05&2IyK)P>)u98$eXyV|5~-wrrW2};Ke
zVSESF2Fq$Yp?0UzrH0FDyP>u@^HTJ%9Ap`0G_9zbl%A6Gi>f3~YC4hQx};@Nx_nL2
ziK;rhS(2V6^2~tW-zl9-&vp-{XC<P}5>-=Ex-^%PNv3-;fte(egnn^G)e~_kJ*yH~
zPZQ{L5^IOA%@RpYDN;h$r1-@|QXy(ef+fUBViFcm?5RRaRnrpblm?v#)9K_3`c6U<
zRZdCe9Y<2|O3#@wf&96+4)gf^-{7u^vZgScnwx>#r^vb-Ps*AWxAzmxKx{PScR;qx
zsLVJEJDgM4abDrZ1%<!CjEfl|Dw;e<D%(zlQxJvLC7qfh@Y;GZBc)S7EdER)HK%=p
zW5=Bda2DL?XcqE^fGjifj1IY#erOv3=Qrka3}G{DhKur}&)80riE;#uk;%Vv=FA$r
znWiSEG#p=g_Cb7L;+&=uZQ|vZdk*(Z45`{BJv}=yb~<+U%*4r*Jf_R~gp!V5QprR-
zotjEaPsk}*gWAq1PzAX&-g)F`=aFL*XEIQka@ttR(>0qht70*bZY-9q203)uKSD6M
z76I}RldBGW_VRM?t=^yfQ!dhw3)SVJni-9HOm8ffl4sOd%=E`%GihZmiRC~nc6m-t
z+8h`i78i?=YUo68*foaKVz~whzBVNRC}_yO!Te4*mh)GCbSlsBV%Tbn&D_!53mi9e
z$3;aL_b4KuT$S-et4tpDLblIVen;cA0ZCSr1S(dCG&7gf6SK)gT(*AW4p0(T5~$v!
z3g-C+q5KAME(0GcDEJ>i0l~k<J|F%|ZSd0IVKQu4O98rXN`;nO$%u~MDrrmGu^B$Y
zL<LZ(c9T8yjO~sJq!AjK{K=sqlYjf%X_Frsd6!U8Q|+=aK&fY|K|BulXs@&bKmh!j
zaIUWDv&eGezc;Q%N{Wx`>X#cogSw?g3ejlPOX{Et2_r$xA>eNrvKvVY5(x>;MYbU+
z>Hw~hE)+XxI63OTAk~2)$#a6(YW2bn?%IHZmTLoUGB6cjr?SVV)s#xW-ce&AO{Gbx
z8S0Q!FnubRp`v+%7Pi3}T@zeiZ_}%wHWDQG#+nxhzRGY;@LDTJ)?c-9U%?<}+qN#h
zWT_<vb(HLbX*Nr_73+{7(_Y#igd>HeA**a@JXB!H<D!c~JqLl&IIjw-sBo_UhZ<53
zHKgLn;ZvHPtxKeIbs8iI<_JxWu9@N$IXS16?HW`-oFd;$ho5JD2>Ir8n;B!)*wH9U
zV9PM>nj56EI=b5d?eb_^KzG9p%ZF|qT52}DyKNn<as$!iVZml77L!w{G}uk_W?-<~
zRP`XP0tqgMnyXKkKL|T>)iu}O%yX>RV!@0pzPl{nm5J%Q0vOAaNmVm>D7s6~@^J1F
z9AgOjB#_`?$SO(@=5i$XGQJvGYmi_l^3!WSxwaU3zWBg>kWL)kO=R83K!Q&}WRaXN
zaQzJwS(7C)<hqLt5v{C#ss|L2r-~?0TQ7oR0!2ih9xC<efU3#QrDsh6w@R5HIhcW}
zVh^3lU68lIu)F#4+sx;jBV>-?2&5N@tCa;^Epf8Pp&hk%maewlYFpZ|GW5mBFGg05
z8=-@S_n<9zchgFJCzU(h+aa8FlRY|ybx3es8roOX*X>mJIe+B(JBUD=g#b2lN5B$`
z6G3e@07V37NuXF1{VrgEp0~El^HMM-0SsSKozi27i0LPZ>5Epm3?1~m6rFdW0LL`8
z5<Uu72_c0Cj*EM}4TrkVtHzk92u`yt%SELuC$&9eqfwsVYY;?;yo#g}oF#5^2-<1w
zKt5ug)P<LhE}yt{!U*qO-Mf1B%ky{6ufBPA@_zk)wfv^Vc<JQVbw=ov;XU<SfT?4A
zKEMOGHY6u-ax|p~@D2;$P}925l&jsoE^N<poH)c<Kx6YVpq)rIU%`EPoxncZy444{
zMD*?sXb`3)NZx>_;DEXd4hUIg%R<mGeR~H~H8^}GDJN3dR#(p`wZSPul@e1D*m>!t
zs42=@Y{9p7OO9C`h84PNN621{V_3h3Em1!#(AQj@5p~g(ttsjlLGm^{8sdd`cjv0>
z*M<5L4}?wJh4}(=ihjLlPCXekr^4Xy@a60w6~p?3o{=V1{i+HlLj7vGG+HW#AlBx=
zeN(oR5m0>ceLyf!c6a%7hoep2l)%#RuvfX!EHAw(t#QR!+~ps@Wjn&Z0E20}fLOM+
z>sFUhw`Vm1TQhbiX6!#^gnA5bkA)0*9olU+r6X8}<SaZ|0}zz_(VVr(C`I}AT6+u|
z{@vs+4i2AIFK2@g1;8x;M6C!!@$LUHG8Uv)UX{pO@E-2c4bnw9;+0V-Tf|$xs(hKg
zlQvp=j8L!PwPZ8uDqhrQf@A_ma>Uzci`TYctk`FX7aO{ZcQ0@%M+>FF>frFGI&FG^
z(2$RM?J`lK3Q~2I=$Mrq4+a3Bme1HdYwYu!Kb_H$*hLsr!^09NB=r{kxB8db7k~7E
zV3k_X%J$(53`meDI6Q^~sHNeYKYV?(#5`b&GWos81&H*DCcA5^{V%zjaku;Ewh59;
z@D$EO2Mcx|S?+5=Ehu7X-P}NoCuI1jV2UGSmlCttI;2vYl17_;F_D^%mSG4ZSQrX)
ztPBe{!Tk#KvG%vSTc<-iKoRJvi9j$O-ey^dsOWZ(aE*V@Lr;PvjpO)%+yF#&A{Y&p
zG9$B00H}1B@-MK}ZlSL*GN$U;Cb$htOs8h>)=vi`Ejh;s>lA<iYMGdDMtr`rWfr6X
zYMSX`qjDS^z*RZ|&cejnP9UXW@X=M_OWz&e%7;d%-SD>CVs{UO@x)?niHd<RS`~t1
z4xU0Fyth0M?y&H{W^s552_=K+MR>USPI%MH*=7xFwwj7t7q#FvOLh&Mj;9ht(@l@2
z!iib=#{k0}_k+hoGfgIuxGFxvQt+4`L$eZC=t+8IY_<N&op*Mw28~dc;q9_vagSu^
z#_z<*+>Rz6AOpz)JOxA!<f?10pUws9uD^{tq}xISo4F&>1Dv9X_-l_QBd0*#*#HED
zaPtF~(n(D<1;oIt#z-+XN#s=gq8XTyfn)zFgXjO}Y?9?+g;@_>q(AHN<2wCW-anOC
z<H<BgfS@xW2_&w#2I-4B`|aPLo%RwC^gQ)TXO}PBy0G-t%GFi<(ZSva2YZbJeP4OM
zu77m$`wvcj-*|1z7<<nMoj1JaEwtC%H{l@8PSK{gyFosMO^|#7PvNlAK%G;ru3=qh
z$b}o%g+@gFf_+%Q=I+q{4aQL%Ih}^HsQ)T_(@>=(l&SbkVKS{`%78_CkJ~=~3Xs3`
z(D}Itae*+J^;q*|1xZQ!v!Y)~r&QRC6gl(?l|aMAI-vaw+G%*Jh@dsD2w(Vq;amD}
zwe_y>pT0HU>WB9a7@>Z{+izh+k~r)(B(+HBU3&^kNIr$9u;c12@%uy9-$J<$SRJsL
z$*QJ@sQMg9mB~f`9+l1iLSgfLx5BQ#t@e*=CLp3<;ZMhwG~KiFF{p)mZybdtyGICn
zEU=|L=Gl98Tw?dZ8xN}ww*q7Q*y@9`_#DnWQ`$#Ie@m0X(;hn~AgWv77Wk4LoYSME
zj(6&^u*GrqH<^#wsF3Zo<Uv2gX{wIj-5l4dN%HKh3J1^BG?;hVqU1zGvB0AP4XL9Z
zdW&fKrbs%greGv`MMke`%y41ESb8c(kEryB57+q^i%=JCa!J+X;M*IDQG#Sad<FSP
zeh!a@)*kL6{MEVOwwvdEdj6M*+n0>S=;HZYun~Tb|JrwV->+(n?OluGx!?|{dH><Q
zWB29teSJoA-{Sj^gW*TPuE&wq)yefp^kK(|ugH4G;DgAZ5g6RynVRk=warU&RA1cn
z!wcwD(2s9}c2Pqtw3{95%5<cNUP065x1b05wpn++!)Uq}1WQw?wlA=HwNqcNxm0)f
zY)@s~d9mue1w(_@3_(T#rbkhFV4~svCZ(A~&2#jHhGAE+<24|gGzNn&f@BqWKLTQF
z%#NGyS^A)??>lZZA76Yw7wo)w_EE6Y2zFLhimoTYuAApTZ;a=v&i@3%pZ)+xQPv~v
zMxY(_X?szhOpyji?rL?@U9Hd{1Tl6iRga2B$5N?XRHfJj_!w6-RP*d~!SLwl;c1#L
zD4JsuK&gs~V3`+7srUu>myr@>D5zseov_)!z-Z{ZX;K7gtlB3)r5D5n&q7t%cpj&3
z$#_*x9j<P{tE2y=X<l?V^Im7=IywcK6tToCiVHrsekHT`oUxpdsA_w%M=GoKCbK9@
z_WvkY-szuV6+}UD3CU$3Q6D`n5scJn$ZqNT2k>)~mQx*}0R`1y>f54z@*%cluTW!Y
za*4z695LCr$?20OH#G_0RIIoTzNxU2^hAaR)Jm2a#gLRB`44!s{|17aB9sf(-#qu}
zd%wJJ`v*ot+v0n<U<+=D79-g5IMTc#uZ;cd#KZkP_b;#S?|%^KHv;{r*3y$;D>iF2
zf~}SJ&4DMue%v?x4}$%Vn-1MQvfkA7@bIax2iFh3{-Ejg#S!c(uSeSM!q7*Jz|jqn
zsTp|cVQM0ef_oh1!}eFdlGoc`dk}fe2)u@~?|o9YYelr8g6J;#O%}d@z<*8<G?!*|
z;h!f|jR;U<eUWd((q1I=M0F5L-AIlh!3$*T9%2Yfc-K|5MD(a{A&8rihWHjnH2$Ed
z(gPdyRn+`YaZ?9b2v(kXU$Oq7-~?HOQ7{b9c7yBQ;8~Xa6IaCw|5wYf4ZmmhJQX}_
zcya$z2C}EMKDHIhko~!VV|{;OfNXdfuKFnlr6nPc6?q;iHn75G32e*aNS=YrW<hBq
zKzj*nlf`N(u$pX^$hIL1GMfdZjT+jkiXCE+hq=wf;zrn6$)a9)B^TXSBC@@UeK=ij
zVY*&>I+5*Ld;?j11y-NU!dC-U*{l6I0Iyyu8lG)f9L_V4+5Mrk;iqdA*^b3yICMv0
z=#Ijy-4?66!0NVH9`*u@BVukdvA9udk2!!$ksT;>9N4Jwvb$EI8w_N3efRgR)#S0b
lQSXQ9whacd)y)0Koqx$=aib~7?p{$h7|5*FPq9eV{4WFr<rn|}
literal 0
HcmV?d00001
diff --git a/Pystan/config/example_interval.py b/Pystan/config/example_interval.py
new file mode 100644
index 0000000..8aa35e0
--- /dev/null
+++ b/Pystan/config/example_interval.py
@@ -0,0 +1,4 @@
+from interval_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/Pystan/config/example_interval_eval_exp.py b/Pystan/config/example_interval_eval_exp.py
new file mode 100644
index 0000000..1203cab
--- /dev/null
+++ b/Pystan/config/example_interval_eval_exp.py
@@ -0,0 +1,32 @@
+from syntax import *
+from interval_analysis import eval_aexp, eval_bexp, abstract_env, Interval
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+# x - y * (x / y)
+test_aexp: ArithExpr = AEBop(Bop.ADD,x, AEUop(Uop.OPP,AEBop(Bop.MUL,y,AEBop(Bop.DIV,x,y))))
+
+# ! (x - y <= y * (x - x/y))
+test_bexp: BoolExpr = BENeg(BELeq(AEBop(Bop.ADD,x,AEUop(Uop.OPP,y)),test_aexp))
+
+def test(env: abstract_env) -> None:
+ res_a = eval_aexp(env,test_aexp)
+ res_b = eval_bexp(env,test_bexp)
+ print(f'In environment { {var: str(i) for (var,i) in env.items()} }')
+ print(f"{test_aexp} -> {res_a}")
+ print(f"{test_bexp} -> {res_b}")
+
+test({ 'x': Interval(20,20), 'y': Interval(2,2) })
+
+test({ 'x': Interval(10,20), 'y': Interval(1,2) })
+
+test({ 'x': Interval(-30,0), 'y': Interval(-10,0) })
+
+test({ 'x': Interval(-20,20), 'y': Interval(0,0) })
+
+test({ 'x': Interval(0,20), 'y': Interval(2,5) })
+
+test({ 'x': Interval(-10,20), 'y': Interval(-5,-2) })
+
+test({})
diff --git a/Pystan/config/example_interval_reduce.py b/Pystan/config/example_interval_reduce.py
new file mode 100644
index 0000000..2d7cdda
--- /dev/null
+++ b/Pystan/config/example_interval_reduce.py
@@ -0,0 +1,39 @@
+from syntax import *
+from interval_analysis import state, abstract_env, Interval, reduce_state
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+test_eq: BoolExpr = BEEq(x,y)
+
+test_neq: BoolExpr = BENeg(test_eq)
+
+test_leq: BoolExpr = BELeq(x,y)
+
+test_gt: BoolExpr = BENeg(test_leq)
+
+def env_str(env: abstract_env) -> str:
+ return '{ ' + ', '.join([ f'{var}: {i}' for (var,i) in env.items()]) + ' }'
+
+def state_str(env: state) -> str:
+ if env is None: return 'None'
+ return env_str(env)
+
+def test(env: abstract_env) -> None:
+ res_eq = reduce_state(env,test_eq)
+ res_neq = reduce_state(env,test_neq)
+ res_leq = reduce_state(env,test_leq)
+ res_gt = reduce_state(env,test_gt)
+ print(f'In environment { env_str(env) }')
+ print(f"{test_eq} -> {state_str(res_eq)}")
+ print(f"{test_neq} -> {state_str(res_neq)}")
+ print(f"{test_leq} -> {state_str(res_leq)}")
+ print(f"{test_gt} -> {state_str(res_gt)}")
+
+test({ 'x': Interval(0,5), 'y': Interval(-5,0) })
+
+test({ 'x': Interval(-5,5), 'y': Interval(3,7) })
+
+test({ 'x': Interval(0,5), 'y': Interval(-10,-5) })
+
+test({ 'x': Interval(0,0), 'y': Interval(0,4) })
diff --git a/Pystan/config/example_sign.py b/Pystan/config/example_sign.py
new file mode 100644
index 0000000..6aa6de3
--- /dev/null
+++ b/Pystan/config/example_sign.py
@@ -0,0 +1,4 @@
+from sign_analysis import analyze
+from example_opsem import factorial
+
+analyze(factorial)
diff --git a/Pystan/config/example_sign_eval_exp.py b/Pystan/config/example_sign_eval_exp.py
new file mode 100644
index 0000000..c8bdd99
--- /dev/null
+++ b/Pystan/config/example_sign_eval_exp.py
@@ -0,0 +1,28 @@
+from syntax import *
+from sign_analysis import eval_aexp, eval_bexp, abstract_env, sign
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+# y * (x - x / y)
+test_aexp: ArithExpr = AEBop(Bop.MUL,y,AEBop(Bop.ADD,x, AEUop(Uop.OPP,AEBop(Bop.DIV,x,y))))
+
+# ! (x - y <= y * (x - x/y))
+test_bexp: BoolExpr = BENeg(BELeq(AEBop(Bop.ADD,x,AEUop(Uop.OPP,y)),test_aexp))
+
+def test(env: abstract_env) -> None:
+ res_a = eval_aexp(env,test_aexp)
+ res_b = eval_bexp(env,test_bexp)
+ print(f'In environment { {var: str(sign) for (var,sign) in env.items()} }')
+ print(f"{test_aexp} -> {res_a}")
+ print(f"{test_bexp} -> {res_b}")
+
+test({ 'x': sign.SPOS, 'y': sign.SPOS })
+
+test({ 'x': sign.NEG, 'y': sign.NEG })
+
+test({ 'x': sign.INT, 'y': sign.Z })
+
+test({ 'x': sign.POS, 'y': sign.NZ })
+
+test({})
diff --git a/Pystan/config/example_sign_reduce.py b/Pystan/config/example_sign_reduce.py
new file mode 100644
index 0000000..17ed636
--- /dev/null
+++ b/Pystan/config/example_sign_reduce.py
@@ -0,0 +1,33 @@
+from syntax import *
+from sign_analysis import state, abstract_env, sign, reduce_state
+
+x: ArithExpr = AEVar("x")
+y: ArithExpr = AEVar("y")
+
+test_eq: BoolExpr = BEEq(x,y)
+
+test_neq: BoolExpr = BENeg(test_eq)
+
+test_leq: BoolExpr = BELeq(x,y)
+
+test_gt: BoolExpr = BENeg(test_leq)
+
+def test(env: abstract_env) -> None:
+ res_eq = reduce_state(env,test_eq)
+ res_neq = reduce_state(env,test_neq)
+ res_leq = reduce_state(env,test_leq)
+ res_gt = reduce_state(env,test_gt)
+ print(f'In environment { {var: str(sign) for (var,sign) in env.items()} }')
+ print(f"{test_eq} -> {res_eq}")
+ print(f"{test_neq} -> {res_neq}")
+ print(f"{test_leq} -> {res_leq}")
+ print(f"{test_gt} -> {res_gt}")
+
+test({ 'x': sign.POS, 'y': sign.NEG })
+
+test({ 'x': sign.NZ, 'y': sign.NEG })
+
+test({ 'x': sign.POS, 'y': sign.SNEG })
+
+test({ 'x': sign.Z, 'y': sign.POS })
+
diff --git a/Pystan/config/example_widen.py b/Pystan/config/example_widen.py
new file mode 100644
index 0000000..c9372be
--- /dev/null
+++ b/Pystan/config/example_widen.py
@@ -0,0 +1,61 @@
+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+from cfg import Cfg
+from example_opsem import factorial
+
+@dataclass
+class Number_step:
+ bound: int | None
+ def __str__(self):
+ if self.bound is None: return "+∞"
+ else: return str(self.bound)
+
+type S = Number_step | None
+
+class Analysis(Transfer[S]):
+ def bottom(self) -> S:
+ return None
+
+ def init_state(self) -> S:
+ return Number_step(0)
+
+ def join(self,s1:S,s2:S) -> S:
+ if s1 is None: return s2
+ if s2 is None: return s1
+ if s1.bound is None: return s1
+ if s2.bound is None: return s2
+ return Number_step(max(s1.bound, s2.bound))
+
+ def widen(self, s1:S, s2:S) -> S:
+ if s1 is None: return s2
+ if s2 is None: return s1
+ if s1.bound is None: return s1
+ if s2.bound is None: return s2
+ if s1.bound < s2.bound: return Number_step(None)
+ return s1
+
+ def included(self,s1: S,s2: S) -> bool:
+ if s1 is None: return True
+ if s2 is None: return False
+ if s2.bound is None: return True
+ if s1.bound is None: return False
+ return s1.bound <= s2.bound
+
+ def tr_skip(self,s: S) -> S:
+ if s is None: return None
+ if s.bound is None: return s
+ return Number_step(s.bound + 1)
+
+ def tr_set(self,s: S,v: str,e: ArithExpr) -> S:
+ return self.tr_skip(s)
+
+ def tr_test(self,s: S,c: BoolExpr) -> S:
+ return self.tr_skip(s)
+
+ def tr_err(self,s: S,e: Expr) -> S:
+ return self.tr_skip(s)
+
+res = fixpoint_iteration(Analysis(),Cfg(factorial))
+
+for (node, nb) in res.items():
+ print(f'{node} -> {nb}')
diff --git a/Pystan/config/interval_analysis.py b/Pystan/config/interval_analysis.py
new file mode 100644
index 0000000..9186efb
--- /dev/null
+++ b/Pystan/config/interval_analysis.py
@@ -0,0 +1,406 @@
+# pyright: strict
+
+"""
+implements a constant propagation analysis
+"""
+
+from dataclasses import dataclass
+from cfg import Cfg
+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+
+@dataclass
+class Interval:
+ """ potentially unbounded interval
+
+ None in either bound means that we don't have info.
+ Hence `Interval(None,None)` denotes all integers
+ """
+ lower_bound: int | None
+ upper_bound: int | None
+ def __str__(self):
+ if self.lower_bound is None:
+ l = "-∞"
+ else:
+ l = str(self.lower_bound)
+ if self.upper_bound is None:
+ u = "+∞"
+ else:
+ u = str(self.upper_bound)
+ return f"[{l}; {u}]"
+
+class Top:
+ def __str__(self): return "TOP"
+
+@dataclass
+class BTop:
+ """class used for the evaluation of boolean expressions
+
+ BTop(False) indicates that we don't know if the result is True or False, but
+ that the evaluation cannot lead to an error
+ BTop(True) indicates that we neither know the result nor whether an error can occur
+ """
+ has_error: bool
+ def __str__(self):
+ if self.has_error: return "TOP (maybe error)"
+ else: return "TOP (no error)"
+
+type abstract_env = dict[str, Interval]
+"""mapping from variables to abstract values.
+
+As with concrete environment, a variable not in the dictionary will
+lead to an error if we try to obtain its value
+"""
+
+type state = abstract_env | None
+"""abstract state is either an abstract env or bottom
+"""
+
+def interval_leq(i1: Interval, i2: Interval) -> bool:
+ if i2.lower_bound is None:
+ if i2.upper_bound is None:
+ return True
+ if i1.upper_bound is None:
+ return False
+ return i1.upper_bound <= i2.upper_bound
+ if i2.upper_bound is None:
+ if i1.lower_bound is None:
+ return False
+ return i1.lower_bound >= i2.lower_bound
+ if i1.lower_bound is None or i1.upper_bound is None:
+ return False
+ return i1.lower_bound >= i2.lower_bound and i1.upper_bound <= i2.upper_bound
+
+def interval_join(i1: Interval, i2: Interval) -> Interval:
+ if i1.lower_bound is None or i2.lower_bound is None:
+ l = None
+ else:
+ l = min(i1.lower_bound,i2.lower_bound)
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = max(i1.upper_bound,i2.upper_bound)
+ return Interval(l,u)
+
+def interval_meet(i1: Interval, i2: Interval) -> Interval | None:
+ if i1.lower_bound is None:
+ l = i2.lower_bound
+ elif i2.lower_bound is None:
+ l = i1.lower_bound
+ else:
+ l = max(i1.lower_bound,i2.lower_bound)
+ if i1.upper_bound is None:
+ u = i2.upper_bound
+ elif i2.upper_bound is None:
+ u = i1.upper_bound
+ else:
+ u = min(i1.upper_bound,i2.upper_bound)
+ if l is not None and u is not None and l > u: return None
+ return Interval(l,u)
+
+def interval_widen(i1: Interval, i2: Interval) -> Interval:
+ if i1.lower_bound is None or i2.lower_bound is None:
+ l = None
+ elif i1.lower_bound <= i2.lower_bound:
+ l = i1.lower_bound
+ else:
+ l = None
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ elif i1.upper_bound >= i2.upper_bound:
+ u = i1.upper_bound
+ else:
+ u = None
+ return Interval(l,u)
+
+def has_strict_positive_val(i: Interval) -> bool:
+ return i.upper_bound is None or i.upper_bound > 0
+
+def has_strict_negative_val(i: Interval) -> bool:
+ return i.lower_bound is None or i.lower_bound < 0
+
+def contains_zero(i: Interval) -> bool:
+ if i.lower_bound is None:
+ return i.upper_bound is None or i.upper_bound >= 0
+ if i.upper_bound is None:
+ return i.lower_bound <= 0
+ return i.lower_bound <= 0 and i.upper_bound >= 0
+
+def is_zero(i: Interval) -> bool:
+ return i.lower_bound == 0 and i.upper_bound == 0
+
+def interval_opp(i: Interval) -> Interval:
+ if i.lower_bound is None:
+ u = None
+ else:
+ u = -i.lower_bound
+ if i.upper_bound is None:
+ l = None
+ else:
+ l = -i.upper_bound
+ return Interval(l,u)
+
+def interval_add(i1: Interval, i2: Interval) -> Interval:
+ raise NotImplementedError
+
+def interval_mul_pos(i1: Interval, i2: Interval) -> Interval:
+ assert (i1.lower_bound is not None and i1.lower_bound >= 0)
+ assert (i2.lower_bound is not None and i2.lower_bound >= 0)
+ l = i1.lower_bound * i2.lower_bound
+ if i1.upper_bound is None or i2.upper_bound is None:
+ u = None
+ else:
+ u = i1.upper_bound * i2.upper_bound
+ return Interval(l,u)
+
+def interval_opt_join(i1: Interval | None, i2: Interval) -> Interval:
+ if i1 is None: return i2
+ return interval_join(i1,i2)
+
+def interval_mul(i1: Interval, i2: Interval) -> Interval:
+ i1_neg = interval_meet(i1,Interval(None,0))
+ i2_neg = interval_meet(i2,Interval(None,0))
+ i1_pos = interval_meet(i1,Interval(0,None))
+ i2_pos = interval_meet(i2,Interval(0,None))
+ if i1_neg is None or i2_pos is None:
+ res = None
+ else:
+ res = interval_opp(interval_mul_pos(interval_opp(i1_neg),i2_pos))
+ if i1_pos is not None and i2_neg is not None:
+ res1 = interval_opp(interval_mul_pos(i1_pos,interval_opp(i2_neg)))
+ res = interval_opt_join(res, res1)
+ if i1_neg is not None and i2_neg is not None:
+ res1 = interval_mul_pos(interval_opp(i1_neg),interval_opp(i2_neg))
+ res = interval_opt_join(res,res1)
+ if i1_pos is not None and i2_pos is not None:
+ res1 = interval_mul_pos(i1_pos, i2_pos)
+ res = interval_opt_join(res, res1)
+ # at least one of the 4 cases is not empty
+ assert res is not None
+ return res
+
+def interval_div(i1: Interval, i2: Interval) -> Interval | Top | None:
+ raise NotImplementedError
+
+def eval_aexp(env: abstract_env, e: ArithExpr) -> Interval | Top | None:
+ """evaluate an arithmetic expression in an abstract environment
+ returns None in case of error
+ """
+ match e:
+ case AECst(value): return Interval(value,value)
+ case AEVar(var):
+ if var in env: return env[var]
+ else: return None
+ case AEUop(uop,expr):
+ res = eval_aexp(env,expr)
+ if res is None or isinstance(res,Top): return res
+ if uop == Uop.OPP: return interval_opp(res)
+ return None
+ case AEBop(bop,left_expr,right_expr):
+ v1 = eval_aexp(env,left_expr)
+ v2 = eval_aexp(env,right_expr)
+ if v1 is None or v2 is None: return None
+ if isinstance(v1,Top) or isinstance(v2,Top):
+ return Top()
+ match bop:
+ case Bop.ADD: return interval_add(v1,v2)
+ case Bop.MUL: return interval_mul(v1,v2)
+ case Bop.DIV: return interval_div(v1,v2)
+ case _: pass
+
+def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
+ """abstract evaluation of a boolean expression"""
+ match e:
+ case BEPlain(aexpr):
+ res = eval_aexp(env, aexpr)
+ if res is None: return None
+ if isinstance(res,Top): return BTop(True)
+ if res.lower_bound == 0 and res.upper_bound == 0: return True
+ if not interval_leq(Interval(0,0), res): return False
+ return BTop(False)
+ case BEEq(left_expr,right_expr):
+ v1 = eval_aexp(env, left_expr)
+ v2 = eval_aexp(env, right_expr)
+ if v1 is None or v2 is None: return None
+ if isinstance(v1,Top) or isinstance(v2,Top): return BTop(True)
+ if v1.lower_bound is None or v2.lower_bound is None or v1.upper_bound is None or v2.upper_bound is None:
+ return BTop(False)
+ if v1.lower_bound > v2.upper_bound or v1.upper_bound < v2.lower_bound:
+ return False
+ if v1.lower_bound == v1.upper_bound and v2.lower_bound == v2.upper_bound and v1.lower_bound == v2.lower_bound:
+ return True
+ return BTop(False)
+ case BELeq(left_expr,right_expr):
+ v1 = eval_aexp(env, left_expr)
+ v2 = eval_aexp(env, right_expr)
+ if v1 is None or v2 is None: return None
+ if isinstance(v1,Top) or isinstance(v2,Top): return BTop(True)
+ if v1.upper_bound is None:
+ if v1.lower_bound is None:
+ return BTop(False)
+ if v2.upper_bound is None:
+ return BTop(False)
+ if v2.upper_bound < v1.lower_bound:
+ return False
+ return BTop(False)
+ if v2.lower_bound is None:
+ return BTop(False)
+ if v1.upper_bound <= v2.lower_bound:
+ return True
+ if v1.lower_bound is None:
+ return BTop(False)
+ if v2.upper_bound is None:
+ return BTop(False)
+ if v2.upper_bound < v1.lower_bound:
+ return False
+ return BTop(False)
+ case BENeg(expr):
+ v = eval_bexp(env,expr)
+ if v is None: return None
+ if isinstance(v,BTop): return v
+ return not v
+ case _: pass
+
+def reduce_eq(s:state, x:str, i: Interval) -> state:
+ raise NotImplementedError
+
+def reduce_neq(s:state, x: str, i: Interval) -> state:
+ raise NotImplementedError
+
+def reduce_leq(s:state,x:str,upper_bound: int) -> state:
+ raise NotImplementedError
+
+def reduce_geq(s: state, x: str, lower_bound: int) -> state:
+ raise NotImplementedError
+
+def reduce_state(s: state,c: BoolExpr) -> state:
+ if s is None: return s
+ match c:
+ case BEEq(AEVar(x), AEVar(y)):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top):
+ s = reduce_eq(s,y,vx)
+ if not isinstance(vy,Top):
+ s = reduce_eq(s,x,vy)
+ return s
+ case BEEq(AEVar(x), right_expr):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_eq(s,x,v)
+ case BEEq(left_expr, AEVar(y)):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_eq(s,y,v)
+ case BELeq(AEVar(x), AEVar(y)):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vy,Top) and vy.upper_bound is not None:
+ s = reduce_leq(s,x,vy.upper_bound)
+ if not isinstance(vx,Top) and vx.lower_bound is not None:
+ s = reduce_geq(s,y,vx.lower_bound)
+ return s
+ case BELeq(AEVar(x),right_expr):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.upper_bound is None: return s
+ return reduce_leq(s,x,v.upper_bound)
+ case BELeq(left_expr,AEVar(y)):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.lower_bound is None: return s
+ return reduce_geq(s,y,v.lower_bound)
+ case BENeg(BEEq(AEVar(x), AEVar(y))):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top):
+ s = reduce_neq(s,y,vx)
+ if not isinstance(vy,Top):
+ s = reduce_neq(s,x,vy)
+ return s
+ case BENeg(BEEq(AEVar(x), right_expr)):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_neq(s,x,v)
+ case BENeg(BEEq(left_expr, AEVar(y))):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ return reduce_neq(s,y,v)
+ case BENeg(BELeq(AEVar(x), AEVar(y))):
+ vx = eval_aexp(s,AEVar(x))
+ vy = eval_aexp(s,AEVar(y))
+ if vx is None or vy is None: return None
+ if not isinstance(vx,Top) and vx.upper_bound is not None:
+ s = reduce_leq(s,y,vx.upper_bound - 1)
+ if not isinstance(vy,Top) and vy.lower_bound is not None:
+ s = reduce_geq(s,x,vy.lower_bound + 1)
+ return s
+ case BENeg(BELeq(AEVar(x),right_expr)):
+ v = eval_aexp(s,right_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.lower_bound is None: return s
+ return reduce_geq(s,x,v.lower_bound + 1)
+ case BENeg(BELeq(left_expr,AEVar(y))):
+ v = eval_aexp(s,left_expr)
+ if v is None: return None
+ if isinstance(v,Top) or v.upper_bound is None: return s
+ return reduce_leq(s,y,v.upper_bound - 1)
+ case _: return s
+
+class Interval_analysis(Transfer[state]):
+ variables: frozenset[str]
+ def __init__(self,instr: Instr):
+ self.variables = variables_of_instr(instr)
+ def bottom(self) -> state:
+ return None
+ def init_state(self) -> state:
+ return dict.fromkeys(self.variables, Interval(None,None))
+ def join(self,s1:state,s2:state) -> state:
+ if s1 is None: return s2
+ if s2 is None: return s1
+ res: abstract_env = {}
+ for var in self.variables:
+ v1 = s1[var]
+ v2 = s2[var]
+ v = interval_join(v1,v2)
+ res[var] = v
+ return res
+
+ def widen(self, s1:state, s2:state) -> state:
+ raise NotImplementedError
+
+ def included(self,s1: state,s2: state) -> bool:
+ if s1 is None: return True
+ if s2 is None: return False
+ for var in self.variables:
+ if not interval_leq(s1[var],s2[var]): return False
+ return True
+
+ def tr_skip(self,s: state) -> state:
+ return s
+
+ def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
+ raise NotImplementedError
+
+ def tr_test(self,s: state,c: BoolExpr) -> state:
+ raise NotImplementedError
+
+ def tr_err(self,s: state,e: Expr) -> state:
+ raise NotImplementedError
+
+def analyze(i: Instr) -> None:
+ cfg = Cfg(i)
+ res = fixpoint_iteration(Interval_analysis(i), cfg)
+ for node in cfg.g.nodes:
+ print(f"State at {node}:")
+ s = res[node]
+ if s is not None:
+ for (v, s) in s.items():
+ print(f" {v}: {s}")
diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py
new file mode 100644
index 0000000..61bd064
--- /dev/null
+++ b/Pystan/config/sign_analysis.py
@@ -0,0 +1,338 @@
+# pyright: strict
+"""
+implements a sign analysis
+"""
+from enum import Enum
+from dataclasses import dataclass
+from cfg import Cfg
+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+
+class sign(Enum):
+ SNEG = auto()
+ SPOS = auto()
+ Z = auto()
+ NEG = auto()
+ POS = auto()
+ NZ = auto()
+ INT = auto()
+
+class Top:
+ def __str__(self): return "TOP"
+
+@dataclass
+class BTop:
+ """class used for the evaluation of boolean expressions
+
+ BTop(False) indicates that we don't know if the result is True or False, but
+ that the evaluation cannot lead to an error
+ BTop(True) indicates that we neither know the result nor whether an error can occur
+ """
+ has_error: bool
+ def __str__(self):
+ if self.has_error: return "TOP (maybe error)"
+ else: return "TOP (no error)"
+
+type abstract_env = dict[str, sign]
+"""mapping from variables to abstract values.
+
+As with concrete environment, a variable not in the dictionary will
+lead to an error if we try to obtain its value
+"""
+type state = abstract_env | None
+"""abstract state is either an abstract env or bottom
+"""
+
+def sign_leq(v1: sign, v2:sign) -> bool:
+ """order relation on the sign lattice"""
+ if v1 == v2: return True
+ match v1,v2:
+ case _, sign.INT: return True
+ case sign.INT, _: return False
+ case sign.SNEG,(sign.NEG | sign.NZ): return True
+ case sign.SPOS,(sign.POS | sign.NZ): return True
+ case sign.Z,(sign.POS | sign.NEG): return True
+ case sign.NEG,sign.NZ: return True
+ case sign.POS,sign.NZ: return True
+ case _: return False
+
+def sign_join(v1: sign, v2:sign) -> sign:
+ """computes least upper bound"""
+ match v1,v2:
+ case sign.INT, _: return sign.INT
+ case _, sign.INT: return sign.INT
+ case sign.NZ, (sign.NZ | sign.SPOS | sign.SNEG): return sign.NZ
+ case sign.NZ,_: return sign.INT
+ case sign.NEG, (sign.NEG | sign.SNEG | sign.Z): return sign.NEG
+ case sign.NEG, _: return sign.INT
+ case sign.POS, (sign.POS | sign.SPOS | sign.Z): return sign.POS
+ case sign.POS,_: return sign.INT
+ case sign.SNEG, sign.SNEG: return sign.SNEG
+ case sign.SNEG, (sign.Z | sign.NEG): return sign.NEG
+ case sign.SNEG, (sign.SPOS | sign.NZ): return sign.NZ
+ case sign.SNEG, _: return sign.INT
+ case sign.SPOS, sign.SPOS: return sign.SPOS
+ case sign.SPOS, (sign.POS | sign.Z): return sign.POS
+ case sign.SPOS, (sign.SNEG | sign.NZ): return sign.NZ
+ case sign.SPOS, _: return sign.INT
+ case sign.Z, sign.SNEG: return sign.NEG
+ case sign.Z, sign.SPOS: return sign.POS
+ case sign.Z, sign.NZ: return sign.INT
+ case sign.Z, _: return v2
+
+def sign_meet(s1: sign, s2:sign) -> sign | None:
+ """computes greatest lower bound. Can be None (i.e. bottom)"""
+ match s1,s2:
+ case sign.INT, _: return s2
+ case _, sign.INT: return s1
+ case sign.SNEG, (sign.NEG | sign.NZ | sign.SNEG): return s1
+ case (sign.NEG | sign.NZ | sign.SNEG), sign.SNEG: return s2
+ case sign.SNEG, _: return None
+ case _, sign.SNEG: return None
+ case sign.SPOS, (sign.POS | sign.NZ | sign.SPOS): return s1
+ case (sign.POS | sign.NZ | sign.SPOS), sign.SPOS: return s2
+ case sign.SPOS, _: return None
+ case _, sign.SPOS: return None
+ case sign.Z, (sign.NEG | sign.POS): return s1
+ case (sign.NEG | sign.POS), sign.Z: return s2
+ case sign.Z, sign.Z: return s1
+ case sign.Z, _: return None
+ case _, sign.Z: return None
+ case sign.NEG, sign.NEG: return s1
+ case sign.POS, sign.POS: return s1
+ case sign.NEG, sign.POS: return sign.Z
+ case sign.POS, sign.NEG: return sign.Z
+ case sign.NZ, sign.NEG: return sign.SNEG
+ case sign.NEG, sign.NZ: return sign.SNEG
+ case sign.NZ, sign.POS: return sign.SPOS
+ case sign.POS, sign.NZ: return sign.SPOS
+ case sign.NZ, sign.NZ: return sign.NZ
+
+def sign_opp(s:sign) -> sign:
+ """unary minus"""
+ match s:
+ case sign.SNEG: return sign.SPOS
+ case sign.SPOS: return sign.SNEG
+ case sign.POS: return sign.NEG
+ case sign.NEG: return sign.POS
+ case _: return s
+
+def sign_add(s1:sign,s2:sign) -> sign:
+ """addition"""
+ match (s1,s2):
+ case sign.INT,_: return sign.INT
+ case _,sign.INT: return sign.INT
+ case sign.Z,_: return s2
+ case _,sign.Z: return s1
+ case sign.SNEG, (sign.SNEG | sign.NEG): return sign.SNEG
+ case (sign.SNEG | sign.NEG), sign.SNEG: return sign.SNEG
+ case sign.NEG, sign.NEG: return sign.NEG
+ case sign.SPOS, (sign.SPOS | sign.POS): return sign.SPOS
+ case (sign.SPOS | sign.POS), sign.SPOS: return sign.SPOS
+ case sign.POS, sign.POS: return sign.POS
+ case _: return sign.INT
+
+def sign_mul(s1: sign, s2: sign) -> sign:
+ """multiplication"""
+ match s1,s2:
+ case sign.INT,_: return sign.INT
+ case _,sign.INT: return sign.INT
+ case sign.Z,_: return sign.Z
+ case _,sign.Z: return sign.Z
+ case sign.SPOS, _: return s2
+ case _, sign.SPOS: return s1
+ case sign.SNEG, _: return sign_opp(s2)
+ case _,sign.SNEG: return sign_opp(s1)
+ case sign.NZ, _: return sign.INT
+ case _, sign.NZ: return sign.INT
+ case sign.NEG, sign.NEG: return sign.POS
+ case sign.NEG, sign.POS: return sign.NEG
+ case sign.POS, sign.NEG: return sign.NEG
+ case sign.POS, sign.POS: return sign.POS
+
+def sign_div(s1: sign, s2: sign) -> sign | Top | None:
+ """division: can lead to errors even if operands are plain sign"""
+ match s1, s2:
+ case _,sign.Z: return None
+ case _,sign.INT: return Top()
+ case _,sign.POS: return Top()
+ case _,sign.NEG: return Top()
+ case sign.Z,_: return sign.Z
+ case sign.INT,_: return sign.INT
+ case sign.NZ,_: return sign.INT
+ case _,sign.NZ: return sign.INT
+ case (sign.POS | sign.SPOS), sign.SPOS: return sign.POS
+ case (sign.NEG | sign.SNEG), sign.SPOS: return sign.NEG
+ case (sign.POS | sign.SPOS), sign.SNEG: return sign.NEG
+ case (sign.NEG | sign.SNEG), sign.SNEG: return sign.POS
+
+def eval_aexp(env: abstract_env, e: ArithExpr) -> sign | Top | None:
+ """evaluate an arithmetic expression in an abstract environment
+ returns None in case of error
+ """
+ match e:
+ case AECst(value):
+ raise NotImplementedError
+ case AEVar(var):
+ raise NotImplementedError
+ case AEUop(uop,expr):
+ raise NotImplementedError
+ case AEBop(bop,left_expr,right_expr):
+ raise NotImplementedError
+ case _: pass
+
+def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
+ """abstract evaluation of a boolean expression"""
+ match e:
+ case BEPlain(aexpr):
+ raise NotImplementedError
+ case BEEq(left_expr,right_expr):
+ raise NotImplementedError
+ case BELeq(left_expr,right_expr):
+ raise NotImplementedError
+ case BENeg(expr):
+ raise NotImplementedError
+ case _: pass
+
+def reduce_eq_sign(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x == expr"""
+ if s is None: return None
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ res = sign_meet(s[x],v)
+ if res is None: return None
+ return s | { x: res }
+
+def reduce_neq_sign(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x != expr"""
+ if s is None: return None
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ match s[x],v:
+ case sign.POS, sign.Z: return s | { x: sign.SPOS }
+ case sign.NEG, sign.Z: return s | { x: sign.SNEG }
+ case sign.INT, sign.Z: return s | { x: sign.NZ }
+ case _: return s
+
+def reduce_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x <= expr"""
+ if s is None: return None
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ upper = sign.INT
+ match v:
+ case sign.NEG | sign.SNEG:
+ upper = v
+ case sign.Z:
+ upper = sign.NEG
+ case _: pass
+ res = sign_meet(s[x],upper)
+ if res is None: return None
+ return s | { x: res }
+
+def reduce_strict_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x < expr"""
+ if s is None: return None
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ match v:
+ case sign.NEG | sign.SNEG | sign.Z:
+ upper = sign.SNEG
+ case _:
+ upper = sign.INT
+ res = sign_meet(s[x],upper)
+ if res is None: return None
+ return s | { x: res }
+
+def reduce_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x >= expr"""
+ if s is None: return None
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ lower = sign.INT
+ match v:
+ case sign.POS | sign.SPOS:
+ lower = v
+ case sign.Z:
+ lower = sign.POS
+ case _: pass
+ res = sign_meet(s[x],lower)
+ if res is None: return None
+ return s | { x: res }
+
+def reduce_strict_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+ """reduce the value associated to x in s under the hypothesis that x > expr"""
+ if s is None: return s
+ v = eval_aexp(s,expr)
+ if v is None: return None
+ if isinstance(v,Top): return s
+ match v:
+ case sign.POS | sign.SPOS | sign.Z:
+ lower = sign.SPOS
+ case _:
+ lower = sign.INT
+ res = sign_meet(s[x],lower)
+ if res is None: return None
+ return s | { x: res }
+
+def reduce_state(s: state,c: BoolExpr) -> state:
+ if s is None: return s
+ match c:
+ # To be completed (see course's slides)
+ case _: return s
+
+class Sign_interp(Transfer[state]):
+ variables: frozenset[str]
+ def __init__(self,instr: Instr):
+ self.variables = variables_of_instr(instr)
+ def bottom(self) -> state:
+ return None
+ def init_state(self) -> state:
+ return dict.fromkeys(self.variables, sign.INT)
+ def join(self,s1:state,s2:state) -> state:
+ if s1 is None: return s2
+ if s2 is None: return s1
+ res: abstract_env = {}
+ for var in self.variables:
+ v1 = s1[var]
+ v2 = s2[var]
+ res[var] = sign_join(v1,v2)
+ return res
+
+ def included(self,s1: state,s2: state) -> bool:
+ if s1 is None: return True
+ if s2 is None: return False
+ for var in self.variables:
+ if not sign_leq(s1[var], s2[var]): return False
+ return True
+
+ def tr_skip(self,s: state) -> state:
+ return s
+
+ def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
+ raise NotImplementedError
+
+ def tr_test(self,s: state,c: BoolExpr) -> state:
+ raise NotImplementedError
+
+ def tr_err(self,s: state,e: Expr) -> state:
+ if s is None: return s
+ if isinstance(e,ArithExpr):
+ raise NotImplementedError
+ if isinstance(e,BoolExpr):
+ raise NotImplementedError
+
+def analyze(i: Instr) -> None:
+ cfg = Cfg(i)
+ res = fixpoint_iteration(Sign_interp(i), cfg)
+ for node in cfg.g.nodes:
+ print(f"State at {node}:")
+ s = res[node]
+ if s is not None:
+ for (v, s) in s.items():
+ print(f" {v}: {s}")
--
GitLab