BTC Language

	* Tests for symbolic execution

tests/language/bitcoin/symbolic/testing_scenarii.py

+"""Testing scenarii, i.e. hardcoded known script to their expected transformation."""
+from collections import namedtuple
+from symbolic_execution.language.bitcoin.symbolic_interpreter import Satifiability
+
+
+TestScenario = namedtuple(
+    "TestScenario", "execution_status hex_script"
+)
+
+TESTING_SCENARII = [
+    TestScenario(Satifiability.UNSATISFIABLE, "6382012088a820be087f56dfd0645993c60f742a32dcd733c75db11a946692500a6b07f65503388876a9148230631bc6978af49e056f58ba57485203df81706704e01d1560b17576a914166ddfe42c7effda275da84e1eda8583cc8794f96888ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "632103d619512240e2da7360e0ba988d222824a8384f7d43f07ceca01825add8802a3d6754b275210205bfac414d5b0078691c01627b30bb3ea3eafdc3dd45f9634a2eb5a0eccd38fd68ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "632102fb8af52ae49c7ff02c04d5474a09fc35bef47080a9f9f5614b14a7e81c96750767029000b275210234405f5183510dfaef4281619e0e0e8d54a169de87c3a9429e6815262ed644c168ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "a9144b1fec264ddee03172e6a0d0e99c9f7b75fd3013876321025990676edd76a365a067a708bb3b25334472846395460a58038a90f86c58a95c67029000b275210393ef9cffe8ffd90393ca96c277c89858f1f7d65aad75df6ed1a88d62ce5da5ff68ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "63a914bb408296de2420403aa79eb61426bb588a08691f8876a91431b31321831520e346b069feebe6e9cf3dd7239c670400925e5ab17576a9140d22433293fe9652ea00d21c5061697aef5ddb296888ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "632102ed03e275914c2c9012623815d82536c3cd0f236800a909e3be35144b776ad43767030ce707b17521029f93a84f6a6fc93b479fc845eb120d0d94188f9ef4fdfcfac03d8f45083c79da68ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "8201208763a914a9ddc31c3aa662dd3df25cfaacf32626bcb9b310882103dddd27e12856ab9f506c18694bc3c4b3419ba266cc4e401fb19123eaa32856ea67750311a409b1752102e90d0b6a7fa8c21630535a77ba0dcaec9a321fe825a401633e70cdd33ca369d268ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "a9144fa22d2b4eed18e026d4a716ef432224b4dfc81b876321038f21a7d24de9bda130b0d85c045e5dffccc0256dea567771f5ea4223ffb05d45670341bd0ab17521021a535dc1ecf9428f2b42f4448e706a80a0b215cdb4cfb904da41db616654aa7a68ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "a820b1a01a9c34ddc93c48e50d55073354fdfa6cbf13db97d9c1dfd98e994b7c492c876321024e8768b37746b1c65fdaaaee241b2f6a6b4f742d637249d1973a14b25a7ae96b6752b2752103e5f85f417a2cb89f0bfc4338eba791bc9ecbb7e1fd0038b1b0ef2e4359ee412268ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "a8205a917fe0e9a08004ea16bd682d656f8780b33af30c1e6d1b483652cecbb9d2908763210219b65599338687c784f5b78a23cac164a9094e94af6ec49532132da22d74e4226703931b06b1752102cff5fe1dae742d57cf2be42ae607f28ae0e4837019ca4b8b1bcdc96bcf4af9ee68ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "a97614b6a9c8c230722b7c748331a8b450f05566dc7d0f87630120b26d41049a797cd64043177214982114420e9e88a1bda92693f35de6934109b015b1c4ecb18570a29dc749e489377b4a6414d01af464773ed5e72abe95c812143eff7a3467148ef113ab29409765b689baab8f1a1fd3e966825887640499ad4658b17568410484ccd0f7c843d9738114e8e59cb057d2cb505892f6bdec8100d404fe33826f9f68300593395478fe13fe39d610d84c51d19e451275d86af3b7c2a3a003c4256468ac"),
+    TestScenario(Satifiability.UNSATISFIABLE, "63a820254e38932fdb9fc27f82aac2a5cc6d789664832383e3cf3298f8c120812712db882102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee675ab2752102661f72301363d25bda5e083342747032bc2a00ac58d74509d902f87a8f086bee68ac"),
+    TestScenario(Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"),
+    TestScenario(Satifiability.SATISFIABLE, "210246414b45204b45592046414b45204b45592046414b45204b45592046414b45206eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75ab6eac75abac91"),
+    TestScenario(Satifiability.SATISFIABLE, "64410408e496fc785089e54dfeb5d1c0ba06f99bee96951e1f9f4ac74b8118b3964cb1f38369f9c972c11ab4b6427f0b2355d0d116269f4043a44332e3ecec5d321d7641046fe513c87278d706338fe95241c183722204483fb19aed9abf2c3259755913b0988ab8385bf615d777d934d7109e9a064a6ca9de0f36f53348c9d760acfc2e0b410421ea36180cc830d85136a2a8c31020d30403f9bf3f0d89918f6f1a68adcb6aa44a354048734132250ce66ecaf55d8ce75140cd175e4a086f17f1b79ef425445f4104f5f5edaed4464297be1b612af7115ec11f40c510946491ab19aeaca4aec226620cd601ffa15cf2a8c7117cc4aba830e9f1a567fc9ab9cf5bd9024f25b67bf4ba4104cd2d1c08987da5f5c9815e675ccc428681632c70c364183bd438f8ebaed029e7e34a9a8ae661cadc9ac34871e2b478ec2a2ce0f267ef7234e949f990851dd4844104d83c59cef19de270175442a4b6517cb293bd401b55997053987bdb0f17e128e13830a4a4e67983c48f9624e86903afdd3206878b2c01ca2c715c618380ea50ed410454f272658d005fcbdf6bada5b161085ededf384ee6a431cded391487767a9e6a8f219b6203943b60acc88cc3b3688f4b1ea06f5a8dbd12f5f3db76a7b80e842f41042ec20548ca134276341806afe0aa5b3f9fb56b5b9d3340b0226719584396044bba2ab0e98af0d3f3b157a667609319296f25b92ab9953607ea6437bb00b9332e4104b17318e61cf59d37a61e8c0c317a2e173a56af5ce64bec421613100e04b689d7099e08231f73fc3b77aa677772fca9daa6147e0014885ddbfd6b092f3c81b24f4104ef03dced2196fece4667d762fd19ac565bc8dcfda40d8f8a3f7c6b6626fe2cc90039dd6af4862f559ef48ab567d8f7c8e7912484b5939903b904654a7680603e41047552bcf8182b037a60eab0137793b39a5ef86c0f172b6a59e096629197944b0abcdc14e7e0bdb83fb57cc31080c55f0fd968d63494d7e2814bc5d7477a7bfe1841041a944fb54d5e9ecddb67f88c64611fe49ac996e204b5df5383b1b43bd7b581ba66f683517481981749849fb93d63d362b701e3c1353e7b0103672077d105195e4104fb1322874b4b0ba454a3c73b08a615bab48370cd2239b693e322e955ac297e86b51ee33f7c4da4cd55f2a13bac5eaa2010953756d2b3ab073ead4c4f0e51b62441042f1eafd03e769be35b7db0044d352363722d152447007386a9ae983197d358604ec8b5f9afa02517fd1d5a9c11148b5f959487067c13c604d15072e68ad296864104b2aec0edd4c5ca08f50bbe9d66954dd5218cd5f4cde6d87cb7c44cb4c41f1faeb70df4532eb88655c93a348b235b3f623ff6028c333d64965fea830d953f755e4104411691845b47eae100fb853b57f99a846ce1dc4dd09be701ef800f8c66b3dcd0bbf0cff20c619db33a590905ee170cedc7fdf1beaa3cf677d5d66416130b0fa841044c17ca58e9eb5769644ef3643c4db4707a16d89f3be5b023933bd914dadd9f6ba8eeedfc7dcb41b23e68c81c633dd77631217ecbf9213f62b319b2aa52692ec3410482a6917e1a9a5141f21b2c5e6bb79b1d00af43ce6c6cd223e4d3146d03a7d73eff12b5f7041d013fe7be806b4a4adb4bcfd34c8b693d01050d397abb70ea6c1e410473a7c78f9ff430f2da389d8c6c40563dc992177aa1466f61c6d0764404475398201fe65bc82eed9ee141d1460b7e9735471c19389cb957bc47502fcc4cb0aaba4104fe0667649e22b3241d2960e654c75635605723cf4e3fcf3940ddc55d6180d098cab35d24df3ccbba83443ab5308efd434247745e69d6b63c4edd5feb5d390de364ae"),
+    TestScenario(Satifiability.SATISFIABLE, "2102cf6397ab627bf61f94f594b0650f72b1efdd0278deed0e6a11d62c08df65ffa2ac7c2102a7783ab0b0b05fc022c1cb0d6cbf31bc83570df40fcd5b6f96141c0d14dc97c5ac937c2103243167b9773d537be3fe118d1c4f17c35d5abdd1c1f6f501b7aa006b24eab71eac937c766302e803b26968937c766302d007b26968935387"),
+    TestScenario(Satifiability.UNSATISFIABLE, "63140bdc9d2d256b3ee9daae347be6f4dc835a467ffe2102259b57015e60de464e1d83c375bdd01d272290c51cede0b794301de1b7770c7bac670450143458b17521023927b837a922696836e26399f759965328437f93aafaf3e02767d22860c0fba7ac68"),
+    TestScenario(Satifiability.SATISFIABLE, "2103fb0b46d9443b88da50dba2a321b35ef38f52d83decbd121d18c16aed13e5aea4ac6374632103f9d1dffcb32de42982f022db41eed2deec76856798919028585bb28117e546e9ac6704fdf0ee58b16868"),
+    TestScenario(Satifiability.SATISFIABLE, "0400925e5a7576140d22433293fe9652ea00d21c5061697aef5ddb2988ac"),
+    TestScenario(Satifiability.SATISFIABLE, ""),
+    TestScenario(Satifiability.SATISFIABLE, ""),
+    TestScenario(Satifiability.SATISFIABLE, ""),
+    TestScenario(Satifiability.SATISFIABLE, ""),
+
+
+
+]
\ No newline at end of file

tests/language/bitcoin/test_parser.py

@@ -7,7 +7,9 @@ from symbolic_execution.hardware.memory.ram import FullySymbolicRAM
 from symbolic_execution.language.bitcoin.parser import BitcoinParser
 from symbolic_execution.hardware.machines.btc_machine import BTC_VECTOR_SIZE, BTCMachine
 from symbolic_execution.program.executer.concrete import ConcreteExecuter
-from tests.language.bitcoin.testing_scenarii import TESTING_SCENARII
+from .concrete.testing_scenarii import TESTING_SCENARII as CONCRETE_TESTING_SCENARII
+from .symbolic.testing_scenarii import TESTING_SCENARII as SYMBOLIC_TESTING_SCENARII
+from symbolic_execution.language.bitcoin.symbolic_interpreter import find_unlocking_script
 from z3 import is_expr
 
 
@@ -15,21 +17,21 @@ class TestParser(unittest.TestCase):
     btc_parser = BitcoinParser()
 
     def test_tokenify_script(self):
-        for scenario in TESTING_SCENARII:
+        for scenario in CONCRETE_TESTING_SCENARII:
             with self.subTest(scenario.name):
                 tokens = self.btc_parser.tokenize_code(scenario.hex_script)
                 self.assertEqual(tokens, scenario.tokens)
 
     def test_build_program(self):
-        for scenario in TESTING_SCENARII:
+        for scenario in CONCRETE_TESTING_SCENARII:
             with self.subTest(scenario.name):
                 graph = self.btc_parser.build_control_flow_graph(scenario.tokens)
                 program = ConcreteExecuter().build_flat_program(graph)
                 self.assertEqual(str(list(program.values())), scenario.program)
 
-    def test_execution(self):
+    def test_concrete_execution(self):
         for memory_type in [FullySymbolicRAM]:
-            for scenario in TESTING_SCENARII:
+            for scenario in CONCRETE_TESTING_SCENARII:
                 with self.subTest(f"{scenario.name} on {memory_type.__name__}"):
                     graph = self.btc_parser.build_control_flow_graph(scenario.tokens)
 
@@ -85,6 +87,12 @@ class TestParser(unittest.TestCase):
 
                             elt_i += 1
 
+    def test_symbolic_execution(self):
+        for i, scenario in enumerate(SYMBOLIC_TESTING_SCENARII):
+            with self.subTest(i):
+                _, status = find_unlocking_script(scenario.hex_script)
+                self.assertEqual(status, scenario.execution_status)
+
 
 if __name__ == "__main__":
     unittest.main()