From 6462adf5d290f68e8af0b914ea33cf46109aa206 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 26 Mar 2021 11:22:38 -0400 Subject: [PATCH] Implement global_lvalue and global_initializer in Python bindings This checks off the first two bullet points of #1153. The third bullet point, related to `llvm_alloc_global`, is left as future work. --- saw-remote-api/python/saw/llvm.py | 28 +++++++++++++ .../tests/saw/test-files/llvm_global.bc | Bin 0 -> 2472 bytes .../python/tests/saw/test-files/llvm_global.c | 5 +++ .../python/tests/saw/test_llvm_global.py | 38 ++++++++++++++++++ 4 files changed, 71 insertions(+) create mode 100644 saw-remote-api/python/tests/saw/test-files/llvm_global.bc create mode 100644 saw-remote-api/python/tests/saw/test-files/llvm_global.c create mode 100644 saw-remote-api/python/tests/saw/test_llvm_global.py diff --git a/saw-remote-api/python/saw/llvm.py b/saw-remote-api/python/saw/llvm.py index 169aae8e68..bba390e90a 100644 --- a/saw-remote-api/python/saw/llvm.py +++ b/saw-remote-api/python/saw/llvm.py @@ -153,6 +153,24 @@ def to_json(self) -> Any: return {'setup value': 'field', 'base': self.base.to_json(), 'field': self.field_name} +class GlobalInitializerVal(SetupVal): + name : str + + def __init__(self, name : str) -> None: + self.name = name + + def to_json(self) -> Any: + return {'setup value': 'global initializer', 'name': self.name} + +class GlobalLValueVal(SetupVal): + name : str + + def __init__(self, name : str) -> None: + self.name = name + + def to_json(self) -> Any: + return {'setup value': 'global lvalue', 'name': self.name} + name_regexp = re.compile('^(?P.*[^0-9])?(?P[0-9]+)?$') def next_name(x : str) -> str: @@ -458,6 +476,16 @@ def field(base : SetupVal, field_name : str) -> 'FieldVal': """Returns a ``FieldVal`` using the field ``field_name`` of the struct ``base``.""" return FieldVal(base, field_name) +# It's tempting to name this `global` to mirror SAWScript's `llvm_global`, +# but that would clash with the Python keyword `global`. +def global_lvalue(name: str) -> 'GlobalLValueVal': + """Returns a ``GlobalLValueVal`` representing a pointer to the named global ``name``.""" + return GlobalLValueVal(name) + +def global_initializer(name: str) -> 'GlobalInitializerVal': + """Returns a ``GlobalInitializerVal`` representing the value of the initializer of a named global ``name``.""" + return GlobalInitializerVal(name) + def struct(*fields : SetupVal) -> StructVal: """Returns a ``StructVal`` with fields ``fields``.""" return StructVal(list(fields)) diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_global.bc b/saw-remote-api/python/tests/saw/test-files/llvm_global.bc new file mode 100644 index 0000000000000000000000000000000000000000..8b27768e00eb6f4ad6c426e82aebb5d82617154d GIT binary patch literal 2472 zcmaJ@eQaA-6~8af@pV(@+38H{D9^9YO zdH#s)xCPmD*6V>mZdW!>><@?ak0Sm_X;l@NP!gxbL}tpWstO^h5+%(Fw3S5*Dq<3x z>uePW#I?@-I_I8yK7Qx=b;~n%zhpwF8X+{Gm-fE&>aT~s_K&My-`=0-Wnj;$N9aHm zLffmX2nMth2qzoQbrm&7v_^aTd1g|-uUc0xXudy?(0`?>`~3Fq<3_uwO=tdUjoqGh ztMk^zo*g7(>^fg{yr{cu66F`t;%^zdebRiub|Bkwdiu30^b%f`4_rV&I@zZsz)!Pqdr|LH%WF)G?-V?}*B z5W^E$5;WtuLQebGi5Q8iIB3H`9~*SzQ*M|OM~=j@IPPOZ3F7b(HIKunWaXDU!U7`} zt(HwIKcBQLOx51E^0$(fWrd$hT7Zi}IvmN7Aku}hMD-ES8H9 z9$^^?8&mvEP&LIb&+w~LmboPV?07oj#!(*|u@S1!$DXp0K%PXi#BrU3MI3iw#GyIM z-KpAJvz8KQqZ(?Lt^9q)@=S>?8Y7NA68GVlkB#eaKq0{#o}s3~rCY~Wto+LVJDwxq zHXN-4=R4p+j7mJ`B;m0x89FzLhpGA2EdC#so@LqM`5nyHf0Fnl&yM#~sQX!SZ zmz0`&i`s{I41HO|QH0|X4(4%4#G}X%RB@m(r<+>>kX!|a^El$dqgf7mx?I$5CNO|7 zAmZ4f_E7@IjX1J(u)@7!#K8o9$)Ky-;X0c!)iDRV&DUOi`+I-?!HsQ+8@nQI7t*s5 ztqO!RjC8T4ib09W3c4y0?RDr(kvfEmu#aKOF64~$b-mflw*4>O)W~x>SG%dZ?n2i# z;9Uma--5AKm*D5u_#qS1nU>oo3z_Z&-~)$p0sSU2JT!7o5?rgk8=?$o;D@B@idd?l z#C8_t&J5dGie;cMPU-N3o2XDBDjSIrRV4MLI_^Q1Tayfa$*^AL%6(j`ao%zl%Fk+< z^9V!Io6ZkX&PBQXD%zpp=e=|(fqa>)N!cb-k37bhcPwGE>+3*M%{?f;7WVv;hVNK*7fES|8 zvN9{obqTki>XO3BDxlo*Cq@`D_qR>Uhu=#%OMQDkbp$XM!?9d{?~|;7MnL$su;AhE zTP=5IE#GD6+flMw${y`2Z=~8v1?RNf2?6>_P$OlCP~B zxd$`cy*}=-)Hr*qOW0W3wX|lr3kJCBoztn#tEq;`LR&^|FBLkj&$br};A2P0eKi1Y zkb(mcz@w!84>!37is9iZz}aw5GTajlf9vD?Ms8i=VEK4e`^QyoqmO$k$!p7%*R9M{ zEcd){`}c)5NY-?rc}YH8k`Jfl!{GIz{ADyDBIE%~1qHV#r}g#Qf_Asqn9Q6z_fb#Y zXgl7~V(2qgTrdLG7Wl1$HLwwk2>6}PK149{^qbZ1jj(E zGHV(d9`S|-M?C%$V#FH^4UhT77U_BTH60uu825+ATg2F~Kim`b1c$_LZb|fb2gXl` zNBl!$pY22keV*X4&~V(_sGE__AY-G>)p7=zVb#*`a)$<0?=&JL-8M;!5CdZma?!VC z&Q)#HA&Hey|ubd1WY5YRy{f2$T zvwAJcQhh&#`i7?fZLfjk9XA zAHdwOLBVeLxQ}~6b$tYWQA2U5<6_GB9uyDTnNM{aTV6+D<8DIIaj=7J}$&%SLKf}0OaFEJ=OQWzbpn!-F zo!B|!o=N6i4c(*73v&Bl+`(S3QF;2!LW$bf3q<#h0?|fC%1hG)G#wDNvjM0Uh|1FT z8K2InJZ+Ts??k^n(B2B`**VIu?0;(A>tGwz3%2>FWNc^)X0bNMF~`9sb+Bn<*gqa? NI^iGx57<-Le*u|I9#a4S literal 0 HcmV?d00001 diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_global.c b/saw-remote-api/python/tests/saw/test-files/llvm_global.c new file mode 100644 index 0000000000..d58d7e324c --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/llvm_global.c @@ -0,0 +1,5 @@ +const int x = 0; + +int f() { + return x; +} diff --git a/saw-remote-api/python/tests/saw/test_llvm_global.py b/saw-remote-api/python/tests/saw/test_llvm_global.py new file mode 100644 index 0000000000..b2b58ee181 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_llvm_global.py @@ -0,0 +1,38 @@ +from pathlib import Path +import unittest +from saw import * +from saw.llvm import Contract, global_lvalue, global_initializer +import saw.llvm_types as ty + + +class FContract(Contract): + def specification(self): + x_init = global_initializer("x") + self.points_to(global_lvalue("x"), x_init) + + self.execute_func() + + self.returns(x_init) + + +class LLVMGlobalTest(unittest.TestCase): + + @classmethod + def setUpClass(self): + connect(reset_server=True) + + @classmethod + def tearDownClass(self): + disconnect() + + def test_llvm_global(self): + if __name__ == "__main__": view(LogResults()) + bcname = str(Path('tests','saw','test-files', 'llvm_global.bc')) + mod = llvm_load_module(bcname) + + result = llvm_verify(mod, 'f', FContract()) + self.assertIs(result.is_success(), True) + + +if __name__ == "__main__": + unittest.main()