diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a728fe90..0860c295 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -46,13 +46,14 @@ jobs: if [ -f requirements.txt ]; then pip3 install -r requirements.txt; fi - name: Typecheck python code working-directory: ./python - run: mypy argo saw cryptol + run: mypy argo_client - name: Build run: | cabal build all - name: Cabal argo tests run: cabal test argo - - name: Cabal file-echo-api tests - run: cabal test file-echo-api - - name: Python unit tests - run: cabal test python + - name: Python argo-client unit tests + working-directory: ./python + run: | + bash tests/run_test_servers.sh + python3 -m unittest tests/test_file-echo-api.py diff --git a/README.rst b/README.rst index e3a07387..743954a4 100644 --- a/README.rst +++ b/README.rst @@ -124,7 +124,7 @@ Working on the Python bindings To run the ``mypy`` type checker, enter the virtual environment and then run:: - mypy argo saw cryptol + mypy argo_client from the ``python`` subdirectory. diff --git a/cabal.project b/cabal.project index fb4ae003..34197e10 100644 --- a/cabal.project +++ b/cabal.project @@ -1,5 +1,4 @@ packages: argo/ - python/ file-echo-api/ tasty-script-exitcode/ diff --git a/docs/CryptolPython.rst b/docs/CryptolPython.rst deleted file mode 100644 index 4cc0f656..00000000 --- a/docs/CryptolPython.rst +++ /dev/null @@ -1,21 +0,0 @@ -================== -Cryptol Python API -================== - -Module ``cryptol`` -================== - -.. automodule:: cryptol - -.. autofunction:: cryptol.connect - -.. autoclass:: cryptol.CryptolConnection - :members: - :special-members: - -Module ``cryptol.cryptoltypes`` -=============================== - -.. automodule:: cryptol.cryptoltypes - :members: - :special-members: diff --git a/docs/SAWPython.rst b/docs/SAWPython.rst deleted file mode 100644 index 806899e4..00000000 --- a/docs/SAWPython.rst +++ /dev/null @@ -1,3 +0,0 @@ -============== -SAW Python API -============== diff --git a/dreams/salsa20.py b/dreams/salsa20.py deleted file mode 100644 index 26054590..00000000 --- a/dreams/salsa20.py +++ /dev/null @@ -1,43 +0,0 @@ -import SAW - - -class SpecUtils: - def pointer_to_fresh(self, name, ty): - x = self.fresh_var(name, ty) - xp = self.alloc(ty) - self.points_to(xp, x) - - return (x, xp) - -saw = SAW.connect() - -saw.import_cryptol("Salsa20.cry") - -salsa20_mod = saw.llvm.load_module("salsa20.bc") - -i8 = saw.llvm.int_t(8); - -class Salsa20Encrypt32Spec(SAW.LLVMSpec, SpecUtils): - def __init__(self, width): - self.width = width - - def i8_array(self, size): - return saw.llvm.array_t(size, i8) - - def spec(self): - key, pkey = self.pointer_to_fresh("key", self.i8_array(32)) - v, pv = self.pointer_to_fresh("key", self.i8_array(32)) - m, pm = self.pointer_to_fresh("buf", self.i8_array(self.width)) - si = self.cryptol("0 : [32]") - buflen = self.cryptol("`%{n} : 32") % {'n' : self.width} - - self.call(pkey, pv, si, pm, buflen) - - self.points_to(pm, self.cryptol("Salsa20_encrypt (%key, %v, %m)" % {'key' : key, 'v': v, 'm': m})) - self.returns(self.cryptol("0 : [32]")) - -# TODO add time call from Python lib -for size in [63, 64, 65]: - saw.crucible.llvm_verify(salsa20_mod, "s20_crypt32", Salsa20Encrypt32Spec(size)) - -print("Done!") diff --git a/dreams/salsa20_comp.py b/dreams/salsa20_comp.py deleted file mode 100644 index b899e826..00000000 --- a/dreams/salsa20_comp.py +++ /dev/null @@ -1,99 +0,0 @@ -import SAW - -saw = SAW.connect() - -saw.import_cryptol("Salsa20.cry") - -salsa20_mod = saw.llvm.load_module("salsa20.bc") - - -class SpecUtils(SAW.LLVMSpec): - def pointer_to_fresh(self, name, ty): - x = self.fresh_var(name, ty) - xp = self.alloc(ty) - self.points_to(xp, x) - - return (x, xp) - - def alloc_init(self, ty, val): - p = self.alloc(ty) - self.points_to(p, v) - return p - - -class PtrUpdateSpec(SpecUtils): - def __init__(self, n, size, ty, f): - self.n = n - self.size = size - self.ty = ty - self.f = f - - def spec(self): - x, p = self.ptr_to_fresh(self.n, saw.llvm.array_t(self.size, self.ty)) - self.call(self.p) - self.points_to(self.p, self.cryptol("%f %x") % {'f': self.f, 'x': self.x}) - - -i8 = saw.llvm.int_t(8) -i32 = saw.llvm.int_t(32) - -class QuarterRoundSetup(SpecUtils): - def spec(self): - y0, p0 = self.ptr_to_fresh("y0", i32) - y1, p1 = self.ptr_to_fresh("y1", i32) - y2, p2 = self.ptr_to_fresh("y2", i32) - y3, p3 = self.ptr_to_fresh("y3", i32) - - self.call(p0, p1, p2, p3) - - zs = self.cryptol("quarterround [%{y0}, %{y1}, %{y2}, %{y3}]") % - {'y0': y0, 'y1': y1, 'y2': y2, 'y3': t3} - self.points_to(p0, self.cryptol("%{zs}@0") % {'zs': zs}) - self.points_to(p1, self.cryptol("%{zs}@1") % {'zs': zs}) - self.points_to(p2, self.cryptol("%{zs}@2") % {'zs': zs}) - self.points_to(p3, self.cryptol("%{zs}@3") % {'zs': zs}) - -row_round_spec = PtrUpdateSpec("y", 16, i32, cryptol("rowround")) -column_round_spec = PtrUpdateSpec("x", 16, i32, cryptol("columnround")) -double_round_spec = PtrUpdateSpec("x", 16, i32, cryptol("doubleround")) -salsa20_spec = PtrUpdateSpec("seq", 64, i8, cryptol("Salsa20")) - -class Salsa20Expansion32(SpecUtils): - def spec(self): - k, pk = self.pointer_to_fresh("k", saw.llvm.array_t(32, i8)) - n, pn = self.pointer_to_fresh("n", saw.llvm.array_t(16, i8)) - pks = self.alloc(saw.llvm.array_t(64, i8)) - - self.call(pk, pn, pks) - - rks = self.cryptol("Salsa20_expansion`{a=2}(%, %)") % (k, n) - self.points_to(pks, rks) - -class Salsa20Encrypt32(SpecUtils): - def __init__(self, size): - self.size = size - - def spec(self): - key, pkey = self.pointer_to_fresh("key", saw.llvm.array_t(32, i8)) - v, pv = self.pointer_to_fresh("nonce", saw.llvm.array_t( 8, i8)) - m, pm = self.pointer_to_fresh("buf", saw.llvm.array_t( n, i8)) - - self.call(pkey, pv, self.cryptol("0 : [32]"), pm, self.cryptol("`% : [32]") % self.size) - self.points_to(pm, self.cryptol("Salsa20_encrypt (%{key}, %{v}, %{m})") % {'key': key, 'v': v, 'm': m}) - self.returns(self.cryptol("0 : [32]")) - -# TODO translate me -# let main : TopLevel () = do { -# m <- llvm_load_module "salsa20.bc"; -# let verify f ovs spec = crucible_llvm_verify m f ovs true spec abc; -# qr <- verify "s20_quarterround" [] quarterround_setup; -# rr <- verify "s20_rowround" [qr] rowround_setup; -# cr <- verify "s20_columnround" [qr] columnround_setup; -# dr <- verify "s20_doubleround" [cr,rr] doubleround_setup; -# s20 <- verify "s20_hash" [dr] salsa20_setup; -# s20e32 <- verify "s20_expand32" [s20] salsa20_expansion_32; -# s20encrypt63 <- time (verify "s20_crypt32" [s20e32] (s20_encrypt32 63)); -# s20encrypt64 <- time (verify "s20_crypt32" [s20e32] (s20_encrypt32 64)); -# s20encrypt65 <- time (verify "s20_crypt32" [s20e32] (s20_encrypt32 65)); -# print "Done!"; -# }; diff --git a/dreams/swap.py b/dreams/swap.py deleted file mode 100644 index d73222a3..00000000 --- a/dreams/swap.py +++ /dev/null @@ -1,46 +0,0 @@ -import SAW - -saw = SAW.connect() - -swap_mod = saw.llvm.load_module("swap-correct.bc") - -model = swap_mod.extract("swap_correct") - -thm = saw.abc.prove_print(saw.cryptol("\ x y -> %{model} x y != 0") % {'model': model}) - - -class SwapSpec (SAW.LLVMSpec): - def spec(self): - x = self.fresh_var("x", saw.llvm.int_t(32)) - y = self.fresh_var("y", saw.llvm.int_t(32)) - xp = self.alloc(saw.llvm.int_t(32)) - yp = self.alloc(saw.llvm.int_t(32)) - self.points_to(xp, x) - self.points_to(yp, y) - - self.call(xp, yp) - - self.points_to(xp, y) - self.points_to(yp, x) - - -class SwapSpec2 (SAW.LLVMSpec): - def pointer_to_fresh(self, name, ty): - x = self.fresh_var(name, ty) - xp = self.alloc(ty) - self.points_to(xp, x) - - return (x, xp) - - def spec(self): - x, xp = self.pointer_to_fresh("x", saw.llvm.int_t(32)) - y, yp = self.pointer_to_fresh("y", saw.llvm.int_t(32)) - - self.call(xp, yp) - - self.points_to(xp, y) - self.points_to(yp, x) - - -saw.crucible.llvm_verify(swap_mod, "swap_xor", SwapSpec2(), extra_specs=[], path_sat=True, prover=saw.abc) - diff --git a/examples/Salsa20.cry b/examples/Salsa20.cry deleted file mode 100644 index 782d5d96..00000000 --- a/examples/Salsa20.cry +++ /dev/null @@ -1,182 +0,0 @@ -/* - * Copyright (c) 2013-2016 Galois, Inc. - * Distributed under the terms of the BSD3 license (see LICENSE file) - */ - -// see http://cr.yp.to/snuffle/spec.pdf - -module Salsa20 where - -quarterround : [4][32] -> [4][32] -quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3] - where - z1 = y1 ^ ((y0 + y3) <<< 0x7) - z2 = y2 ^ ((z1 + y0) <<< 0x9) - z3 = y3 ^ ((z2 + z1) <<< 0xd) - z0 = y0 ^ ((z3 + z2) <<< 0x12) - -property quarterround_passes_tests = - (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000000] == [0x00000000, 0x00000000, 0x00000000, 0x00000000]) /\ - (quarterround [0x00000001, 0x00000000, 0x00000000, 0x00000000] == [0x08008145, 0x00000080, 0x00010200, 0x20500000]) /\ - (quarterround [0x00000000, 0x00000001, 0x00000000, 0x00000000] == [0x88000100, 0x00000001, 0x00000200, 0x00402000]) /\ - (quarterround [0x00000000, 0x00000000, 0x00000001, 0x00000000] == [0x80040000, 0x00000000, 0x00000001, 0x00002000]) /\ - (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000001] == [0x00048044, 0x00000080, 0x00010000, 0x20100001]) /\ - (quarterround [0xe7e8c006, 0xc4f9417d, 0x6479b4b2, 0x68c67137] == [0xe876d72b, 0x9361dfd5, 0xf1460244, 0x948541a3]) /\ - (quarterround [0xd3917c5b, 0x55f1c407, 0x52a58a7a, 0x8f887a3b] == [0x3e2f308c, 0xd90a8f36, 0x6ab2a923, 0x2883524c]) - -rowround : [16][32] -> [16][32] -rowround [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] = - [z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15] - where - [ z0, z1, z2, z3] = quarterround [ y0, y1, y2, y3] - [ z5, z6, z7, z4] = quarterround [ y5, y6, y7, y4] - [z10, z11, z8, z9] = quarterround [y10, y11, y8, y9] - [z15, z12, z13, z14] = quarterround [y15, y12, y13, y14] - -property rowround_passes_tests = - (rowround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000] == - [0x08008145, 0x00000080, 0x00010200, 0x20500000, - 0x20100001, 0x00048044, 0x00000080, 0x00010000, - 0x00000001, 0x00002000, 0x80040000, 0x00000000, - 0x00000001, 0x00000200, 0x00402000, 0x88000100]) /\ - (rowround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, - 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, - 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, - 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == - [0xa890d39d, 0x65d71596, 0xe9487daa, 0xc8ca6a86, - 0x949d2192, 0x764b7754, 0xe408d9b9, 0x7a41b4d1, - 0x3402e183, 0x3c3af432, 0x50669f96, 0xd89ef0a8, - 0x0040ede5, 0xb545fbce, 0xd257ed4f, 0x1818882d]) - - -rowround_opt : [16][32] -> [16][32] -rowround_opt ys = join [ (quarterround (yi<<>>i | yi <- split ys | i <- [0 .. 3] ] - -property rowround_opt_is_rowround ys = rowround ys == rowround_opt ys - -columnround : [16][32] -> [16][32] -columnround [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15] = - [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] - where - [ y0, y4, y8, y12] = quarterround [ x0, x4, x8, x12] - [ y5, y9, y13, y1] = quarterround [ x5, x9, x13, x1] - [y10, y14, y2, y6] = quarterround [x10, x14, x2, x6] - [y15, y3, y7, y11] = quarterround [x15, x3, x7, x11] - -property columnround_passes_tests = - (columnround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000] == - [0x10090288, 0x00000000, 0x00000000, 0x00000000, - 0x00000101, 0x00000000, 0x00000000, 0x00000000, - 0x00020401, 0x00000000, 0x00000000, 0x00000000, - 0x40a04001, 0x00000000, 0x00000000, 0x00000000]) /\ - (columnround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, - 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, - 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, - 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == - [0x8c9d190a, 0xce8e4c90, 0x1ef8e9d3, 0x1326a71a, - 0x90a20123, 0xead3c4f3, 0x63a091a0, 0xf0708d69, - 0x789b010c, 0xd195a681, 0xeb7d5504, 0xa774135c, - 0x481c2027, 0x53a8e4b5, 0x4c1f89c5, 0x3f78c9c8]) - - -columnround_opt : [16][32] -> [16][32] -columnround_opt xs = join (transpose [ (quarterround (xi<<>>i | xi <- transpose(split xs) | i <- [0 .. 3] ]) - -columnround_opt_is_columnround xs = columnround xs == columnround_opt xs - -property columnround_is_transpose_of_rowround ys = - rowround ys == join(transpose(split`{4}(columnround xs))) - where xs = join(transpose(split`{4} ys)) - -doubleround : [16][32] -> [16][32] -doubleround(xs) = rowround(columnround(xs)) - -property doubleround_passes_tests = - (doubleround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000] == - [0x8186a22d, 0x0040a284, 0x82479210, 0x06929051, - 0x08000090, 0x02402200, 0x00004000, 0x00800000, - 0x00010200, 0x20400000, 0x08008104, 0x00000000, - 0x20500000, 0xa0000040, 0x0008180a, 0x612a8020]) /\ - (doubleround [0xde501066, 0x6f9eb8f7, 0xe4fbbd9b, 0x454e3f57, - 0xb75540d3, 0x43e93a4c, 0x3a6f2aa0, 0x726d6b36, - 0x9243f484, 0x9145d1e8, 0x4fa9d247, 0xdc8dee11, - 0x054bf545, 0x254dd653, 0xd9421b6d, 0x67b276c1] == - [0xccaaf672, 0x23d960f7, 0x9153e63a, 0xcd9a60d0, - 0x50440492, 0xf07cad19, 0xae344aa0, 0xdf4cfdfc, - 0xca531c29, 0x8e7943db, 0xac1680cd, 0xd503ca00, - 0xa74b2ad6, 0xbc331c5c, 0x1dda24c7, 0xee928277]) - -littleendian : [4][8] -> [32] -littleendian b = join(reverse b) - -property littleendian_passes_tests = - (littleendian [ 0, 0, 0, 0] == 0x00000000) /\ - (littleendian [ 86, 75, 30, 9] == 0x091e4b56) /\ - (littleendian [255, 255, 255, 250] == 0xfaffffff) - -littleendian_inverse : [32] -> [4][8] -littleendian_inverse b = reverse(split b) - -property littleendian_is_invertable b = littleendian_inverse(littleendian b) == b - -Salsa20 : [64][8] -> [64][8] -Salsa20 xs = join ar - where - ar = [ littleendian_inverse words | words <- xw + zs@10 ] - xw = [ littleendian xi | xi <- split xs ] - zs = [xw] # [ doubleround zi | zi <- zs ] - -property Salsa20_passes_tests = - (Salsa20 [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] == - [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) /\ - (Salsa20 [211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, 191, 187, 234, 136, - 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, 86, 16, 179, 207, - 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113, 238, 55, 204, 36, - 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, 88, 118, 104, 54] == - [109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, 26, 110, 170, 154, - 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, 69, 144, 51, 57, - 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35, 27, 111, 114, 114, - 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, 179, 19, 48, 202]) /\ - (Salsa20 [ 88, 118, 104, 54, 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, - 191, 187, 234, 136, 211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, - 86, 16, 179, 207, 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, - 238, 55, 204, 36, 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113] == - [179, 19, 48, 202, 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, - 26, 110, 170, 154, 109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, - 69, 144, 51, 57, 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, - 27, 111, 114, 114, 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35]) - -property Salsa20_has_no_collisions x1 x2 = - if(x1 != x2) then (doubleround x1) != (doubleround x2) else True - -// Salsa 20 supports two key sizes, [16][8] and [32][8] -Salsa20_expansion : {a} (a >= 1, 2 >= a) => ([16*a][8], [16][8]) -> [64][8] -Salsa20_expansion(k, n) = z - where - [s0, s1, s2, s3] = split "expand 32-byte k" : [4][4][8] - [t0, t1, t2, t3] = split "expand 16-byte k" : [4][4][8] - x = if(`a == 2) then s0 # k0 # s1 # n # s2 # k1 # s3 - else t0 # k0 # t1 # n # t2 # k0 # t3 - z = Salsa20(x) - [k0, k1] = (split(k#zero)):[2][16][8] - -Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([16*a][8], [8][8], [l][8]) -> [l][8] -Salsa20_encrypt(k, v, m) = c - where - salsa = take (join [ Salsa20_expansion(k, v#(reverse (split i))) | i <- [0, 1 ... ] ]) - c = m ^ salsa diff --git a/examples/salsa20.bc b/examples/salsa20.bc deleted file mode 100644 index 80847446..00000000 Binary files a/examples/salsa20.bc and /dev/null differ diff --git a/examples/salsa20.c b/examples/salsa20.c deleted file mode 100644 index fd951639..00000000 --- a/examples/salsa20.c +++ /dev/null @@ -1,191 +0,0 @@ -#include -#include -#include "salsa20.h" - -// Implements DJB's definition of '<<<' -static uint32_t rotl(uint32_t value, int shift) -{ - return (value << shift) | (value >> (32 - shift)); -} - -static void s20_quarterround(uint32_t *y0, uint32_t *y1, uint32_t *y2, uint32_t *y3) -{ - *y1 = *y1 ^ rotl(*y0 + *y3, 7); - *y2 = *y2 ^ rotl(*y1 + *y0, 9); - *y3 = *y3 ^ rotl(*y2 + *y1, 13); - *y0 = *y0 ^ rotl(*y3 + *y2, 18); -} - -static void s20_rowround(uint32_t y[static 16]) -{ - s20_quarterround(&y[0], &y[1], &y[2], &y[3]); - s20_quarterround(&y[5], &y[6], &y[7], &y[4]); - s20_quarterround(&y[10], &y[11], &y[8], &y[9]); - s20_quarterround(&y[15], &y[12], &y[13], &y[14]); -} - -static void s20_columnround(uint32_t x[static 16]) -{ - s20_quarterround(&x[0], &x[4], &x[8], &x[12]); - s20_quarterround(&x[5], &x[9], &x[13], &x[1]); - s20_quarterround(&x[10], &x[14], &x[2], &x[6]); - s20_quarterround(&x[15], &x[3], &x[7], &x[11]); -} - -static void s20_doubleround(uint32_t x[static 16]) -{ - s20_columnround(x); - s20_rowround(x); -} - -// Creates a little-endian word from 4 bytes pointed to by b -static uint32_t s20_littleendian(uint8_t *b) -{ - return b[0] + - (b[1] << 8) + - (b[2] << 16) + - (b[3] << 24); -} - -// Moves the little-endian word into the 4 bytes pointed to by b -static void s20_rev_littleendian(uint8_t *b, uint32_t w) -{ - b[0] = w; - b[1] = w >> 8; - b[2] = w >> 16; - b[3] = w >> 24; -} - -// The core function of Salsa20 -static void s20_hash(uint8_t seq[static 64]) -{ - int i; - uint32_t x[16]; - uint32_t z[16]; - - // Create two copies of the state in little-endian format - // First copy is hashed together - // Second copy is added to first, word-by-word - for (i = 0; i < 16; ++i) - x[i] = z[i] = s20_littleendian(seq + (4 * i)); - - for (i = 0; i < 10; ++i) - s20_doubleround(z); - - for (i = 0; i < 16; ++i) { - z[i] += x[i]; - s20_rev_littleendian(seq + (4 * i), z[i]); - } -} - -// The 16-byte (128-bit) key expansion function -static void s20_expand16(uint8_t *k, - uint8_t n[static 16], - uint8_t keystream[static 64]) -{ - int i, j; - // The constants specified by the Salsa20 specification, 'tau' - // "expand 16-byte k" - uint8_t t[4][4] = { - { 'e', 'x', 'p', 'a' }, - { 'n', 'd', ' ', '1' }, - { '6', '-', 'b', 'y' }, - { 't', 'e', ' ', 'k' } - }; - - // Copy all of 'tau' into the correct spots in our keystream block - for (i = 0; i < 64; i += 20) - for (j = 0; j < 4; ++j) - keystream[i + j] = t[i / 20][j]; - - // Copy the key and the nonce into the keystream block - for (i = 0; i < 16; ++i) { - keystream[4+i] = k[i]; - keystream[44+i] = k[i]; - keystream[24+i] = n[i]; - } - - s20_hash(keystream); -} - - -// The 32-byte (256-bit) key expansion function -static void s20_expand32(uint8_t *k, - uint8_t n[static 16], - uint8_t keystream[static 64]) -{ - int i, j; - // The constants specified by the Salsa20 specification, 'sigma' - // "expand 32-byte k" - uint8_t o[4][4] = { - { 'e', 'x', 'p', 'a' }, - { 'n', 'd', ' ', '3' }, - { '2', '-', 'b', 'y' }, - { 't', 'e', ' ', 'k' } - }; - - // Copy all of 'sigma' into the correct spots in our keystream block - for (i = 0; i < 64; i += 20) - for (j = 0; j < 4; ++j) - keystream[i + j] = o[i / 20][j]; - - // Copy the key and the nonce into the keystream block - for (i = 0; i < 16; ++i) { - keystream[4+i] = k[i]; - keystream[44+i] = k[i+16]; - keystream[24+i] = n[i]; - } - - s20_hash(keystream); -} - -// Performs up to 2^32-1 bytes of encryption or decryption under a -// 128- or 256-bit key. -enum s20_status_t s20_crypt32(uint8_t *key, - uint8_t nonce[static 8], - uint32_t si, - uint8_t *buf, - uint32_t buflen) -{ - uint8_t keystream[64]; - // 'n' is the 8-byte nonce (unique message number) concatenated - // with the per-block 'counter' value (4 bytes in our case, 8 bytes - // in the standard). We leave the high 4 bytes set to zero because - // we permit only a 32-bit integer for stream index and length. - uint8_t n[16] = { 0 }; - uint32_t i; - - // If any of the parameters we received are invalid - if (key == NULL || nonce == NULL || buf == NULL) - return S20_FAILURE; - - // Set up the low 8 bytes of n with the unique message number - for (i = 0; i < 8; ++i) - n[i] = nonce[i]; - - // If we're not on a block boundary, compute the first keystream - // block. This will make the primary loop (below) cleaner - if (si % 64 != 0) { - // Set the second-to-highest 4 bytes of n to the block number - s20_rev_littleendian(n+8, si / 64); - // Expand the key with n and hash to produce a keystream block - s20_expand32(key, n, keystream); - } - - // Walk over the plaintext byte-by-byte, xoring the keystream with - // the plaintext and producing new keystream blocks as needed - for (i = 0; i < buflen; ++i) { - // If we've used up our entire keystream block (or have just begun - // and happen to be on a block boundary), produce keystream block - if ((si + i) % 64 == 0) { - s20_rev_littleendian(n+8, ((si + i) / 64)); - s20_expand32(key, n, keystream); - } - - // xor one byte of plaintext with one byte of keystream - buf[i] ^= keystream[(si + i) % 64]; - } - - return S20_SUCCESS; -} - diff --git a/examples/salsa20.h b/examples/salsa20.h deleted file mode 100644 index df94eed6..00000000 --- a/examples/salsa20.h +++ /dev/null @@ -1,72 +0,0 @@ -#ifndef _SALSA20_H_ -#define _SALSA20_H_ - -#include -#include - -/** - * Return codes for s20_crypt - */ -enum s20_status_t -{ - S20_SUCCESS, - S20_FAILURE -}; - -/** - * Key size - * Salsa20 only permits a 128-bit key or a 256-bit key, so these are - * the only two options made available by this library. - */ -enum s20_keylen_t -{ - S20_KEYLEN_256, - S20_KEYLEN_128 -}; - -/** - * Performs up to 2^32-1 bytes of encryption or decryption under a - * 128- or 256-bit key in blocks of arbitrary size. Permits seeking - * to any point within a stream. - * - * key Pointer to either a 128-bit or 256-bit key. - * No key-derivation function is applied to this key, and no - * entropy is gathered. It is expected that this key is already - * appropriate for direct use by the Salsa20 algorithm. - * - * keylen Length of the key. - * Must be S20_KEYLEN_256 or S20_KEYLEN_128. - * - * nonce Pointer to an 8-byte nonce. - * Does not have to be random, but must be unique for every - * message under a single key. Nonce reuse destroys message - * confidentiality. - * - * si Stream index. - * The position within the stream. When encrypting/decrypting - * a message sequentially from beginning to end in fixed-size - * chunks of length L, this value is increased by L on every - * call. Care must be taken not to select values that cause - * overlap. Example: encrypting 1000 bytes at index 100, and - * then encrypting 1000 bytes at index 500. Doing so will - * result in keystream reuse, which destroys message - * confidentiality. - * - * buf The data to encrypt or decrypt. - * - * buflen Length of the data in buf. - * - * This function returns either S20_SUCCESS or S20_FAILURE. - * A return of S20_SUCCESS indicates that basic sanity checking on - * parameters succeeded and encryption/decryption was performed. - * A return of S20_FAILURE indicates that basic sanity checking on - * parameters failed and encryption/decryption was not performed. - */ -enum s20_status_t s20_crypt(uint8_t *key, - enum s20_keylen_t keylen, - uint8_t nonce[static 8], - uint32_t si, - uint8_t *buf, - uint32_t buflen); - -#endif diff --git a/examples/salsa20.py b/examples/salsa20.py deleted file mode 100755 index 82b0fe73..00000000 --- a/examples/salsa20.py +++ /dev/null @@ -1,187 +0,0 @@ -#!/usr/bin/env python3 -import os -import os.path -from cryptol.cryptoltypes import to_cryptol -from saw.llvm import Contract, LLVMArrayType, uint8_t, uint32_t, void -from saw import * -from saw.dashboard import Dashboard - -dir_path = os.path.dirname(os.path.realpath(__file__)) -connect("cabal -v0 v2-run exe:saw-remote-api") -view(DebugLog(err=None)) -view(LogResults()) -view(Dashboard(path=__file__)) - -bcname = os.path.join(dir_path, 'salsa20.bc') -cryname = os.path.join(dir_path, 'Salsa20.cry') - -cryptol_load_file(cryname) - -mod = llvm_load_module(bcname) - -class RotlContract(Contract): - def pre(self): - self.value = self.declare(uint32_t) - self.shift = self.declare(uint32_t) - self.proclaim(self.shift > self.cryptol("0")) - self.proclaim(self.shift < self.cryptol("32")) - def call(self): - self.arguments(self.value, self.shift) - def post(self): - self.returns(self.cryptol("(<<<)")(self.value, self.shift)) - - -rotl_result = llvm_verify(mod, 'rotl', RotlContract()) - -class TrivialContract(Contract): - def post(self): self.returns(void) - -class QuarterRoundContract(Contract): - def pre(self): - self.y0 = self.declare(uint32_t) - self.y1 = self.declare(uint32_t) - self.y2 = self.declare(uint32_t) - self.y3 = self.declare(uint32_t) - - self.y0_p = self.declare_pointer(uint32_t) - self.y1_p = self.declare_pointer(uint32_t) - self.y2_p = self.declare_pointer(uint32_t) - self.y3_p = self.declare_pointer(uint32_t) - - self.points_to(self.y0_p, self.y0) - self.points_to(self.y1_p, self.y1) - self.points_to(self.y2_p, self.y2) - self.points_to(self.y3_p, self.y3) - - def call(self): - self.arguments(self.y0_p, self.y1_p, self.y2_p, self.y3_p) - - def post(self): - self.points_to(self.y0_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("0"))) - self.points_to(self.y1_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("1"))) - self.points_to(self.y2_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("2"))) - self.points_to(self.y3_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("3"))) - self.returns(void) - - -qr_result = llvm_verify(mod, 's20_quarterround', QuarterRoundContract(), lemmas=[rotl_result]) - - -class OnePointerUpdateContract(Contract): - def __init__(self, the_type): - super().__init__() - self.t = the_type - - - def pre(self): - self.y = self.declare(self.t) - self.y_p = self.declare_pointer(self.t) - self.points_to(self.y_p, self.y) - - def call(self): - self.arguments(self.y_p) - - def post(self): - - self.returns(void) - - -class RowRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("rowround")(self.y)) - -rr_result = llvm_verify(mod, 's20_rowround', RowRoundContract(), lemmas=[qr_result]) - - -class ColumnRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("columnround")(self.y)) - -cr_result = llvm_verify(mod, 's20_columnround', ColumnRoundContract(), lemmas=[rr_result]) - - -class DoubleRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("doubleround")(self.y)) - -dr_result = llvm_verify(mod, 's20_doubleround', DoubleRoundContract(), lemmas=[cr_result, rr_result]) - - -class HashContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint8_t, 64)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("Salsa20")(self.y)) - -hash_result = llvm_verify(mod, 's20_hash', HashContract(), lemmas=[dr_result]) - - -class ExpandContract(Contract): - def pre(self): - self.k = self.declare(LLVMArrayType(uint8_t, 32)) - self.n = self.declare(LLVMArrayType(uint8_t, 16)) - - self.k_p = self.declare_pointer(LLVMArrayType(uint8_t, 32)) - self.n_p = self.declare_pointer(LLVMArrayType(uint8_t, 16)) - self.ks_p = self.declare_pointer(LLVMArrayType(uint8_t, 64)) - - self.points_to(self.k_p, self.k) - self.points_to(self.n_p, self.n) - - def call(self): - self.arguments(self.k_p, self.n_p, self.ks_p) - - def post(self): - self.returns(void) - self.points_to(self.ks_p, self.cryptol("Salsa20_expansion`{a=2}")((self.k, self.n))) - -expand_result = llvm_verify(mod, 's20_expand32', ExpandContract(), lemmas=[hash_result]) - - -class Salsa20CryptContract(Contract): - def __init__(self, size): - super().__init__() - self.size = size - self.zero = self.cryptol("0 : [32]") - - def val_and_pointer(self, t): - v = self.declare(t) - p = self.declare_pointer(t) - self.points_to(p, v) - return (v, p) - - def pre(self): - (self.k, self.k_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 32)) - (self.v, self.v_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 8)) - (self.m, self.m_p) = self.val_and_pointer(LLVMArrayType(uint8_t, self.size)) - - def call(self): - self.arguments(self.k_p, self.v_p, self.zero, self.m_p, self.cryptol(str(self.size) + " : [32]")) - - def post(self): - self.returns(self.zero) - self.points_to(self.m_p, self.cryptol("Salsa20_encrypt")((self.k, self.v, self.m))) - -crypt_result = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(63), lemmas=[expand_result]) diff --git a/examples/swap.bc b/examples/swap.bc deleted file mode 100644 index e6293c8d..00000000 Binary files a/examples/swap.bc and /dev/null differ diff --git a/examples/swap.c b/examples/swap.c deleted file mode 100644 index 37804462..00000000 --- a/examples/swap.c +++ /dev/null @@ -1,13 +0,0 @@ -#include - -void swap(uint32_t *a, uint32_t *b) { - uint32_t tmp = *a; - *a = *b; - *b = tmp; -} - -void xor_swap(uint32_t *a, uint32_t *b) { - *a ^= *b; - *b ^= *a; - *a ^= *b; -} diff --git a/examples/swap.py b/examples/swap.py deleted file mode 100755 index e62d40f6..00000000 --- a/examples/swap.py +++ /dev/null @@ -1,39 +0,0 @@ -#!/usr/bin/env python3 -from saw import * -from saw.dashboard import Dashboard -from saw.llvm import uint32_t, Contract, void - -import os -import os.path - -dir_path = os.path.dirname(os.path.realpath(__file__)) -swap_bc = os.path.join(dir_path, 'swap.bc') - -class Swap(Contract): - def __init__(self) -> None: - super().__init__() - self.t = uint32_t - - def pre(self) -> None: - self.x = self.declare(self.t) - self.y = self.declare(self.t) - self.x_pointer = self.declare_pointer(self.t) - self.y_pointer = self.declare_pointer(self.t) - self.points_to(self.x_pointer, self.x) - self.points_to(self.y_pointer, self.y) - - def call(self) -> None: - self.arguments(self.x_pointer, self.y_pointer) - - def post(self) -> None: - self.points_to(self.x_pointer, self.y) - self.points_to(self.y_pointer, self.x) - self.returns(void) - -connect("cabal -v0 v2-run exe:saw-remote-api") -view(DebugLog(err=None)) -view(LogResults()) - -mod = llvm_load_module(swap_bc) - -result = llvm_verify(mod, 'swap', Swap()) diff --git a/file-echo-api/file-echo-api.cabal b/file-echo-api/file-echo-api.cabal index d3e054b4..8c3ae6cc 100644 --- a/file-echo-api/file-echo-api.cabal +++ b/file-echo-api/file-echo-api.cabal @@ -56,17 +56,3 @@ executable file-echo-api build-depends: file-echo-api - -test-suite test-file-echo-api - import: deps, warnings - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Test.hs - other-modules: Paths_file_echo_api - build-depends: - argo-python, - file-echo-api, - quickcheck-instances ^>= 0.3.19, - tasty >= 1.2.1, - tasty-quickcheck ^>= 0.10, - tasty-script-exitcode diff --git a/python/LICENSE b/python/LICENSE new file mode 100644 index 00000000..36cd7c51 --- /dev/null +++ b/python/LICENSE @@ -0,0 +1,11 @@ +Copyright 2021 Galois, Inc. + +Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/python/README.md b/python/README.md new file mode 100644 index 00000000..56bd2e11 --- /dev/null +++ b/python/README.md @@ -0,0 +1,3 @@ +# Argo Client + +A python library for client connections to [JSON RPC](https://www.jsonrpc.org/specification) servers, specifically desigend with the Haskell [Argo](https://github.com/galoisinc/argo) sister library in mind. diff --git a/python/argo-python.cabal b/python/argo-python.cabal deleted file mode 100644 index 6bf1fae7..00000000 --- a/python/argo-python.cabal +++ /dev/null @@ -1,34 +0,0 @@ -cabal-version: 2.4 -name: argo-python -version: 0.1.0.0 -synopsis: Dummy package that contains the Python components of Argo as data files. -license: BSD-3-Clause ---license-file: LICENSE -author: Galois, Inc. -maintainer: dtc@galois.com -category: Network -data-files: argo/**/*.py - cryptol/**/*.py - saw/**/*.py - requirements.txt - -library - build-depends: base - default-language: Haskell2010 - hs-source-dirs: hs - exposed-modules: Argo.PythonBindings - other-modules: Paths_argo_python - -test-suite test-argo-python - type: exitcode-stdio-1.0 - hs-source-dirs: hs-test - main-is: Main.hs - other-modules: Paths_argo_python - build-depends: base, - argo-python, - filepath, - directory, - tasty, - tasty-hunit, - tasty-quickcheck, - tasty-script-exitcode diff --git a/python/argo/__init__.py b/python/argo_client/__init__.py similarity index 100% rename from python/argo/__init__.py rename to python/argo_client/__init__.py diff --git a/python/argo/connection.py b/python/argo_client/connection.py similarity index 100% rename from python/argo/connection.py rename to python/argo_client/connection.py diff --git a/python/argo/interaction.py b/python/argo_client/interaction.py similarity index 99% rename from python/argo/interaction.py rename to python/argo_client/interaction.py index c2560ddf..b75863b7 100644 --- a/python/argo/interaction.py +++ b/python/argo_client/interaction.py @@ -1,6 +1,6 @@ """Higher-level tracking of the semantics of specific commands.""" -from argo.connection import ServerConnection +from argo_client.connection import ServerConnection from abc import abstractmethod from typing import Any, Dict, Tuple diff --git a/python/argo/netstring.py b/python/argo_client/netstring.py similarity index 100% rename from python/argo/netstring.py rename to python/argo_client/netstring.py diff --git a/python/argo/py.typed b/python/argo_client/py.typed similarity index 100% rename from python/argo/py.typed rename to python/argo_client/py.typed diff --git a/python/cryptol/__init__.py b/python/cryptol/__init__.py deleted file mode 100644 index ba9fbe8a..00000000 --- a/python/cryptol/__init__.py +++ /dev/null @@ -1,457 +0,0 @@ -"""Cryptol bindings from Python. Use :py:func:`cryptol.connect` to start a new connection.""" - -from __future__ import annotations - -import base64 -import os -import types -import sys -from typing import Any, Dict, Iterable, List, Mapping, NoReturn, Optional, Type, Union -from mypy_extensions import TypedDict - -import argo.interaction -from argo.interaction import HasProtocolState -from argo.connection import DynamicSocketProcess, ServerConnection, ServerProcess, StdIOProcess -from . import cryptoltypes -from . import solver -from cryptol.bitvector import BV - - -__all__ = ['cryptoltypes', 'solver'] - - - -# Current status: -# It can currently launch a server, given a suitable command line as an argument. Try this: -# >>> c = CryptolConnection("cabal -v0 run cryptol-remote-api") -# >>> f = c.load_file(FILE) -# >>> f.result() -# - - - -def extend_hex(string : str) -> str: - if len(string) % 2 == 1: - return '0' + string - else: - return string - -def fail_with(x : Exception) -> NoReturn: - "Raise an exception. This is valid in expression positions." - raise x - - - -def from_cryptol_arg(val : Any) -> Any: - """Return the canonical Python value for a Cryptol JSON value.""" - if isinstance(val, bool): - return val - elif isinstance(val, int): - return val - elif 'expression' in val.keys(): - tag = val['expression'] - if tag == 'unit': - return () - elif tag == 'tuple': - return tuple(from_cryptol_arg(x) for x in val['data']) - elif tag == 'record': - return {k : from_cryptol_arg(val[k]) for k in val['data']} - elif tag == 'sequence': - return [from_cryptol_arg(v) for v in val['data']] - elif tag == 'bits': - enc = val['encoding'] - size = val['width'] - if enc == 'base64': - n = int.from_bytes( - base64.b64decode(val['data'].encode('ascii')), - byteorder='big') - elif enc == 'hex': - n = int.from_bytes( - bytes.fromhex(extend_hex(val['data'])), - byteorder='big') - else: - raise ValueError("Unknown encoding " + str(enc)) - return BV(size, n) - else: - raise ValueError("Unknown expression tag " + tag) - else: - raise TypeError("Unsupported value " + str(val)) - - - -class CryptolChangeDirectory(argo.interaction.Command): - def __init__(self, connection : HasProtocolState, new_directory : str) -> None: - super(CryptolChangeDirectory, self).__init__( - 'change directory', - {'directory': new_directory}, - connection - ) - - def process_result(self, res : Any) -> Any: - return res - -class CryptolLoadModule(argo.interaction.Command): - def __init__(self, connection : HasProtocolState, mod_name : str) -> None: - super(CryptolLoadModule, self).__init__('load module', {'module name': mod_name}, connection) - - def process_result(self, res : Any) -> Any: - return res - -class CryptolLoadFile(argo.interaction.Command): - def __init__(self, connection : HasProtocolState, filename : str) -> None: - super(CryptolLoadFile, self).__init__('load file', {'file': filename}, connection) - - def process_result(self, res : Any) -> Any: - return res - - -class CryptolEvalExpr(argo.interaction.Query): - def __init__(self, connection : HasProtocolState, expr : Any) -> None: - super(CryptolEvalExpr, self).__init__( - 'evaluate expression', - {'expression': expr}, - connection - ) - - def process_result(self, res : Any) -> Any: - return res - -class CryptolCall(argo.interaction.Query): - def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None: - super(CryptolCall, self).__init__( - 'call', - {'function': fun, 'arguments': args}, - connection - ) - - def process_result(self, res : Any) -> Any: - return from_cryptol_arg(res['value']) - -class CryptolCheckType(argo.interaction.Query): - def __init__(self, connection : HasProtocolState, expr : Any) -> None: - super(CryptolCheckType, self).__init__( - 'check type', - {'expression': expr}, - connection - ) - - def process_result(self, res : Any) -> Any: - return res['type schema'] - -class CryptolProveSat(argo.interaction.Query): - def __init__(self, connection : HasProtocolState, qtype : str, expr : Any, solver : solver.Solver, count : Optional[int]) -> None: - super(CryptolProveSat, self).__init__( - 'prove or satisfy', - {'query type': qtype, - 'expression': expr, - 'prover': solver, - 'result count': 'all' if count is None else count}, - connection - ) - self.qtype = qtype - - def process_result(self, res : Any) -> Any: - if res['result'] == 'unsatisfiable': - if self.qtype == 'sat': - return False - elif self.qtype == 'prove': - return True - else: - raise ValueError("Unknown prove/sat query type: " + self.qtype) - elif res['result'] == 'invalid': - return [from_cryptol_arg(arg['expr']) - for arg in res['counterexample']] - elif res['result'] == 'satisfied': - return [from_cryptol_arg(arg['expr']) - for m in res['models'] - for arg in m] - else: - raise ValueError("Unknown sat result " + str(res)) - -class CryptolProve(CryptolProveSat): - def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None: - super(CryptolProve, self).__init__(connection, 'prove', expr, solver, 1) - -class CryptolSat(CryptolProveSat): - def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None: - super(CryptolSat, self).__init__(connection, 'sat', expr, solver, count) - -class CryptolNames(argo.interaction.Query): - def __init__(self, connection : HasProtocolState) -> None: - super(CryptolNames, self).__init__('visible names', {}, connection) - - def process_result(self, res : Any) -> Any: - return res - -class CryptolFocusedModule(argo.interaction.Query): - def __init__(self, connection : HasProtocolState) -> None: - super(CryptolFocusedModule, self).__init__( - 'focused module', - {}, - connection - ) - - def process_result(self, res : Any) -> Any: - return res - -def connect(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection: - """Start a new connection to a new Cryptol server process. - - :param command: The command to launch the Cryptol server. - - :param cryptol_path: An optional replacement for the contents of - the ``CRYPTOLPATH`` environment variable. - - """ - return CryptolConnection(command, cryptol_path) - -def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection: - """Start a new connection to a new Cryptol server process. - - :param command: The command to launch the Cryptol server. - - :param cryptol_path: An optional replacement for the contents of - the ``CRYPTOLPATH`` environment variable. - - """ - conn = CryptolStdIOProcess(command, cryptol_path=cryptol_path) - return CryptolConnection(conn) - - -class CryptolConnection: - """Instances of ``CryptolConnection`` represent a particular point of - time in an interaction with Cryptol. Issuing a command through a - ``CryptolConnection`` causes it to change its state into one in - which the command has been carried out. - - Use :py:meth:`cryptol.CryptolConnection.snapshot` to make a - lightweight copy of the current state that shares the underlying - server process. - - ``CryptolConnection`` is in the middle of the abstraction - hierarchy. It relieves users from thinking about explicitly - encoding state and protocol messages, but it provides a - non-blocking interface in which answers from Cryptol must be - explicitly requested. Note that blocking may occur in the case of - sequential state dependencies between commands. - """ - most_recent_result : Optional[argo.interaction.Interaction] - proc: ServerProcess - - def __init__(self, command_or_connection : Union[str, ServerConnection, ServerProcess], cryptol_path : Optional[str] = None) -> None: - self.most_recent_result = None - if isinstance(command_or_connection, ServerProcess): - self.proc = command_or_connection - self.server_connection = ServerConnection(self.proc) - elif isinstance(command_or_connection, str): - self.proc = CryptolDynamicSocketProcess(command_or_connection, cryptol_path=cryptol_path) - self.server_connection = ServerConnection(self.proc) - else: - self.server_connection = command_or_connection - - def snapshot(self) -> CryptolConnection: - """Create a lightweight snapshot of this connection. The snapshot - shares the underlying server process, but can have different - application state. - """ - copy = CryptolConnection(self.server_connection) - copy.most_recent_result = self.most_recent_result - return copy - - def protocol_state(self) -> Any: - if self.most_recent_result is None: - return None - else: - return self.most_recent_result.state() - - # Protocol messages - def change_directory(self, new_directory : str) -> argo.interaction.Command: - """Change the working directory of the Cryptol process.""" - self.most_recent_result = CryptolChangeDirectory(self, new_directory) - return self.most_recent_result - - def load_file(self, filename : str) -> argo.interaction.Command: - """Load a filename as a Cryptol module, like ``:load`` at the Cryptol - REPL. - """ - self.most_recent_result = CryptolLoadFile(self, filename) - return self.most_recent_result - - def load_module(self, module_name : str) -> argo.interaction.Command: - """Load a Cryptol module, like ``:module`` at the Cryptol REPL.""" - self.most_recent_result = CryptolLoadModule(self, module_name) - return self.most_recent_result - - def evaluate_expression(self, expression : Any) -> argo.interaction.Query: - """Evaluate a Cryptol expression, represented according to - :ref:`cryptol-json-expression`, with Python datatypes standing - for their JSON equivalents. - """ - self.most_recent_result = CryptolEvalExpr(self, expression) - return self.most_recent_result - - def call(self, fun : str, *args : List[Any]) -> argo.interaction.Query: - encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args] - self.most_recent_result = CryptolCall(self, fun, encoded_args) - return self.most_recent_result - - def check_type(self, code : Any) -> argo.interaction.Query: - """Check the type of a Cryptol expression, represented according to - :ref:`cryptol-json-expression`, with Python datatypes standing for - their JSON equivalents. - """ - self.most_recent_result = CryptolCheckType(self, code) - return self.most_recent_result - - def sat(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1) -> argo.interaction.Query: - """Check the satisfiability of a Cryptol expression, represented according to - :ref:`cryptol-json-expression`, with Python datatypes standing for - their JSON equivalents. Use the solver named `solver`, and return up to - `count` solutions. - """ - self.most_recent_result = CryptolSat(self, expr, solver, count) - return self.most_recent_result - - def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.interaction.Query: - """Check the validity of a Cryptol expression, represented according to - :ref:`cryptol-json-expression`, with Python datatypes standing for - their JSON equivalents. Use the solver named `solver`. - """ - self.most_recent_result = CryptolProve(self, expr, solver) - return self.most_recent_result - - def names(self) -> argo.interaction.Query: - """Discover the list of names currently in scope in the current context.""" - self.most_recent_result = CryptolNames(self) - return self.most_recent_result - - def focused_module(self) -> argo.interaction.Query: - """Return the name of the currently-focused module.""" - self.most_recent_result = CryptolFocusedModule(self) - return self.most_recent_result - - - -class CryptolDynamicSocketProcess(DynamicSocketProcess): - - def __init__(self, command: str, *, - persist: bool=False, - cryptol_path: Optional[str]=None): - - environment = os.environ.copy() - if cryptol_path is not None: - environment["CRYPTOLPATH"] = str(cryptol_path) - - super().__init__(command, persist=persist, environment=environment) - -class CryptolStdIOProcess(StdIOProcess): - - def __init__(self, command: str, *, - cryptol_path: Optional[str]=None): - - environment = os.environ.copy() - if cryptol_path is not None: - environment["CRYPTOLPATH"] = str(cryptol_path) - - super().__init__(command, environment=environment) - - - -class CryptolFunctionHandle: - def __init__(self, - connection : CryptolConnection, - name : str, - ty : Any, - schema : Any, - docs : Optional[str] = None) -> None: - self.connection = connection.snapshot() - self.name = name - self.ty = ty - self.schema = schema - self.docs = docs - - self.__doc__ = "Cryptol type: " + ty - if self.docs is not None and self.__doc__ is not None: - self.__doc__ += "\n" + self.docs - - def __call__(self, *args : List[Any]) -> Any: - current_type = self.schema - remaining_args = args - arg_types = cryptoltypes.argument_types(current_type) - Call = TypedDict('Call', {'expression': str, 'function': str, 'arguments': List[Any]}) - current_expr : Union[str, Call] - current_expr = self.name - found_args = [] - while len(arg_types) > 0 and len(remaining_args) > 0: - found_args.append(arg_types[0].from_python(remaining_args[0])) - current_expr = {'expression': 'call', 'function': self.name, 'arguments': found_args} - ty = self.connection.check_type(current_expr).result() - current_type = cryptoltypes.to_schema(ty) - arg_types = cryptoltypes.argument_types(current_type) - remaining_args = remaining_args[1:] - return from_cryptol_arg(self.connection.evaluate_expression(current_expr).result()['value']) - - -def cry(string : str) -> cryptoltypes.CryptolCode: - return cryptoltypes.CryptolLiteral(string) - -class CryptolModule(types.ModuleType): - def __init__(self, connection : CryptolConnection) -> None: - self.connection = connection.snapshot() - name = connection.focused_module().result() - if name["module"] is None: - raise ValueError("Provided connection is not in a module") - super(CryptolModule, self).__init__(name["module"]) - - for x in self.connection.names().result(): - if 'documentation' in x: - setattr(self, x['name'], - CryptolFunctionHandle(self.connection, - x['name'], - x['type string'], - cryptoltypes.to_schema(x['type']), - x['documentation'])) - else: - setattr(self, x['name'], - CryptolFunctionHandle(self.connection, - x['name'], - x['type string'], - cryptoltypes.to_schema(x['type']))) - - -def add_cryptol_module(name : str, connection : CryptolConnection) -> None: - """Given a name for a Python module and a Cryptol connection, - establish a Python module with the given name in which all the - Cryptol names are in scope as Python proxy objects. - """ - sys.modules[name] = CryptolModule(connection) - -class CryptolContext: - _defined : Dict[str, CryptolFunctionHandle] - - def __init__(self, connection : CryptolConnection) -> None: - self.connection = connection.snapshot() - self._defined = {} - for x in self.connection.names().result(): - if 'documentation' in x: - self._defined[x['name']] = \ - CryptolFunctionHandle(self.connection, - x['name'], - x['type string'], - cryptoltypes.to_schema(x['type']), - x['documentation']) - else: - self._defined[x['name']] = \ - CryptolFunctionHandle(self.connection, - x['name'], - x['type string'], - cryptoltypes.to_schema(x['type'])) - - def __dir__(self) -> Iterable[str]: - return self._defined.keys() - - def __getattr__(self, name : str) -> Any: - if name in self._defined: - return self._defined[name] - else: - raise AttributeError() diff --git a/python/cryptol/bitvector.py b/python/cryptol/bitvector.py deleted file mode 100644 index 058ac2a9..00000000 --- a/python/cryptol/bitvector.py +++ /dev/null @@ -1,478 +0,0 @@ - -from functools import reduce -from typing import Any, List, Union, Optional, overload -from BitVector import BitVector #type: ignore - - -class BV: - """A class representing a cryptol bit vector (i.e., a sequence of bits). - - ``BV(size : int, value : int)`` will create a ``BV`` of length ``size`` and bits corresponding - to the unsigned integer representation of ``value`` (N.B., ``0 <= size <= value <= 2 ** size - 1`` - must evaluate to ``True`` or an error will be raised). - - N.B., the ``size`` and ``value`` arguments can be passed positionally or by name: - - ``BV(8,0xff) == BV(size=8, value=0xff) == BV(value=0xff, size=8)`` - - ``BV(bv : BitVector)`` will create an equivalent ``BV`` to the given ``BitVector`` value. - """ - __size : int - __value : int - - def __init__(self, size : Union[int, BitVector], value : Optional[int] = None) -> None: - """Initialize a ``BV`` from a ``BitVector`` or from size and value nonnegative integers.""" - if value is not None: - if not isinstance(size, int) or size < 0: - raise ValueError(f'`size` parameter to BV must be a nonnegative integer but was given {size!r}.') - self.__size = size - if not isinstance(value, int): - raise ValueError(f'{value!r} is not an integer value to initilize a bit vector of size {self.__size!r} with.') - self.__value = value - elif not isinstance(size, BitVector): - raise ValueError(f'BV can only be created from a single value when that value is a BitVector, but got {size!r}') - else: - self.__size = len(size) - self.__value = int(size) - if self.__value < 0 or self.__value.bit_length() > self.__size: - raise ValueError(f'{self.__value!r} is not representable as an unsigned integer with {self.__size!r} bits.') - - def hex(self) -> str: - """Return the (padded) hexadecimal string for the unsigned integer this ``BV`` represents. - - Note: padding is determined by ``self.size()``, rounding up a single digit - for widths not evenly divisible by 4.""" - hex_str_width = 2 + (self.__size // 4) + (0 if (self.__size % 4 == 0) else 1) - return format(self.__value, f'#0{hex_str_width!r}x') - - def __repr__(self) -> str: - return f"BV({self.__size!r}, {self.hex()})" - - @overload - def __getitem__(self, key : int) -> bool: - pass - @overload - def __getitem__(self, key : slice) -> 'BV': - pass - def __getitem__(self, key : Union[int, slice]) -> Union[bool, 'BV']: - """``BV`` indexing and slicing. - - :param key: If ``key`` is an integer, ``True`` is returned if the corresponding bit - is non-zero, else ``False`` is returned. If ``key`` is a ``slice`` (i.e., ``[high:low]``) - it specifies a sub-``BV`` of ``self`` corresponding to the bits from - index ``low`` up until (but not including) index ``high``. - - Examples: - - ``BV(8,0b00000010)[0] == False`` - - ``BV(8,0b00000010)[1] == True`` - - ``BV(8,0b00000010)[4:0] == BV(4,0b0010)`` - """ - if isinstance(key, int): - if key < 0 or key >= self.__size: - raise ValueError(f'{key!r} is not a valid index for {self!r}') - else: - return (self.__value & (1 << key)) != 0 - if isinstance(key, slice): - high = key.start - low = key.stop - if not isinstance(low, int): raise ValueError(f'Expected BV slice to use non-negative integer indices, but got low index of {low!r}.') - if low < 0 and low > self.__size: raise ValueError(f'Expected BV slice low index to be >= 0 and <= the BV size (i.e., {self.__size!r}) but got {low!r}.') - if not isinstance(high, int): raise ValueError(f'Expected BV slice to use non-negative integer indices, but got high index of {high!r}.') - if low > high: raise ValueError(f'BV slice low index {low!r} is larger than the high index {high!r}.') - if high > self.__size: raise ValueError(f'BV slice high index {high!r} is larger than the BV size (i.e., {self.__size!r}).') - if key.step: raise ValueError(f'BV slicing expects a step of None, but found {key.step!r}') - new_sz = high - low - return BV(new_sz, (self.__value >> low) & ((2 ** new_sz) - 1)) - else: - raise ValueError(f'{key!r} is not a valid BV index or slice.') - - def size(self) -> int: - """Size of the ``BV`` (i.e., the available "bit width").""" - return self.__size - - def widen(self, n : int) -> 'BV': - """Returns a "widened" version of ``self``, i.e. ``BV(self.size() + n, self.value())``. - - Args: - n (int): How many bits wider the returned ``BV`` should be than ``self`` (must be nonnegative). - """ - if not isinstance(n, int) or n < 0: #type: ignore - raise ValueError(f'``widen`` expects a nonnegative integer, but got {n!r}') - else: - return BV(self.__size + n, self.__value) - - def value(self) -> int: - """The unsigned integer interpretation of the ``self``.""" - return self.__value - - def __concat_single(self, other : 'BV') -> 'BV': - if isinstance(other, BV): - return BV(self.__size + other.__size, (self.__value << other.__size) + other.__value) - else: - raise ValueError(f'Cannot concat BV with {other!r}') - - def concat(self, *others : 'BV') -> 'BV': - """Concatenate the given ``BV``s to the right of ``self``. - - :param others: The BVs to concatenate onto the right side of ``self`` in order. - - Returns: - BV: a bit vector with the bits from ``self`` on the left and the bits from - ``others`` in order on the right. - """ - return reduce(lambda acc, b: acc.__concat_single(b), others, self) - - @staticmethod - def join(*bs : 'BV') -> 'BV': - """Concatenate the given ``BV``s in order. - - :param bs: The ``BV``s to concatenate in order. - - Returns: - BV: A bit vector with the bits from ``others`` in order. - """ - return reduce(lambda acc, b: acc.__concat_single(b), bs, BV(0,0)) - - def zero(self) -> 'BV': - """The zero bit vector for ``self``'s size (i.e., ``BV(self.size(), 0)``).""" - return BV(self.size() ,0) - - def to_int(self) -> int: - """Return the unsigned integer the ``BV`` represents (equivalent to ``self.value()``).""" - return self.__value - - def to_signed_int(self) -> int: - """Return the signed (i.e., two's complement) integer the ``BV`` represents.""" - if not self.msb(): - n = self.__value - else: - n = 0 - ((2 ** self.__size) - self.__value) - return n - - def msb(self) -> bool: - """Returns ``True`` if the most significant bit is 1, else returns ``False``.""" - if self.__size == 0: - raise ValueError("0-length BVs have no most significant bit.") - else: - return self[self.__size - 1] - - def lsb(self) -> bool: - """Returns ``True`` if the least significant bit is 1, else returns ``False``.""" - if self.__size == 0: - raise ValueError("0-length BVs have no least significant bit.") - else: - return self[0] - - - def __eq__(self, other : Any) -> bool: - """Returns ``True`` if ``other`` is also a ``BV`` of the same size and value, else returns ``False``.""" - if isinstance(other, BV): - return self.__size == other.__size and self.__value == other.__value - else: - return False - - def __index__(self) -> int: - """Equivalent to ``self.value()``.""" - return self.__value - - def __len__(self) -> int: - """Equivalent to ``self.size()``.""" - return self.__size - - def __bytes__(self) -> bytes: - """Returns the ``bytes`` value equivalent to ``self.value()``.""" - byte_len = (self.__size // 8) + (0 if self.__size % 8 == 0 else 1) - return self.__value.to_bytes(byte_len, 'big') - - - def split(self, size : int) -> List['BV']: - """Split ``self`` into a list of ``BV``s of length ``size``. - - :param size: Size of segments to partition ``self`` into (must evently divide ``self.size()``). - """ - if not isinstance(size, int) or size <= 0: #type: ignore - raise ValueError(f'`size` argument to splits must be a positive integer, got {size!r}') - if not self.size() % size == 0: - raise ValueError(f'{self!r} is not divisible into equal parts of size {size!r}') - mask = (1 << size) - 1 - return [BV(size, (self.__value >> (i * size)) & mask) - for i in range(self.size() // size - 1, -1, -1)] - - - def popcount(self) -> int: - """Return the number of bits set to ``1`` in ``self``.""" - return bin(self).count("1") - - @staticmethod - def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big') -> 'BV': - """Convert the given bytes ``bs`` into a ``BV``. - - :param bs: Bytes to convert to a ``BV``. - :param size, optional: Desired ``BV``'s size (must be large enough to represent ``bs``). The - default (i.e., ``None``) will result in a ``BV`` of size ``len(bs) * 8``. - :param byteorder, optional: Byte ordering ``bs`` should be interpreted as, defaults to - ``'big'``, ``little`` being the other acceptable value. Equivalent to the ``byteorder`` - parameter from Python's ``int.from_bytes``.""" - - if not isinstance(bs, bytes): - raise ValueError("from_bytes given not bytes value: {bs!r}") - - if not byteorder == 'little' and not byteorder == 'big': - raise ValueError("from_bytes given not bytes value: {bs!r}") - - if size == None: - return BV(len(bs) * 8, int.from_bytes(bs, byteorder=byteorder)) - elif isinstance(size, int) and size >= len(bs) * 8: - return BV(size, int.from_bytes(bs, byteorder=byteorder)) - else: - raise ValueError(f'from_bytes given invalid bit size {size!r} for bytes {bs!r}') - - def with_bit(self, index : int, set_bit : bool) -> 'BV': - """Return a ``BV`` identical to ``self`` but with the bit at ``index`` set to - ``1`` if ``set_bit == True``, else ``0``.""" - if index < 0 or index >= self.__size: - raise ValueError(f'{index!r} is not a valid bit index for {self!r}') - if set_bit: - mask = (1 << index) - return BV(self.__size, self.__value | mask) - else: - mask = (2 ** self.__size - 1) ^ (1 << index) - return BV(self.__size, self.__value & mask) - - - def with_bits(self, low : int, bits : 'BV') -> 'BV': - """Return a ``BV`` identical to ``self`` but with the bits from ``low`` to - ``low + bits.size() - 1`` replaced by the bits from ``bits``.""" - if not isinstance(low, int) or low < 0 or low >= self.__size: # type: ignore - raise ValueError(f'{low!r} is not a valid low bit index for {self!r}') - elif not isinstance(bits, BV): - raise ValueError(f'Expected a BV but got {bits!r}') - elif low + bits.size() > self.__size: - raise ValueError(f'{bits!r} does not fit within {self!r} when starting from low bit index {low!r}.') - else: - wider = self.size() - (low + bits.size()) - mask = (BV(bits.size(), 2 ** bits.size() - 1) << low).widen(wider) - return (self & ~mask) | (bits << low).widen(wider) - - def to_bytes(self) -> bytes: - """Convert the given ``BV`` into a python native ``bytes`` value. - - Note: equivalent to bytes(_).""" - - return self.__bytes__() - - def __mod_if_overflow(self, value : int) -> int: - n : int = value if value.bit_length() <= self.__size \ - else (value % (2 ** self.__size)) - return n - - def __add__(self, other : Union[int, 'BV']) -> 'BV': - """Addition bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - return BV( - self.__size, - self.__mod_if_overflow(self.__value + other.__value)) - else: - raise ValueError(self.__unequal_len_op_error_msg("+", other)) - elif isinstance(other, int): - return BV( - self.__size, - self.__mod_if_overflow(self.__value + other)) - else: - raise ValueError(f'Cannot add {self!r} with {other!r}.') - - def __radd__(self, other : int) -> 'BV': - if isinstance(other, int): - return BV(self.__size, self.__mod_if_overflow(self.__value + other)) - else: - raise ValueError(f'Cannot add {self!r} with {other!r}.') - - def __and__(self, other : Union['BV', int]) -> 'BV': - """Bitwise 'logical and' bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - return BV(self.__size, self.__value & other.__value) - else: - raise ValueError(self.__unequal_len_op_error_msg("&", other)) - elif isinstance(other, int): - return BV(self.__size, self.__value & other) - else: - raise ValueError(f'Cannot bitwise and {self!r} with value {other!r}.') - - def __rand__(self, other : int) -> 'BV': - if isinstance(other, int): - return BV(self.__size, self.__value & other) - else: - raise ValueError(f'Cannot bitwise and {self!r} with value {other!r}.') - - def __or__(self, other : Union['BV', int]) -> 'BV': - """Bitwise 'logical or' bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - return BV(self.__size, self.__value | other.__value) - else: - raise ValueError(self.__unequal_len_op_error_msg("|", other)) - elif isinstance(other, int): - return BV(self.__size, self.__value | other) - else: - raise ValueError(f'Cannot bitwise or {self!r} with value {other!r}.') - - def __ror__(self, other : int) -> 'BV': - if isinstance(other, int): - return BV(self.__size, self.__value | other) - else: - raise ValueError(f'Cannot bitwise or {self!r} with value {other!r}.') - - def __xor__(self, other : Union['BV', int]) -> 'BV': - """Bitwise 'logical xor' bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - return BV(self.__size, self.__value ^ other.__value) - else: - raise ValueError(self.__unequal_len_op_error_msg("^", other)) - elif isinstance(other, int): - return BV(self.__size, self.__value ^ other) - else: - raise ValueError(f'Cannot bitwise xor {self!r} with value {other!r}.') - - def __rxor__(self, other : int) -> 'BV': - if isinstance(other, int): - return BV(self.__size, self.__value ^ other) - else: - raise ValueError(f'Cannot bitwise xor {self!r} with value {other!r}.') - - - def __invert__(self) -> 'BV': - """Returns the bitwise inversion of ``self``.""" - return BV(self.__size, (1 << self.__size) - 1 - self.__value) - - @staticmethod - def __from_signed_int(size: int, val : int) -> 'BV': - excl_max = 2 ** size - if (size == 0): - return BV(0,0) - elif val >= 0: - return BV(size, val % excl_max) - else: - return BV(size, ((excl_max - 1) & ~(abs(val + 1))) % excl_max) - - @staticmethod - def from_signed_int(size: int, value : int) -> 'BV': - """Returns the ``BV`` corrsponding to the ``self.size()``-bit two's complement representation of ``value``. - - :param size: Bit width of desired ``BV``. - :param value: Integer returned ``BV`` is derived from (must be in range - ``-(2 ** (size - 1))`` to ``(2 ** (size - 1) - 1)`` inclusively). - """ - if size == 0: - raise ValueError("There are no two's complement 0-bit vectors.") - max_val = 2 ** (size - 1) - 1 - min_val = -(2 ** (size - 1)) - if value < min_val or value > max_val: - raise ValueError(f'{value!r} is not in range [{min_val!r},{max_val!r}].') - else: - return BV.__from_signed_int(size, value) - - def __sub__(self, other : Union[int, 'BV']) -> 'BV': - """Subtraction bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - if self.__size == 0: - return self - else: - return BV.__from_signed_int( - self.__size, - self.to_signed_int() - other.to_signed_int()) - else: - raise ValueError(self.__unequal_len_op_error_msg("-", other)) - elif isinstance(other, int): - self.__check_int_size(other) - if self.__size == 0: - return self - else: - return BV.__from_signed_int( - self.__size, - self.to_signed_int() - other) - else: - raise ValueError(f'Cannot subtract {other!r} from {self!r}.') - - def __rsub__(self, other : int) -> 'BV': - if isinstance(other, int): - self.__check_int_size(other) - if self.__size == 0: - return self - else: - return BV.__from_signed_int( - self.__size, - other - self.to_signed_int()) - else: - raise ValueError(f'Cannot subtract {self!r} from {other!r}.') - - - def __mul__(self, other: Union[int, 'BV']) -> 'BV': - """Multiplication bewteen ``BV``s of equal size or bewteen a ``BV`` and a nonnegative - integer whose value is expressible with the ``BV`` parameter's size.""" - if isinstance(other, BV): - if self.__size == other.__size: - return BV( - self.__size, - self.__mod_if_overflow(self.__value * other.__value)) - else: - raise ValueError(self.__unequal_len_op_error_msg("*", other)) - elif isinstance(other, int): - self.__check_int_size(other) - return BV.__from_signed_int( - self.__size, - self.__mod_if_overflow(self.__value * other)) - else: - raise ValueError(f'Cannot multiply {self!r} and {other!r}.') - - def __rmul__(self, other : int) -> 'BV': - return self.__mul__(other) - - - def __lshift__(self, other : Union[int, 'BV']) -> 'BV': - """Returns the bitwise left shift of ``self``. - - :param other: Nonnegative amount to left shift ``self`` by (resulting - ``BV``'s size is ``self.size() + int(other)``)). - """ - if isinstance(other, int) or isinstance(other, BV): - n = int(other) - if n < 0: - raise ValueError(f'Cannot left shift a negative amount (i.e, {n!r}).') - return BV(self.__size + n, self.__value << n) - else: - raise ValueError(f'Shift must be specified with an integer or BV, but got {other!r}.') - - - def __rshift__(self, other : Union[int, 'BV']) -> 'BV': - """Returns the bitwise right shift of ``self``. - - :param other: Nonnegative amount to right shift ``self`` by (resulting - ``BV``'s size is ``max(0, self.size() - int(other))``). - """ - if isinstance(other, int) or isinstance(other, BV): - n = int(other) - if n < 0: - raise ValueError(f'Cannot right shift a negative amount (i.e, {n!r}).') - return BV(max(0, self.__size - n), self.__value >> n) - else: - raise ValueError(f'Shift must be specified with an integer or BV, but got {other!r}.') - - def __check_int_size(self, val : int) -> None: - if val >= (2 ** self.__size) or val < 0: - raise ValueError(f'{val!r} is not a valid unsigned {self.__size!r}-bit value.') - - - def __unequal_len_op_error_msg(self, op : str, other : 'BV') -> str: - return f'Operator `{op}` cannot be called on BV of unequal length {self!r} and {other!r}.' diff --git a/python/cryptol/cryptoltypes.py b/python/cryptol/cryptoltypes.py deleted file mode 100644 index ee7ccbba..00000000 --- a/python/cryptol/cryptoltypes.py +++ /dev/null @@ -1,505 +0,0 @@ -from __future__ import annotations -from collections import OrderedDict -from abc import ABCMeta, abstractmethod -import base64 -from math import ceil -import BitVector #type: ignore -from cryptol.bitvector import BV - -from typing import Any, Dict, Iterable, List, NoReturn, Optional, TypeVar, Union - -from typing_extensions import Literal, Protocol - -A = TypeVar('A') - -class CryptolJSON(Protocol): - def __to_cryptol__(self, ty : CryptolType) -> Any: ... - -class CryptolCode(metaclass=ABCMeta): - def __call__(self, other : CryptolJSON) -> CryptolCode: - return CryptolApplication(self, other) - - @abstractmethod - def __to_cryptol__(self, ty : CryptolType) -> Any: ... - - -class CryptolLiteral(CryptolCode): - def __init__(self, code : str) -> None: - self._code = code - - def __to_cryptol__(self, ty : CryptolType) -> Any: - return self._code - -class CryptolApplication(CryptolCode): - def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None: - self._rator = rator - self._rands = rands - - def __to_cryptol__(self, ty : CryptolType) -> Any: - return {'expression': 'call', - 'function': to_cryptol(self._rator), - 'arguments': [to_cryptol(arg) for arg in self._rands]} - -class CryptolArrowKind: - def __init__(self, dom : CryptolKind, ran : CryptolKind): - self.domain = dom - self.range = ran - - def __repr__(self) -> str: - return f"CryptolArrowKind({self.domain!r}, {self.range!r})" - -CryptolKind = Union[Literal['Type'], Literal['Num'], Literal['Prop'], CryptolArrowKind] - -def to_kind(k : Any) -> CryptolKind: - if k == "Type": return "Type" - elif k == "Num": return "Num" - elif k == "Prop": return "Prop" - elif k['kind'] == "arrow": - return CryptolArrowKind(k['from'], k['to']) - else: - raise ValueError(f'Not a Cryptol kind: {k!r}') - -class CryptolProp: - pass - -class UnaryProp(CryptolProp): - def __init__(self, subject : CryptolType) -> None: - self.subject = subject - -class Fin(UnaryProp): - def __repr__(self) -> str: - return f"Fin({self.subject!r})" - -class Cmp(UnaryProp): - def __repr__(self) -> str: - return f"Cmp({self.subject!r})" - -class SignedCmp(UnaryProp): - def __repr__(self) -> str: - return f"SignedCmp({self.subject!r})" - -class Zero(UnaryProp): - def __repr__(self) -> str: - return f"Zero({self.subject!r})" - -class Arith(UnaryProp): - def __repr__(self) -> str: - return f"Arith({self.subject!r})" - -class Logic(UnaryProp): - def __repr__(self) -> str: - return f"Logic({self.subject!r})" - - -def to_cryptol(val : Any, cryptol_type : Optional[CryptolType] = None) -> Any: - if cryptol_type is not None: - return cryptol_type.from_python(val) - else: - return CryptolType().from_python(val) - -def fail_with(exn : Exception) -> NoReturn: - raise exn - -def is_plausible_json(val : Any) -> bool: - for ty in [bool, int, float, str]: - if isinstance(val, ty): return True - - if isinstance(val, dict): - return all(isinstance(k, str) and is_plausible_json(val[k]) for k in val) - - if isinstance(val, tuple) or isinstance(val, list): - return all(is_plausible_json(elt) for elt in val) - - return False - -class CryptolType: - def from_python(self, val : Any) -> Any: - if hasattr(val, '__to_cryptol__'): - code = val.__to_cryptol__(self) - if is_plausible_json(code): - return code - else: - raise ValueError(f"Improbable JSON from __to_cryptol__: {val!r} gave {code!r}") - # if isinstance(code, CryptolCode): - # return self.convert(code) - # else: - # raise ValueError(f"Expected Cryptol code from __to_cryptol__ on {val!r}, but got {code!r}.") - else: - return self.convert(val) - - def convert(self, val : Any) -> Any: - if isinstance(val, bool): - return val - elif isinstance(val, tuple) and val == (): - return {'expression': 'unit'} - elif isinstance(val, tuple): - return {'expression': 'tuple', - 'data': [to_cryptol(x) for x in val]} - elif isinstance(val, dict): - return {'expression': 'record', - 'data': {k : to_cryptol(val[k]) - if isinstance(k, str) - else fail_with (TypeError("Record keys must be strings")) - for k in val}} - elif isinstance(val, int): - return val - elif isinstance(val, list): - return {'expression': 'sequence', - 'data': [to_cryptol(v) for v in val]} - elif isinstance(val, bytes) or isinstance(val, bytearray): - return {'expression': 'bits', - 'encoding': 'base64', - 'width': 8 * len(val), - 'data': base64.b64encode(val).decode('ascii')} - elif isinstance(val, BitVector.BitVector): - n = int(val) - byte_width = ceil(n.bit_length()/8) - return {'expression': 'bits', - 'encoding': 'base64', - 'width': val.length(), # N.B. original length, not padded - 'data': base64.b64encode(n.to_bytes(byte_width,'big')).decode('ascii')} - elif isinstance(val, BV): - return {'expression': 'bits', - 'encoding': 'hex', - 'width': val.size(), # N.B. original length, not padded - 'data': val.hex()[2:]} - else: - raise TypeError("Unsupported value: " + str(val)) - -class Var(CryptolType): - def __init__(self, name : str, kind : CryptolKind) -> None: - self.name = name - self.kind = kind - - def __repr__(self) -> str: - return f"Var({self.name!r}, {self.kind!r})" - - - -class Function(CryptolType): - def __init__(self, dom : CryptolType, ran : CryptolType) -> None: - self.domain = dom - self.range = ran - - def __repr__(self) -> str: - return f"Function({self.domain!r}, {self.range!r})" - -class Bitvector(CryptolType): - def __init__(self, width : CryptolType) -> None: - self.width = width - - def __repr__(self) -> str: - return f"Bitvector({self.width!r})" - - def convert(self, val : Any) -> Any: - # XXX figure out what to do when width is not evenly divisible by 8 - if isinstance(val, int): - w = eval_numeric(self.width, None) - if w is not None: - return self.convert(int.to_bytes(val, int(w / 8), 'big', signed=True)) - else: - raise ValueError(f"Insufficent type information to serialize int as bitvector") - elif isinstance(val, bytearray) or isinstance(val, bytes): - return {'expression': 'bits', - 'encoding': 'base64', - 'width': eval_numeric(self.width, 8 * len(val)), - 'data': base64.b64encode(val).decode('ascii')} - elif isinstance(val, BitVector.BitVector): - return CryptolType.convert(self, val) - elif isinstance(val, BV): - return CryptolType.convert(self, val) - else: - raise ValueError(f"Not supported as bitvector: {val!r}") - -def eval_numeric(t : Any, default : A) -> Union[int, A]: - if isinstance(t, Num): - return t.number - else: - return default - - -class Num(CryptolType): - def __init__(self, number : int) -> None: - self.number = number - - def __repr__(self) -> str: - return f"Num({self.number!r})" - -class Bit(CryptolType): - def __init__(self) -> None: - pass - - def __repr__(self) -> str: - return f"Bit()" - -class Sequence(CryptolType): - def __init__(self, length : CryptolType, contents : CryptolType) -> None: - self.length = length - self.contents = contents - - def __repr__(self) -> str: - return f"Sequence({self.length!r}, {self.contents!r})" - -class Inf(CryptolType): - def __repr__(self) -> str: - return f"Inf()" - -class Integer(CryptolType): - def __repr__(self) -> str: - return f"Integer()" - -class Rational(CryptolType): - def __repr__(self) -> str: - return f"Rational()" - -class Z(CryptolType): - def __init__(self, modulus : CryptolType) -> None: - self.modulus = modulus - - def __repr__(self) -> str: - return f"Z({self.modulus!r})" - - -class Plus(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} + {self.right})" - - def __repr__(self) -> str: - return f"Plus({self.left!r}, {self.right!r})" - -class Minus(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} - {self.right})" - - def __repr__(self) -> str: - return f"Minus({self.left!r}, {self.right!r})" - -class Times(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} * {self.right})" - - def __repr__(self) -> str: - return f"Times({self.left!r}, {self.right!r})" - - -class Div(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} / {self.right})" - - def __repr__(self) -> str: - return f"Div({self.left!r}, {self.right!r})" - -class CeilDiv(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} /^ {self.right})" - - def __repr__(self) -> str: - return f"CeilDiv({self.left!r}, {self.right!r})" - -class Mod(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} % {self.right})" - - def __repr__(self) -> str: - return f"Mod({self.left!r}, {self.right!r})" - -class CeilMod(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} %^ {self.right})" - - def __repr__(self) -> str: - return f"CeilMod({self.left!r}, {self.right!r})" - -class Expt(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"({self.left} ^^ {self.right})" - - def __repr__(self) -> str: - return f"Expt({self.left!r}, {self.right!r})" - -class Log2(CryptolType): - def __init__(self, operand : CryptolType) -> None: - self.operand = operand - - def __str__(self) -> str: - return f"(lg2 {self.operand})" - - def __repr__(self) -> str: - return f"Log2({self.operand!r})" - -class Width(CryptolType): - def __init__(self, operand : CryptolType) -> None: - self.operand = operand - - def __str__(self) -> str: - return f"(width {self.operand})" - - def __repr__(self) -> str: - return f"Width({self.operand!r})" - -class Max(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"(max {self.left} {self.right})" - - def __repr__(self) -> str: - return f"Max({self.left!r}, {self.right!r})" - -class Min(CryptolType): - def __init__(self, left : CryptolType, right : CryptolType) -> None: - self.left = left - self.right = right - - def __str__(self) -> str: - return f"(min {self.left} {self.right})" - - def __repr__(self) -> str: - return f"Min({self.left!r}, {self.right!r})" - -class Tuple(CryptolType): - types : Iterable[CryptolType] - - def __init__(self, *types : CryptolType) -> None: - self.types = types - - def __repr__(self) -> str: - return "Tuple(" + ", ".join(map(str, self.types)) + ")" - -class Record(CryptolType): - def __init__(self, fields : Dict[str, CryptolType]) -> None: - self.fields = fields - - def __repr__(self) -> str: - return f"Record({self.fields!r})" - -def to_type(t : Any) -> CryptolType: - if t['type'] == 'variable': - return Var(t['name'], to_kind(t['kind'])) - elif t['type'] == 'function': - return Function(to_type(t['domain']), to_type(t['range'])) - elif t['type'] == 'bitvector': - return Bitvector(to_type(t['width'])) - elif t['type'] == 'number': - return Num(t['value']) - elif t['type'] == 'Bit': - return Bit() - elif t['type'] == 'sequence': - return Sequence(to_type(t['length']), to_type(t['contents'])) - elif t['type'] == 'inf': - return Inf() - elif t['type'] == '+': - return Plus(*map(to_type, t['arguments'])) - elif t['type'] == '-': - return Minus(*map(to_type, t['arguments'])) - elif t['type'] == '*': - return Times(*map(to_type, t['arguments'])) - elif t['type'] == '/': - return Div(*map(to_type, t['arguments'])) - elif t['type'] == '/^': - return CeilDiv(*map(to_type, t['arguments'])) - elif t['type'] == '%': - return Mod(*map(to_type, t['arguments'])) - elif t['type'] == '%^': - return CeilMod(*map(to_type, t['arguments'])) - elif t['type'] == '^^': - return Expt(*map(to_type, t['arguments'])) - elif t['type'] == 'lg2': - return Log2(*map(to_type, t['arguments'])) - elif t['type'] == 'width': - return Width(*map(to_type, t['arguments'])) - elif t['type'] == 'max': - return Max(*map(to_type, t['arguments'])) - elif t['type'] == 'min': - return Min(*map(to_type, t['arguments'])) - elif t['type'] == 'tuple': - return Tuple(*map(to_type, t['contents'])) - elif t['type'] == 'record': - return Record({k : to_type(t['fields'][k]) for k in t['fields']}) - elif t['type'] == 'Integer': - return Integer() - elif t['type'] == 'Rational': - return Rational() - elif t['type'] == 'Z': - return Z(to_type(t['modulus'])) - else: - raise NotImplementedError(f"to_type({t!r})") - -class CryptolTypeSchema: - def __init__(self, - variables : OrderedDict[str, CryptolKind], - propositions : List[Optional[CryptolProp]], # TODO complete me! - body : CryptolType) -> None: - self.variables = variables - self.propositions = propositions - self.body = body - - def __repr__(self) -> str: - return f"CryptolTypeSchema({self.variables!r}, {self.propositions!r}, {self.body!r})" - -def to_schema(obj : Any) -> CryptolTypeSchema: - return CryptolTypeSchema(OrderedDict((v['name'], to_kind(v['kind'])) - for v in obj['forall']), - [to_prop(p) for p in obj['propositions']], - to_type(obj['type'])) - -def to_prop(obj : Any) -> Optional[CryptolProp]: - if obj['prop'] == 'fin': - return Fin(to_type(obj['subject'])) - elif obj['prop'] == 'Cmp': - return Cmp(to_type(obj['subject'])) - elif obj['prop'] == 'SignedCmp': - return SignedCmp(to_type(obj['subject'])) - elif obj['prop'] == 'Zero': - return Zero(to_type(obj['subject'])) - elif obj['prop'] == 'Arith': - return Arith(to_type(obj['subject'])) - elif obj['prop'] == 'Logic': - return Logic(to_type(obj['subject'])) - else: - return None - #raise ValueError(f"Can't convert to a Cryptol prop: {obj!r}") - -def argument_types(obj : Union[CryptolTypeSchema, CryptolType]) -> List[CryptolType]: - if isinstance(obj, CryptolTypeSchema): - return argument_types(obj.body) - elif isinstance(obj, Function): - arg1 = obj.domain - args = argument_types(obj.range) - return [arg1] + args - else: - return [] diff --git a/python/cryptol/solver.py b/python/cryptol/solver.py deleted file mode 100644 index b1c8bf98..00000000 --- a/python/cryptol/solver.py +++ /dev/null @@ -1,29 +0,0 @@ -"""Cryptol solver-related definitions""" -from typing import NewType - -Solver = NewType('Solver', str) - -# Cryptol-supported SMT configurations/solvers -# (see Cryptol.Symbolic.SBV Haskell module) -CVC4: Solver = Solver("cvc4") -YICES: Solver = Solver("yices") -Z3: Solver = Solver("z3") -BOOLECTOR: Solver = Solver("boolector") -MATHSAT: Solver = Solver("mathsat") -ABC: Solver = Solver("abc") -OFFLINE: Solver = Solver("offline") -ANY: Solver = Solver("any") -SBV_CVC4: Solver = Solver("sbv-cvc4") -SBV_YICES: Solver = Solver("sbv-yices") -SBV_Z3: Solver = Solver("sbv-z3") -SBV_BOOLECTOR: Solver = Solver("sbv-boolector") -SBV_MATHSAT: Solver = Solver("sbv-mathsat") -SBV_ABC: Solver = Solver("sbv-abc") -SBV_OFFLINE: Solver = Solver("sbv-offline") -SBV_ANY: Solver = Solver("sbv-any") -W4_CVC4: Solver = Solver("w4-cvc4") -W4_YICES: Solver = Solver("w4-yices") -W4_Z3: Solver = Solver("w4-z3") -W4_BOOLECTOR: Solver = Solver("w4-boolector") -W4_MATHSAT: Solver = Solver("w4-offline") -W4_ABC: Solver = Solver("w4-any") diff --git a/python/cryptol/test/__init__.py b/python/cryptol/test/__init__.py deleted file mode 100644 index ed84c688..00000000 --- a/python/cryptol/test/__init__.py +++ /dev/null @@ -1,2 +0,0 @@ -# import the package -import cryptol.bitvector diff --git a/python/cryptol/test/test_bitvector.py b/python/cryptol/test/test_bitvector.py deleted file mode 100644 index 4d87b626..00000000 --- a/python/cryptol/test/test_bitvector.py +++ /dev/null @@ -1,447 +0,0 @@ -import unittest -import random -from cryptol.bitvector import BV -from BitVector import BitVector #type: ignore -from typing import Callable, cast - - -class BVBaseTest(unittest.TestCase): - """Base class for BV test cases.""" - - def assertBVEqual(self, b : BV, size : int, value : int) -> None: - """Assert BV `b` has the specified `size` and `value`.""" - self.assertEqual(b.size(), size) - self.assertEqual(b.value(), value) - - - def assertUnOpExpected(self, op_fn : Callable[[BV], BV], expected_fn : Callable[[BV], BV]) -> None: - """Assert `prop` holds for any BV value.""" - for width in range(0, 129): - max_val = 2 ** width - 1 - for i in range(0, 100): - b = BV(width, random.randint(0, max_val)) - # Put `b` in the assertion so we can see its value - # on failed test cases. - self.assertEqual((b, op_fn(b)), (b, expected_fn(b))) - - def assertBinOpExpected(self, op_fn : Callable[[BV, BV], BV], expected_fn : Callable[[BV, BV], BV]) -> None: - """Assert `prop` holds for any BV value.""" - for width in range(0, 129): - max_val = 2 ** width - 1 - for i in range(0, 100): - b1 = BV(width, random.randint(0, max_val)) - b2 = BV(width, random.randint(0, max_val)) - # Put `b1` and `b2` in the assertion so we can - # see its value on failed test cases. - self.assertEqual((b1,b2,op_fn(b1, b2)), (b1,b2,expected_fn(b1, b2))) - - -class BVBasicTests(BVBaseTest): - def test_constructor1(self) -> None: - b = BV(BitVector(intVal = 0, size = 8)) - self.assertBVEqual(b, 8, 0) - b = BV(BitVector(intVal = 42, size = 8)) - self.assertBVEqual(b, 8, 42) - - def test_constructor2(self) -> None: - b = BV(0,0) - self.assertBVEqual(b, 0, 0) - b = BV(value=16,size=8) - self.assertBVEqual(b, 8, 16) - b = BV(8,42) - self.assertBVEqual(b, 8, 42) - - def test_constructor_fails(self) -> None: - with self.assertRaises(ValueError): - BV(8, 256) - with self.assertRaises(ValueError): - BV(8, -1) - - def test_hex(self) -> None: - self.assertEqual(hex(BV(0,0)), "0x0") - self.assertEqual(BV(0,0).hex(), "0x0") - self.assertEqual(hex(BV(4,0)), "0x0") - self.assertEqual(BV(4,0).hex(), "0x0") - self.assertEqual(hex(BV(5,0)), "0x0") - self.assertEqual(BV(5,0).hex(), "0x00") - self.assertEqual(hex(BV(5,11)), "0xb") - self.assertEqual(BV(5,11).hex(), "0x0b") - self.assertEqual(hex(BV(8,255)), "0xff") - self.assertEqual(BV(8,255).hex(), "0xff") - self.assertEqual(hex(BV(9,255)), "0xff") - self.assertEqual(BV(9,255).hex(), "0x0ff") - - def test_repr(self) -> None: - self.assertEqual(repr(BV(0,0)), "BV(0, 0x0)") - self.assertEqual(repr(BV(9,255)), "BV(9, 0x0ff)") - - def test_int(self) -> None: - self.assertEqual(int(BV(0,0)), 0) - self.assertEqual(int(BV(9,255)), 255) - self.assertUnOpExpected( - lambda b: BV(b.size(), int(b)), - lambda b: b) - - def test_size(self) -> None: - self.assertEqual(BV(0,0).size(), 0) - self.assertEqual(BV(9,255).size(), 9) - - def test_len(self) -> None: - self.assertEqual(len(BV(0,0)), 0) - self.assertEqual(len(BV(9,255)), 9) - - def test_popcount(self) -> None: - self.assertEqual(BV(0,0).popcount(), 0) - self.assertEqual(BV(8,0).popcount(), 0) - self.assertEqual(BV(8,1).popcount(), 1) - self.assertEqual(BV(8,2).popcount(), 1) - self.assertEqual(BV(8,3).popcount(), 2) - self.assertEqual(BV(8,255).popcount(), 8) - - def test_eq(self) -> None: - self.assertEqual(BV(0,0), BV(0,0)) - self.assertEqual(BV(8,255), BV(8,255)) - self.assertTrue(BV(8,255) == BV(8,255)) - self.assertFalse(BV(8,255) == BV(8,254)) - self.assertFalse(BV(8,255) == BV(9,255)) - - def test_neq(self) -> None: - self.assertNotEqual(BV(0,0), BV(1,0)) - self.assertNotEqual(BV(0,0), 0) - self.assertNotEqual(0, BV(0,0)) - self.assertTrue(BV(0,0) != BV(1,0)) - self.assertTrue(BV(1,0) != BV(0,0)) - self.assertFalse(BV(0,0) != BV(0,0)) - self.assertTrue(BV(0,0) != 0) - self.assertTrue(0 != BV(0,0)) - - def test_widen(self) -> None: - self.assertEqual(BV(0,0).widen(8), BV(8,0)) - self.assertEqual(BV(9,255).widen(8), BV(17,255)) - - - def test_add(self) -> None: - self.assertEqual(BV(16,7) + BV(16,9), BV(16,16)) - self.assertEqual(BV(16,9) + BV(16,7), BV(16,16)) - self.assertEqual(BV(16,9) + BV(16,7) + 1, BV(16,17)) - self.assertEqual(1 + BV(16,9) + BV(16,7), BV(16,17)) - self.assertBinOpExpected( - lambda b1, b2: b1 + b2, - lambda b1, b2: BV(0,0) if b1.size() == 0 else - BV(b1.size(), (int(b1) + int(b2)) % ((2 ** b1.size() - 1) + 1))) - with self.assertRaises(ValueError): - BV(15,7) + BV(16,9) - - - def test_bitewise_and(self) -> None: - self.assertEqual(BV(0,0) & BV(0,0), BV(0,0)) - self.assertEqual(BV(8,0xff) & BV(8,0xff), BV(8,0xff)) - self.assertEqual(BV(8,0xff) & BV(8,42), BV(8,42)) - self.assertEqual(BV(16,7) & BV(16,9), BV(16,1)) - self.assertEqual(BV(16,9) & BV(16,7), BV(16,1)) - self.assertEqual(BV(16,9) & BV(16,7) & 1, BV(16,1)) - self.assertEqual(1 & BV(16,9) & BV(16,7), BV(16,1)) - self.assertUnOpExpected( - lambda b: b & 0, - lambda b: BV(b.size(), 0)) - self.assertUnOpExpected( - lambda b: b & cast(int, 2 ** b.size() - 1), - lambda b: b) - self.assertBinOpExpected( - lambda b1, b2: b1 & b2, - lambda b1, b2: BV(b1.size(), int(b1) & int(b2))) - with self.assertRaises(ValueError): - BV(15,7) & BV(16,9) - - def test_bitewise_not(self) -> None: - self.assertEqual(~BV(0,0), BV(0,0)) - self.assertEqual(~BV(1,0b0), BV(1,0b1)) - self.assertEqual(~BV(8,0x0f), BV(8,0xf0)) - self.assertEqual(~BV(10,0b0001110101), BV(10,0b1110001010)) - self.assertEqual(~~BV(10,0b0001110101), BV(10,0b0001110101)) - self.assertUnOpExpected( - lambda b: ~~b, - lambda b: b) - self.assertUnOpExpected( - lambda b: ~b & b, - lambda b: BV(b.size(), 0)) - - - def test_positional_index(self) -> None: - self.assertFalse(BV(16,0b10)[0]) - self.assertTrue(BV(16,0b10)[1]) - self.assertFalse(BV(16,0b10)[3]) - self.assertFalse(BV(8,0b10)[7]) - with self.assertRaises(ValueError): - BV(8,7)["Bad Index"] #type: ignore - with self.assertRaises(ValueError): - BV(8,7)[-1] - with self.assertRaises(ValueError): - BV(8,7)[8] - - def test_positional_slice(self) -> None: - self.assertEqual(BV(0,0)[0:0], BV(0,0)) - self.assertEqual(BV(16,0b10)[2:0], BV(2,0b10)) - self.assertEqual(BV(16,0b10)[16:0], BV(16,0b10)) - self.assertEqual(BV(16,0b1100110011001100)[16:8], BV(8,0b11001100)) - with self.assertRaises(ValueError): - BV(0,0)[2:0] - with self.assertRaises(ValueError): - BV(8,42)[0:1] - with self.assertRaises(ValueError): - BV(8,42)[9:0] - with self.assertRaises(ValueError): - BV(8,42)[8:-1] - with self.assertRaises(ValueError): - BV(8,42)[10:10] - - def test_concat(self) -> None: - self.assertEqual(BV(0,0).concat(BV(0,0)), BV(0,0)) - self.assertEqual(BV(1,0b1).concat(BV(0,0b0)), BV(1,0b1)) - self.assertEqual(BV(0,0b0).concat(BV(1,0b1)), BV(1,0b1)) - self.assertEqual(BV(1,0b1).concat(BV(1,0b0)), BV(2,0b10)) - self.assertEqual(BV(1,0b0).concat(BV(1,0b1)), BV(2,0b01)) - self.assertEqual(BV(1,0b1).concat(BV(1,0b1)), BV(2,0b11)) - self.assertEqual(BV(5,0b11111).concat(BV(3,0b000)), BV(8,0b11111000)) - self.assertEqual(BV(0,0).concat(), BV(0,0)) - self.assertEqual(BV(0,0).concat(BV(2,0b10),BV(2,0b01)), BV(4,0b1001)) - self.assertBinOpExpected( - lambda b1, b2: b1.concat(b2)[b2.size():0], - lambda b1, b2: b2) - self.assertBinOpExpected( - lambda b1, b2: b1.concat(b2)[b1.size() + b2.size():b2.size()], - lambda b1, b2: b1) - with self.assertRaises(ValueError): - BV(8,42).concat(42) #type: ignore - with self.assertRaises(ValueError): - BV(8,42).concat("Oops not a BV") #type: ignore - - def test_join(self) -> None: - self.assertEqual(BV.join(), BV(0,0)) - self.assertEqual(BV.join(*[]), BV(0,0)) - self.assertEqual(BV.join(BV(8,42)), BV(8,42)) - self.assertEqual(BV.join(*[BV(8,42)]), BV(8,42)) - self.assertEqual(BV.join(BV(0,0), BV(2,0b10),BV(3,0b110)), BV(5,0b10110)) - self.assertEqual(BV.join(*[BV(0,0), BV(2,0b10),BV(3,0b110)]), BV(5,0b10110)) - - def test_bytes(self) -> None: - self.assertEqual(bytes(BV(0,0)), b'') - self.assertEqual(bytes(BV(1,1)), b'\x01') - self.assertEqual(bytes(BV(8,255)), b'\xff') - self.assertEqual(bytes(BV(16,255)), b'\x00\xff') - - - def test_zero(self) -> None: - self.assertEqual(BV(0,0).zero(), BV(0,0)) - self.assertEqual(BV(9,255).zero(), BV(9,0)) - - def test_msb(self) -> None: - self.assertEqual(BV(8,0).msb(), False) - self.assertEqual(BV(8,1).msb(), False) - self.assertEqual(BV(8,127).msb(), False) - self.assertEqual(BV(8,128).msb(), True) - self.assertEqual(BV(8,255).msb(), True) - with self.assertRaises(ValueError): - BV(0,0).msb() - - - def test_lsb(self) -> None: - self.assertEqual(BV(8,0).lsb(), False) - self.assertEqual(BV(8,1).lsb(), True) - self.assertEqual(BV(8,127).lsb(), True) - self.assertEqual(BV(8,128).lsb(), False) - self.assertEqual(BV(8,255).lsb(), True) - with self.assertRaises(ValueError): - BV(0,0).lsb() - - def test_from_signed_int(self) -> None: - self.assertEqual(BV.from_signed_int(8,127), BV(8,127)) - self.assertEqual(BV.from_signed_int(8,-128), BV(8,0x80)) - self.assertEqual(BV.from_signed_int(8,-1), BV(8,255)) - self.assertUnOpExpected( - lambda b: b if b.size() == 0 else BV.from_signed_int(b.size(), b.to_signed_int()), - lambda b: b) - with self.assertRaises(ValueError): - BV.from_signed_int(8,128) - with self.assertRaises(ValueError): - BV.from_signed_int(8,-129) - - def test_sub(self) -> None: - self.assertEqual(BV(0,0) - BV(0,0), BV(0,0)) - self.assertEqual(BV(0,0) - 0, BV(0,0)) - self.assertEqual(0 - BV(0,0), BV(0,0)) - self.assertEqual(BV(8,5) - 3, BV(8,2)) - self.assertEqual(5 - BV(8,3), BV(8,2)) - self.assertEqual(BV(8,3) - BV(8,3), BV(8,0)) - self.assertEqual(BV(8,3) - BV(8,4), BV(8,255)) - self.assertEqual(BV(8,3) - BV(8,255), BV(8,4)) - self.assertEqual(BV(8,255) - BV(8,3), BV(8,252)) - self.assertEqual(BV(8,3) - 255, BV(8,4)) - self.assertEqual(255 - BV(8,3), BV(8,252)) - self.assertUnOpExpected( - lambda b: b - b, - lambda b: b.zero()) - self.assertUnOpExpected( - lambda b: b - BV(b.size(), 2 ** b.size() - 1), - lambda b: b + 1) - with self.assertRaises(ValueError): - BV(9,3) - BV(8,3) - with self.assertRaises(ValueError): - 256 - BV(8,3) - with self.assertRaises(ValueError): - BV(8,3) - 256 - with self.assertRaises(ValueError): - (-1) - BV(8,3) - with self.assertRaises(ValueError): - BV(8,3) - (-1) - - - def test_mul(self) -> None: - self.assertEqual(BV(8,5) * BV(8,4), BV(8,20)) - self.assertEqual(5 * BV(8,4), BV(8,20)) - self.assertEqual(4 * BV(8,5), BV(8,20)) - self.assertEqual(100 * BV(8,5), BV(8,0xf4)) - self.assertEqual(BV(8,5) * 100, BV(8,0xf4)) - self.assertUnOpExpected( - lambda b: b * 3 if b.size() >= 3 else b.zero(), - lambda b: b + b + b if b.size() >= 3 else b.zero()) - with self.assertRaises(ValueError): - BV(9,3) * BV(8,3) - with self.assertRaises(ValueError): - 256 * BV(8,3) - with self.assertRaises(ValueError): - BV(8,3) * 256 - with self.assertRaises(ValueError): - (-1) * BV(8,3) - with self.assertRaises(ValueError): - BV(8,3) * (-1) - - def test_split(self) -> None: - self.assertEqual( - BV(8,0xff).split(1), - [BV(1,0x1), - BV(1,0x1), - BV(1,0x1), - BV(1,0x1), - BV(1,0x1), - BV(1,0x1), - BV(1,0x1), - BV(1,0x1)]) - self.assertEqual( - BV(9,0b100111000).split(3), - [BV(3,0b100), - BV(3,0b111), - BV(3,0x000)]) - self.assertEqual( - BV(64,0x0123456789abcdef).split(4), - [BV(4,0x0), - BV(4,0x1), - BV(4,0x2), - BV(4,0x3), - BV(4,0x4), - BV(4,0x5), - BV(4,0x6), - BV(4,0x7), - BV(4,0x8), - BV(4,0x9), - BV(4,0xa), - BV(4,0xb), - BV(4,0xc), - BV(4,0xd), - BV(4,0xe), - BV(4,0xf)]) - with self.assertRaises(ValueError): - BV(9,3).split("4") #type: ignore - with self.assertRaises(ValueError): - BV(9,3).split(4) - - - def test_from_bytes(self) -> None: - self.assertEqual(BV.from_bytes(b''), BV(0,0)) - self.assertEqual(BV.from_bytes(b'', size=64), BV(64,0)) - self.assertEqual(BV.from_bytes(b'\x00'), BV(8,0)) - self.assertEqual(BV.from_bytes(b'\x01'), BV(8,1)) - self.assertEqual(BV.from_bytes(b'\x01', size=16), BV(16,1)) - self.assertEqual(BV.from_bytes(b'\x00\x01'), BV(16,1)) - self.assertEqual(BV.from_bytes(b'\x01\x00', byteorder='little'), BV(16,1)) - self.assertEqual(BV.from_bytes(b'\x01\x00'), BV(16,0x0100)) - self.assertEqual(BV.from_bytes(b'\x01\x00', byteorder='little'), BV(16,0x0001)) - self.assertEqual(BV.from_bytes(b'\x01\x00', size=32,byteorder='little'), BV(32,0x0001)) - - def test_to_bytes(self) -> None: - self.assertEqual(BV(0,0).to_bytes() ,b'') - self.assertEqual(BV(8,0).to_bytes() ,b'\x00') - self.assertEqual(BV(8,1).to_bytes() ,b'\x01') - self.assertEqual(BV(16,1).to_bytes(), b'\x00\x01') - - - def test_bitewise_or(self) -> None: - self.assertEqual(BV(0,0) | BV(0,0), BV(0,0)) - self.assertEqual(BV(8,0xff) | BV(8,0x00), BV(8,0xff)) - self.assertEqual(BV(8,0x00) | BV(8,0xff), BV(8,0xff)) - self.assertEqual(BV(8,0x00) | 0xff, BV(8,0xff)) - self.assertEqual(0xff | BV(8,0x00), BV(8,0xff)) - self.assertEqual(BV(8,0x00) | BV(8,42), BV(8,42)) - self.assertUnOpExpected( - lambda b: b | 0, - lambda b: b) - with self.assertRaises(ValueError): - BV(15,7) | BV(16,9) - with self.assertRaises(ValueError): - BV(8,255) | 256 - with self.assertRaises(ValueError): - 256 | BV(8,9) - with self.assertRaises(ValueError): - BV(8,255) | -1 - with self.assertRaises(ValueError): - -1 | BV(8,9) - - - def test_bitewise_xor(self) -> None: - self.assertEqual(BV(0,0) ^ BV(0,0), BV(0,0)) - self.assertEqual(BV(8,0xff) ^ BV(8,0x00), BV(8,0xff)) - self.assertEqual(BV(8,0x00) ^ BV(8,0xff), BV(8,0xff)) - self.assertEqual(BV(8,0x0f) ^ BV(8,0xff), BV(8,0xf0)) - self.assertEqual(BV(8,0xf0) ^ BV(8,0xff), BV(8,0x0f)) - self.assertUnOpExpected( - lambda b: b ^ 0, - lambda b: b) - self.assertUnOpExpected( - lambda b: b ^ ~b, - lambda b: BV(b.size(), 2 ** b.size() - 1)) - with self.assertRaises(ValueError): - BV(15,7) ^ BV(16,9) - with self.assertRaises(ValueError): - BV(8,255) ^ 256 - with self.assertRaises(ValueError): - 256 ^ BV(8,9) - with self.assertRaises(ValueError): - BV(8,255) ^ -1 - with self.assertRaises(ValueError): - -1 ^ BV(8,9) - - def test_with_bit(self) -> None: - self.assertEqual(BV(1,0).with_bit(0,True), BV(1,1)) - self.assertEqual(BV(1,1).with_bit(0,False), BV(1,0)) - self.assertEqual(BV(8,0b11001100).with_bit(0,True), BV(8,0b11001101)) - self.assertEqual(BV(8,0b11001100).with_bit(3,False), BV(8,0b11000100)) - self.assertEqual(BV(8,0b11001100).with_bit(7,False), BV(8,0b01001100)) - with self.assertRaises(ValueError): - BV(8,0b11001100).with_bit(8,False) - with self.assertRaises(ValueError): - BV(8,0b11001100).with_bit(-1,False) - - def test_with_bits(self) -> None: - self.assertEqual(BV(1,0b0).with_bits(0,BV(1,0b0)), BV(1,0b0)) - self.assertEqual(BV(1,0b0).with_bits(0,BV(1,0b1)), BV(1,0b1)) - self.assertEqual(BV(1,0b1).with_bits(0,BV(1,0b0)), BV(1,0b0)) - self.assertEqual(BV(8,0b11010101).with_bits(3,BV(3,0b101)), BV(8,0b11101101)) - self.assertEqual(BV(8,0b11010101).with_bits(5,BV(3,0b101)), BV(8,0b10110101)) - with self.assertRaises(ValueError): - BV(8,0b11000101).with_bits(-1,BV(3,0b111)) - with self.assertRaises(ValueError): - BV(8,0b11000101).with_bits(0,"bad") #type: ignore - with self.assertRaises(ValueError): - BV(8,0b11000101).with_bits(0,BV(9,0)) - with self.assertRaises(ValueError): - BV(8,0b11000101).with_bits(1,BV(8,0)) diff --git a/python/hs-test/Main.hs b/python/hs-test/Main.hs deleted file mode 100644 index e46a6b39..00000000 --- a/python/hs-test/Main.hs +++ /dev/null @@ -1,42 +0,0 @@ -module Main where - -import System.FilePath ((), takeBaseName) -import System.Directory -import Data.Traversable -import Control.Monad - -import Test.Tasty -import Test.Tasty.HUnit -import Test.Tasty.HUnit.ScriptExit -import System.Exit - -import Paths_argo_python -import Argo.PythonBindings - -main :: IO () -main = - do reqs <- getArgoPythonFile "requirements.txt" - withPython3venv (Just reqs) $ \pip python -> - do pySrc <- getArgoPythonFile "." - pip ["install", pySrc] - - thisDirectory <- getDataFileName "." - - subdirectories <- - do paths <- listDirectory thisDirectory - filterM (doesDirectoryExist . ("." )) paths - - allTests <- for subdirectories $ \dir -> - do let name = takeBaseName dir - tests <- makeScriptTests dir [mypy] - pure (testGroup ("Typechecking: " <> name) tests) - - -- Have python discover and run unit tests - (unitExitCode, unitStdOut, unitStdErr) <- - runPythonUnitTests $ testLangExecutable python - - defaultMain $ - testGroup "Tests for Python components" $ - allTests ++ - [testCase "Python Unit Tests" $ - unitExitCode @?= ExitSuccess] diff --git a/python/hs/Argo/PythonBindings.hs b/python/hs/Argo/PythonBindings.hs deleted file mode 100644 index e62643e6..00000000 --- a/python/hs/Argo/PythonBindings.hs +++ /dev/null @@ -1,6 +0,0 @@ -module Argo.PythonBindings where - -import Paths_argo_python - -getArgoPythonFile :: FilePath -> IO FilePath -getArgoPythonFile file = getDataFileName file diff --git a/python/mypy.ini b/python/mypy.ini index d9cbd32b..a7b00d36 100644 --- a/python/mypy.ini +++ b/python/mypy.ini @@ -11,14 +11,3 @@ warn_unused_ignores = True [mypy-argo.*] disallow_untyped_defs = True warn_unreachable = True - -[mypy-cryptol.*] -disallow_untyped_defs = True -warn_unreachable = True - -[mypy-saw.*] -disallow_untyped_defs = True - -[mypy-saw.llvm] -# fails for re match objects right now -warn_unreachable = False diff --git a/python/pyproject.toml b/python/pyproject.toml new file mode 100644 index 00000000..374b58cb --- /dev/null +++ b/python/pyproject.toml @@ -0,0 +1,6 @@ +[build-system] +requires = [ + "setuptools>=42", + "wheel" +] +build-backend = "setuptools.build_meta" diff --git a/python/requirements.txt b/python/requirements.txt index c9870b94..9a9081a5 100644 --- a/python/requirements.txt +++ b/python/requirements.txt @@ -1,5 +1,3 @@ -BitVector==3.4.9 - mypy==0.790 requests==2.24.0 diff --git a/python/saw/__init__.py b/python/saw/__init__.py deleted file mode 100644 index 08c41130..00000000 --- a/python/saw/__init__.py +++ /dev/null @@ -1,365 +0,0 @@ -from abc import ABCMeta, abstractmethod -from dataclasses import dataclass, field -from typing import List, Optional, Set, Union, Dict, Tuple, Any, Callable, IO -import webbrowser -import subprocess -import uuid -import os -import sys -import inspect -import posixpath -import atexit -import re - -from . import connection -from argo.connection import ServerConnection -from argo.interaction import ArgoException -from . import llvm -from . import exceptions -from . import proofscript - -__designated_connection = None # type: Optional[connection.SAWConnection] -__designated_views = [] # type: List[View] -__global_success = True # type: bool - -# Script-execution-global set of all results verified so far -__used_server_names = set([]) # type: Set[str] - - -def __fresh_server_name(hint: Optional[str] = None) -> str: - if hint is None: - hint = 'x' - name = llvm.uniquify(hint, __used_server_names) - __used_server_names.add(name) - return name - - -def __get_designated_connection() -> connection.SAWConnection: - global __designated_connection - if __designated_connection is None: - raise ValueError("There is not yet a designated connection.") - else: - return __designated_connection - - -def __set_designated_connection(conn: connection.SAWConnection) -> None: - global __designated_connection - __designated_connection = conn - - -class VerificationResult(metaclass=ABCMeta): - server_name: str - assumptions: List[Any] # really, List[VerificationResult], - contract: llvm.Contract # but mypy doesn't allow recursive types - _unique_id: uuid.UUID - - @abstractmethod - def is_success(self) -> bool: ... - - -@dataclass -class VerificationSucceeded(VerificationResult): - def __init__(self, - server_name: str, - assumptions: List[VerificationResult], - contract: llvm.Contract, - stdout: str, - stderr: str) -> None: - self.server_name = server_name - self.assumptions = assumptions - self.contract = contract - self._unique_id = uuid.uuid4() - self.stdout = stdout - self.stderr = stderr - - def is_success(self) -> bool: - return True - - -@dataclass -class VerificationFailed(VerificationResult): - exception: exceptions.VerificationError - - def __init__(self, - server_name: str, - assumptions: List[VerificationResult], - contract: llvm.Contract, - exception: exceptions.VerificationError) -> None: - self.server_name = server_name - self.assumptions = assumptions - self.contract = contract - self.exception = exception - self._unique_id = uuid.uuid4() - - def is_success(self) -> bool: - return False - - -@dataclass -class AssumptionFailed(VerificationFailed): - def __init__(self, - server_name: str, - assumptions: List[VerificationResult], - contract: llvm.Contract, - exception: exceptions.VerificationError) -> None: - super().__init__(server_name, - assumptions, - contract, - exception) - - -def connect(command_or_connection: Union[str, ServerConnection], - *, persist: bool = False) -> None: - global __designated_connection - - # Set the designated connection by starting a server process - if __designated_connection is None: - __designated_connection = \ - connection.SAWConnection(command_or_connection, persist=persist) - else: - raise ValueError("There is already a designated connection." - " Did you call `connect()` more than once?") - - # After the script quits, print the server PID - if persist: - def print_if_still_running() -> None: - if __designated_connection is not None: - try: - pid = __designated_connection.pid() - if __designated_connection.running(): - message = f"Created persistent server process: PID {pid}" - print(message) - except ProcessLookupError: - pass - atexit.register(print_if_still_running) - - -class View: - """An instance of View describes how to (potentially interactively) view - or log the results of a verification script, in real-time.""" - - def on_failure(self, failure: VerificationFailed) -> None: - """When a verification attempt fails, do this.""" - pass - - def on_success(self, success: VerificationSucceeded) -> None: - """When a verification attempt succeeds, do this.""" - pass - - def on_python_exception(self, exception: Exception) -> None: - """When some Python exception occurs, do this.""" - pass - - def on_finish_success(self) -> None: - """After all verifications are finished successfully, do this.""" - pass - - def on_finish_failure(self) -> None: - """After all verifications are finished but with some failures, - do this.""" - pass - - def on_abort(self) -> None: - """If the proof is aborted due to inability to assume a lemma, do - this.""" - pass - - -class DebugLog(View): - """A view on the verification results that logs the stdout/stderr of the - method to stdout/stderr, or specified file handles.""" - - def __init__(self, *, out: IO[str] = sys.stdout, err: IO[str] = sys.stderr) -> None: - self.out = out - self.err = err - - def on_failure(self, failure: VerificationFailed) -> None: - if self.out is not None: - print(failure.exception.stdout, file=self.out, end='') - if self.err is not None: - print(failure.exception.stderr, file=self.err, end='') - - def on_success(self, success: VerificationSucceeded) -> None: - if self.out is not None: - print(success.stdout, file=self.out, end='') - if self.err is not None: - print(success.stderr, file=self.err, end='') - - -class LogResults(View): - """A view on the verification results that logs failures and successes in a - human-readable text format to stdout, or a given file handle.""" - - def __init__(self, file: IO[str] = sys.stdout, verbose_failure: bool = False): - self.file = file - self.verbose = verbose_failure - self.successes: List[VerificationSucceeded] = [] - self.failures: List[VerificationFailed] = [] - - def format_failure(self, failure: VerificationFailed) -> str: - filename, lineno, lemma_name = self.__result_attributes(failure) - message = f"⚠️ Failed to verify: {lemma_name}" + \ - f" (defined at {filename}:{lineno}):\n{failure.exception}" - if self.verbose: - message += '\n\tstdout:\n' + '\n'.join( - '\t\t' + line for line in failure.exception.stdout.split('\n') - ) - # message += '\n\tstderr:\n' + '\n'.join( - # '\t\t' + line for line in failure.exception.stderr.split('\n') - # ) - return message - - def format_success(self, success: VerificationSucceeded) -> str: - filename, lineno, lemma_name = self.__result_attributes(success) - return (f"✅ Verified: {lemma_name}" - f" (defined at {filename}:{lineno})") - - @staticmethod - def __result_attributes(result: VerificationResult) -> Tuple[str, Union[int, str], str]: - lineno: Optional[Union[int, str]] = result.contract.definition_lineno() - if lineno is None: - lineno = "" - filename = result.contract.definition_filename() - if filename is None: - filename = "" - lemma_name = result.contract.lemma_name() - return (filename, lineno, lemma_name) - - def on_failure(self, result: VerificationFailed) -> None: - self.failures.append(result) - print(self.format_failure(result), file=self.file) - - def on_success(self, result: VerificationSucceeded) -> None: - self.successes.append(result) - print(self.format_success(result), file=self.file) - - def on_finish_success(self) -> None: - print("✅ All verified!", file=self.file) - - def on_finish_failure(self) -> None: - print("🛑 Some lemmas failed to verify.", file=self.file) - - def on_abort(self) -> None: - print("🛑 Aborting proof script.", file=self.file) - - -def view(v: View) -> None: - """Add a view to the global list of views. Future verification results will - be handed to this view, and its on_finish() handler will be called at - the end of the script.""" - global __designated_views - __designated_views.append(v) - - -def cryptol_load_file(filename: str) -> None: - __get_designated_connection().cryptol_load_file(filename) - return None - - -@dataclass -class LLVMModule: - bitcode_file: str - server_name: str - - -def llvm_load_module(bitcode_file: str) -> LLVMModule: - name = __fresh_server_name(bitcode_file) - __get_designated_connection().llvm_load_module(name, bitcode_file).result() - return LLVMModule(bitcode_file, name) - - -def llvm_verify(module: LLVMModule, - function: str, - contract: llvm.Contract, - lemmas: Optional[List[VerificationResult]] = None, - check_sat: bool = False, - script: Optional[proofscript.ProofScript] = None, - lemma_name_hint: Optional[str] = None) -> VerificationResult: - - if lemmas is None: - lemmas = [] - if script is None: - script = proofscript.ProofScript([proofscript.abc]) - - lemma_name_hint = contract.__class__.__name__ + "_" + function - name = llvm.uniquify(lemma_name_hint, __used_server_names) - __used_server_names.add(name) - - result: VerificationResult - conn = __get_designated_connection() - conn_snapshot = conn.snapshot() - - global __global_success - global __designated_views - - try: - res = conn.llvm_verify(module.server_name, - function, - [l.server_name for l in lemmas], - check_sat, - contract.to_json(), - script.to_json(), - name) - stdout = res.stdout() - stderr = res.stderr() - result = VerificationSucceeded(server_name=name, - assumptions=lemmas, - contract=contract, - stdout=stdout, - stderr=stderr) - # If the verification did not succeed... - except exceptions.VerificationError as err: - # roll back to snapshot because the current connection's - # latest result is now a verification exception! - __set_designated_connection(conn_snapshot) - conn = __get_designated_connection() - # Assume the verification succeeded - try: - conn.llvm_assume(module.server_name, - function, - contract.to_json(), - name).result() - result = VerificationFailed(server_name=name, - assumptions=lemmas, - contract=contract, - exception=err) - # If something stopped us from even **assuming**... - except exceptions.VerificationError as err: - __set_designated_connection(conn_snapshot) - result = AssumptionFailed(server_name=name, - assumptions=lemmas, - contract=contract, - exception=err) - # If something else went wrong... - except Exception as err: - __global_success = False - for view in __designated_views: - view.on_python_exception(err) - raise err from None - - # Log or otherwise process the verification result - for view in __designated_views: - if isinstance(result, VerificationSucceeded): - view.on_success(result) - elif isinstance(result, VerificationFailed): - view.on_failure(result) - - # Note when any failure occurs - __global_success = __global_success and result.is_success() - - # Abort the proof if we failed to assume a failed verification, otherwise - # return the result of the verification - if isinstance(result, AssumptionFailed): - raise result.exception from None - - return result - - -@atexit.register -def script_exit() -> None: - global __designated_views - for view in __designated_views: - if __global_success: - view.on_finish_success() - else: - view.on_finish_failure() diff --git a/python/saw/commands.py b/python/saw/commands.py deleted file mode 100644 index e316d381..00000000 --- a/python/saw/commands.py +++ /dev/null @@ -1,84 +0,0 @@ -import argo.interaction -from argo.interaction import HasProtocolState -from . import exceptions - -from typing import Any, List - -class SAWCommand(argo.interaction.Command): - def process_error(self, ae : argo.interaction.ArgoException) -> Exception: - return exceptions.make_saw_exception(ae) - -class CryptolLoadFile(SAWCommand): - def __init__(self, connection : HasProtocolState, filename : str) -> None: - super(CryptolLoadFile, self).__init__( - 'SAW/Cryptol/load file', - {'file': filename}, - connection - ) - - def process_result(self, _res : Any) -> Any: - return None - -class CryptolLoadModule(SAWCommand): - def __init__(self, connection : HasProtocolState, module_name : str) -> None: - super(CryptolLoadModule, self).__init__( - 'SAW/Cryptol/load module', - {'module': module_name}, - connection - ) - - def process_result(self, _res : Any) -> Any: - return None - -class LLVMLoadModule(SAWCommand): - def __init__(self, connection : HasProtocolState, - name : str, - bitcode_file : str) -> None: - super(LLVMLoadModule, self).__init__( - 'SAW/LLVM/load module', - {'name': name, 'bitcode file': bitcode_file}, - connection - ) - - def process_result(self, _res : Any) -> Any: - return None - -class LLVMAssume(SAWCommand): - def __init__( - self, - connection : HasProtocolState, - module : str, - function : str, - setup : Any, - lemma_name : str) -> None: - params = {'module': module, - 'function': function, - 'contract': setup, - 'lemma name': lemma_name} - super(LLVMAssume, self).__init__('SAW/LLVM/assume', params, connection) - - def process_result(self, _res : Any) -> Any: - return None - -class LLVMVerify(SAWCommand): - def __init__( - self, - connection : HasProtocolState, - module : str, - function : str, - lemmas : List[str], - check_sat : bool, - setup : Any, - script : str, - lemma_name : str) -> None: - params = {'module': module, - 'function': function, - 'lemmas': lemmas, - 'check sat': check_sat, - 'contract': setup, - 'script': script, - 'lemma name': lemma_name} - super(LLVMVerify, self).__init__('SAW/LLVM/verify', params, connection) - - def process_result(self, _res : Any) -> Any: - return None diff --git a/python/saw/connection.py b/python/saw/connection.py deleted file mode 100644 index 81883184..00000000 --- a/python/saw/connection.py +++ /dev/null @@ -1,82 +0,0 @@ -from __future__ import annotations - -import argo -import argo.connection as ac -import argo.interaction -from saw.commands import * - -from typing import Optional, Union, Any, List - - -def connect(command: str, cryptol_path: Optional[str] = None, *, persist: bool = False) -> SAWConnection: - return SAWConnection(command, persist=persist) - - -class SAWConnection: - """A representation of a current user state in a session with SAW.""" - - most_recent_result: Optional[argo.interaction.Interaction] - - def __init__(self, - command_or_connection: Union[str, ac.ServerConnection], - *, persist: bool = False) -> None: - self.most_recent_result = None - self.persist = persist - if isinstance(command_or_connection, str): - self.proc = ac.DynamicSocketProcess(command_or_connection, persist=self.persist) - self.server_connection = ac.ServerConnection(self.proc) - else: - self.server_connection = command_or_connection - - def pid(self) -> Optional[int]: - """Return the PID of the running server process.""" - return self.proc.pid() - - def running(self) -> bool: - """Return whether the underlying server process is still running.""" - return self.proc.running() - - def snapshot(self) -> SAWConnection: - """Return a ``SAWConnection`` that has the same process and state as - the current connection. The new connection's state will be - independent of the current state. - """ - copy = SAWConnection(self.server_connection) - copy.most_recent_result = self.most_recent_result - return copy - - def protocol_state(self) -> Any: - if self.most_recent_result is None: - return None - else: - return self.most_recent_result.state() - - # Protocol messages - def cryptol_load_file(self, filename: str) -> argo.interaction.Command: - self.most_recent_result = CryptolLoadFile(self, filename) - return self.most_recent_result - - def llvm_load_module(self, name: str, bitcode_file: str) -> argo.interaction.Command: - self.most_recent_result = LLVMLoadModule(self, name, bitcode_file) - return self.most_recent_result - - def llvm_verify(self, - module: str, - function: str, - lemmas: List[str], - check_sat: bool, - contract: Any, - script: Any, - lemma_name: str) -> argo.interaction.Command: - self.most_recent_result = \ - LLVMVerify(self, module, function, lemmas, check_sat, contract, script, lemma_name) - return self.most_recent_result - - def llvm_assume(self, - module: str, - function: str, - contract: Any, - lemma_name: str) -> argo.interaction.Command: - self.most_recent_result = \ - LLVMAssume(self, module, function, contract, lemma_name) - return self.most_recent_result diff --git a/python/saw/dashboard.py b/python/saw/dashboard.py deleted file mode 100644 index d47cc9a3..00000000 --- a/python/saw/dashboard.py +++ /dev/null @@ -1,243 +0,0 @@ -import requests -import uuid -from typing import Dict, Optional -import subprocess -import os -import sys -from . import View, VerificationResult, VerificationFailed, VerificationSucceeded - -MYXINE_PORT = 1123 - -# Loading SVG is licensed for free reuse from https://icons8.com/preloaders/ -LOADING_SVG = \ - """ - - - - - - - - - - - - - - """ - - -def serve_self_refreshing(path: str, title: str, content: str) -> None: - url = 'http://localhost:' + str(MYXINE_PORT) + '/' + path.strip('/') - requests.post(url=url, - params={ - 'title': title, - # 'refresh': 'set', - }, - data=content.encode("utf-8")) - - -class Dashboard(View): - __results: Dict[uuid.UUID, VerificationResult] - __path: str - __disconnected: bool = False - __python_exception: Optional[Exception] = None - - def on_failure(self, failure: VerificationFailed) -> None: - self.__add_result__(failure) - self.__update_dashboard__(False) - - def on_success(self, success: VerificationSucceeded) -> None: - self.__add_result__(success) - self.__update_dashboard__(False) - - def on_finish_failure(self) -> None: - self.__update_dashboard__(True) - - def on_finish_success(self) -> None: - self.__update_dashboard__(True) - - def on_python_exception(self, exception: Exception) -> None: - self.__python_exception = exception - self.__update_dashboard__(True) - - def __init__(self, *, path: str) -> None: - self.__results = {} - self.__path = path - self.__update_dashboard__(False) - if not self.__disconnected: - print(f"Dashboard: http://localhost:{MYXINE_PORT}/{path}", - file=sys.stderr) - - def __add_result__(self, result: VerificationResult) -> None: - self.__results[result._unique_id] = result - - def dot_graph(self) -> str: - out = "digraph { \n" - for _, result in self.__results.items(): - # Determine the node color - if result.is_success(): - color = "green" - bgcolor = "lightgreen" - else: - color = "red" - bgcolor = "lightpink" - # Determine the node attributes - node_attrs: Dict[str, str] = { - 'label': result.contract.__class__.__name__, - 'color': color, - 'bgcolor': bgcolor, - 'fontname': "monospace", - 'shape': 'rect', - 'penwidth': '2', - } - # Render the attributes - node_attr_string = "" - for key, val in node_attrs.items(): - node_attr_string += key + " = \"" + val + "\"; " - # Render this node line - out += ' "' + str(result._unique_id) \ - + '" [' + node_attr_string.rstrip('; ') + "];\n" - # Render each of the assumption edges - for assumption in result.assumptions[:]: - edge_attrs: Dict[str, str] = { - 'penwidth': '2', - 'arrowType': 'open', - } - edge_attr_string = "" - for key, val in edge_attrs.items(): - edge_attr_string += key + " = \"" + val + "\"; " - out += ' "' \ - + str(assumption._unique_id) \ - + '" -> "' \ - + str(result._unique_id) \ - + '" [' + edge_attr_string.rstrip('; ') + '];\n' - out += "}" - # print(out) - return out - - def svg_graph(self) -> str: - # Generate a GraphViz DOT representation - dot_repr = self.dot_graph() - # Write out & render the DOT file and open it in a web browser - svg = subprocess.check_output(["dot", "-T", "svg"], - input=dot_repr, - text=True) - cleaned = [] - lines = svg.split('\n').__iter__() - for line in lines: - if line.startswith(' str: - # Generate an HTML representation of all the errors so far - out = "" - if not self.all_ok(): - out += '
' - out += '

Errors:

' - for _, result in self.__results.items(): - if isinstance(result, VerificationFailed): - out += '

' - out += '' + result.contract.__class__.__name__ + ': ' - out += '' - out += '

' + str(result.exception) + '
' - out += '' - out += '

' - if self.__python_exception is not None: - out += '

' - out += 'Script Exception (see terminal for stack trace): ' - out += '' - out += '

' + str(self.__python_exception.__repr__()) + '
' - out += '' - out += '

' - out += '
' - return out - - def dashboard_html(self, qed_called: bool) -> str: - progress: str - progress = '
' - if qed_called: - if self.all_ok(): - progress += \ - '✅ ' \ - '(successfully verified!)' - elif self.__python_exception is None: - progress += \ - '🚫 ' \ - '(failed to verify)' - else: - progress += \ - '🛑 ' \ - '(exception in script)' - else: - progress += LOADING_SVG \ - + '
' \ - '(running...)' - progress += "
" - proof_name: str = os.path.basename(self.__path) - return \ - '

' \ - + proof_name \ - + """

""" \ - + self.svg_graph() \ - + "
" \ - + progress \ - + self.errors_html() \ - + "
" - - def __update_dashboard__(self, qed_called: bool) -> None: - if not self.__disconnected: - try: - serve_self_refreshing(self.__path, - os.path.basename(self.__path), - self.dashboard_html(qed_called)) - except Exception as e: - print(f"Dashboard error: can't connect to server: {e}", - file=sys.stderr) - self.__disconnected = True - - def all_ok(self) -> bool: - # Iterate through all lemmata to determine if everything is okay - # Builds a graph of all dependencies - if self.__python_exception is not None: - return False - ok = True - for _, result in self.__results.items(): - if not result.is_success(): - ok = False - return ok - -# # Set up the dashboard path -# if designated_dashboard_path is None: -# if dashboard_path is None: -# current_frame = inspect.currentframe() -# if current_frame is None: -# raise ValueError("Cannot automatically assign a dashboard URL" -# " outside a file; use the explicit option" -# " `dashboard_path = \"...\"` when calling " -# "`connect()`") -# else: -# f_back = current_frame.f_back -# if f_back is not None: -# filename = os.path.realpath(inspect.getfile(f_back)) -# dashboard_path = \ -# re.sub(r'\.py$', '', -# posixpath.join(*filename.split(os.path.sep))) \ -# .replace('^/', '') -# designated_dashboard_path = dashboard_path -# else: -# raise ValueError("There is already a designated dashboard URL." -# " Did you call `connect()` more than once?") diff --git a/python/saw/exceptions.py b/python/saw/exceptions.py deleted file mode 100644 index 4d24c1f1..00000000 --- a/python/saw/exceptions.py +++ /dev/null @@ -1,99 +0,0 @@ -from abc import ABC, abstractmethod -from itertools import chain -from typing import Dict, Any, List, Iterable, Type -from argo.interaction import ArgoException - - -class SAWException(Exception): - data: Dict[str, Any] - code: int - stdout: str - stderr: str - - def __init__(self, ae: ArgoException) -> None: - super().__init__(ae.message) - self.data = ae.data - self.code = ae.code - self.stdout = ae.stdout - self.stderr = ae.stderr - - # The exception gets fields for each data field in the ArgoException - def __getattr__(self, attr: str) -> Any: - self.data.get(attr) - - def __dir__(self) -> Iterable[str]: - return chain(super().__dir__(), [str(k) for k in self.data.keys()]) - - def __str__(self) -> str: - lines: List[str] = [] - for k, v in self.data.items(): - lines.append(f"{k}: {v}") - return '\n'.join(lines) - - -def make_saw_exception(ae: ArgoException) -> SAWException: - """Convert an ArgoException to its corresponding SAWException, failing with - the original ArgoException if the code for this ArgoException does not - correspond to a SAWException. - """ - specific_exception_class = error_code_table.get(ae.code) - if specific_exception_class is not None: - return specific_exception_class(ae) - else: - raise ae - -# Server value errors: -class ServerValueError(SAWException): pass -class NoServerValue(ServerValueError): pass -class NotACryptolEnvironment(ServerValueError): pass -class NotAnLLVMModule(ServerValueError): pass -class NotAnLLVMSetupScript(ServerValueError): pass -class NotAnLLVMSetupValue(ServerValueError): pass -class NotAnLLVMMethodSpecification(ServerValueError): pass -class NotAnLLVMMethodSpecIR(ServerValueError): pass -class NotAJVMClass(ServerValueError): pass -class NotAJVMMethodSpecIR(ServerValueError): pass -class NotASimpset(ServerValueError): pass -class NotATerm(ServerValueError): pass - -# Setup errors: -class SetupError(SAWException): pass -class NotSettingUpCryptol(SetupError): pass -class NotSettingUpCrucibleLLVM(SetupError): pass -class NotAtTopLevel(SetupError): pass - -# Loading errors: -class LoadingError(SAWException): pass -class CantLoadLLVMModule(LoadingError): pass - -# Verification errors: -class VerificationError(SAWException): pass - -# Cryptol errors: -class CryptolError(SAWException): pass - -# The canonical mapping from Argo error codes to SAW exceptions: -error_code_table : Dict[int, Type[SAWException]] = { - # Server value errors: - 10000: NoServerValue, - 10010: NotACryptolEnvironment, - 10020: NotAnLLVMModule, - 10030: NotAnLLVMSetupScript, - 10040: NotAnLLVMSetupValue, - 10040: NotAnLLVMMethodSpecification, - 10050: NotAnLLVMMethodSpecIR, - 10060: NotASimpset, - 10070: NotATerm, - 10080: NotAJVMClass, - 10090: NotAJVMMethodSpecIR, - # Setup errors: - 10100: NotSettingUpCryptol, - 10110: NotSettingUpCrucibleLLVM, - 10120: NotAtTopLevel, - # Loading errors: - 10200: CantLoadLLVMModule, - # Verification errors: - 10300: VerificationError, - # Cryptol errors: - 11000: CryptolError, -} diff --git a/python/saw/llvm.py b/python/saw/llvm.py deleted file mode 100644 index 21a5d7fc..00000000 --- a/python/saw/llvm.py +++ /dev/null @@ -1,384 +0,0 @@ -from abc import ABCMeta, abstractmethod -from cryptol import cryptoltypes -from saw.llvm_types import LLVMType -from dataclasses import dataclass, field -import pprint -import re -from typing import Any, List, Optional, Set, Union -from typing_extensions import Literal -import inspect -import uuid - -class SetupVal(metaclass=ABCMeta): - """Represent a ``SetupValue`` in SawScript, which "corresponds to - values that can occur during symbolic execution, which includes both 'Term' - values, pointers, and composite types consisting of either of these - (both structures and arrays)." - """ - @abstractmethod - def to_json(self) -> Any: - """JSON representation for this ``SetupVal`` (i.e., how it is represented in expressions, etc). - - N.B., should be a JSON object with a ``'setup value'`` field with a unique tag which the - server will dispatch on to then interpret the rest of the JSON object.``""" - pass - -class NamedSetupVal(SetupVal): - """Represents those ``SetupVal``s which are a named reference to some value, e.e., a variable - or reference to allocated memory.""" - @abstractmethod - def to_init_json(self) -> Any: - """JSON representation with the information for those ``SetupVal``s which require additional - information to initialize/allocate them vs that which is required later to reference them. - - I.e., ``.to_json()`` will be used to refer to such ``SetupVal``s in expressions, and - ``.to_init_json() is used to initialize/allocate them.`` - """ - pass - -class CryptolTerm(SetupVal): - expression : cryptoltypes.CryptolJSON - - def __init__(self, code : Union[str, cryptoltypes.CryptolJSON]): - if isinstance(code, str): - self.expression = cryptoltypes.CryptolLiteral(code) - else: - self.expression = code - - def __call__(self, *args : cryptoltypes.CryptolJSON) -> 'CryptolTerm': - out_term = self.expression - for a in args: - out_term = cryptoltypes.CryptolApplication(out_term, a) - - return CryptolTerm(out_term) - - def __repr__(self) -> str: - return f"CryptolTerm({self.expression!r})" - - def to_json(self) -> Any: - return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)} - - def __to_cryptol__(self, ty : Any) -> Any: - return self.expression.__to_cryptol__(ty) - -class FreshVar(NamedSetupVal): - __name : Optional[str] - - def __init__(self, spec : 'Contract', type : LLVMType, suggested_name : Optional[str] = None) -> None: - self.__name = suggested_name - self.spec = spec - self.type = type - - def __to_cryptol__(self, ty : Any) -> Any: - return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty) - - def to_init_json(self) -> Any: - #FIXME it seems we don't actually use two names ever... just the one...do we actually need both? - name = self.name() - return {"server name": name, - "name": name, - "type": self.type.to_json()} - - def name(self) -> str: - if self.__name is None: - self.__name = self.spec.get_fresh_name() - return self.__name - - def to_json(self) -> Any: - return {'setup value': 'named', 'name': self.name()} - - def __gt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: - gt = CryptolTerm("(>)") - return gt(self, other) - - def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm: - lt = CryptolTerm("(<)") - return lt(self, other) - - -class Allocated(NamedSetupVal): - name : Optional[str] - - def __init__(self, spec : 'Contract', type : LLVMType, *, mutable : bool = True) -> None: - self.name = None - self.spec = spec - self.type = type - self.mutable = mutable - - def to_init_json(self) -> Any: - if self.name is None: - self.name = self.spec.get_fresh_name() - return {"server name": self.name, - "type": self.type.to_json(), - "mutable": self.mutable, - "alignment": None} - - def to_json(self) -> Any: - if self.name is None: - self.name = self.spec.get_fresh_name() - return {'setup value': 'named', 'name': self.name} - -class StructVal(SetupVal): - fields : List[SetupVal] - - def __init__(self, fields : List[SetupVal]) -> None: - self.fields = fields - - def to_json(self) -> Any: - return {'setup value': 'struct', 'fields': [fld.to_json() for fld in self.fields]} - -name_regexp = re.compile('^(?P.*[^0-9])?(?P[0-9]+)?$') - -def next_name(x : str) -> str: - match = name_regexp.match(x) - if match is None: - return 'x' - prefix, number = match.group('prefix', 'number') - - if prefix is None: - prefix = 'x' - if number is None: - next_number = 0 - else: - next_number = int(number) + 1 - return f'{prefix}{next_number}' - - -def uniquify(x : str, used : Set[str]) -> str: - while x in used: - x = next_name(x) - return x - - -class PointsTo: - def __init__(self, pointer : SetupVal, target : SetupVal) -> None: - self.pointer = pointer - self.target = target - - def to_json(self) -> Any: - return {"pointer": self.pointer.to_json(), - "points to": self.target.to_json()} - - -class Condition: - def __init__(self, condition : CryptolTerm) -> None: - self.cryptol_term = condition - - def to_json(self) -> Any: - return cryptoltypes.to_cryptol(self.cryptol_term) - - -@dataclass -class State: - contract : 'Contract' - fresh : List[FreshVar] = field(default_factory=list) - conditions : List[Condition] = field(default_factory=list) - allocated : List[Allocated] = field(default_factory=list) - points_to : List[PointsTo] = field(default_factory=list) - - def to_json(self) -> Any: - return {'variables': [v.to_init_json() for v in self.fresh], - 'conditions': [c.to_json() for c in self.conditions], - 'allocated': [a.to_init_json() for a in self.allocated], - 'points to': [p.to_json() for p in self.points_to] - } - -ContractState = \ - Union[Literal['pre'], - Literal['post'], - Literal['done']] - -@dataclass -class Void: - def to_json(self) -> Any: - return None - -void = Void() - -@dataclass -class VerifyResult: - contract : 'Contract' - lemma_name : str - -# Lemma names are generated deterministically with respect to a -# particular Python execution trace. This means that re-running the -# same script will be fast when using caching, but REPL-style usage -# will be slow, invalidating the cache at each step. We should be -# smarter about this. -used_lemma_names = set([]) # type: Set[str] - -class Contract: - __used_names : Set[str] - - __state : ContractState = 'pre' - - __pre_state : State - __post_state : State - - __returns : Optional[Union[SetupVal, Void]] - - __arguments : Optional[List[SetupVal]] - - __definition_lineno : Optional[int] - __definition_filename : Optional[str] - __unique_id : uuid.UUID - __cached_json : Optional[Any] - - def __init__(self) -> None: - self.__pre_state = State(self) - self.__post_state = State(self) - self.__used_names = set() - self.__arguments = None - self.__returns = None - self.__unique_id = uuid.uuid4() - self.__cached_json = None - frame = inspect.currentframe() - if frame is not None and frame.f_back is not None: - self.__definition_lineno = frame.f_back.f_lineno - self.__definition_filename = frame.f_back.f_code.co_filename - else: - self.__definition_lineno = None - self.__definition_filename = None - - # To be overridden by users - def specification(self) -> None: - pass - - def execute_func(self, *args : SetupVal) -> None: - """Denotes the end of the precondition specification portion of this ``Contract``, records that - the function is executed with arguments ``args``, and denotes the beginning of the postcondition - portion of this ``Contract``.""" - if self.__arguments is not None: - raise ValueError("The function has already been called once during the specification.") - elif self.__state is not 'pre': - raise ValueError("Contract state expected to be 'pre', but found {self.__state!r} (has `execute_func` already been called for this contract?).") - else: - self.__arguments = [arg for arg in args] - self.__state = 'post' - - def get_fresh_name(self, hint : str = 'x') -> str: - new_name = uniquify(hint, self.__used_names) - self.__used_names.add(new_name) - return new_name - - def fresh_var(self, type : LLVMType, suggested_name : Optional[str] = None) -> FreshVar: - """Declares a fresh variable of type ``type`` (with name ``suggested_name`` if provided and available).""" - fresh_name = self.get_fresh_name('x' if suggested_name is None else self.get_fresh_name(suggested_name)) - v = FreshVar(self, type, fresh_name) - if self.__state == 'pre': - self.__pre_state.fresh.append(v) - elif self.__state == 'post': - self.__post_state.fresh.append(v) - else: - raise Exception("wrong state") - return v - - def alloc(self, type : LLVMType, *, read_only : bool = False, points_to : Optional[SetupVal] = None) -> SetupVal: - """Allocates a pointer of type ``type``. - - If ``read_only == True`` then the allocated memory is immutable. - - If ``points_to != None``, it will also be asserted that the allocated memory contains the - value specified by ``points_to``. - - :returns A pointer of the proper type to the allocated region.""" - a = Allocated(self, type, mutable = not read_only) - if self.__state == 'pre': - self.__pre_state.allocated.append(a) - elif self.__state == 'post': - self.__post_state.allocated.append(a) - else: - raise Exception("wrong state") - - if points_to is not None: - self.points_to(a, points_to) - - return a - - def points_to(self, pointer : SetupVal, target : SetupVal) -> None: - pt = PointsTo(pointer, target) - if self.__state == 'pre': - self.__pre_state.points_to.append(pt) - elif self.__state == 'post': - self.__post_state.points_to.append(pt) - else: - raise Exception("wrong state") - - def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: - if not isinstance(proposition, CryptolTerm): - condition = Condition(CryptolTerm(proposition)) - else: - condition = Condition(proposition) - if self.__state == 'pre': - self.__pre_state.conditions.append(condition) - elif self.__state == 'post': - self.__post_state.conditions.append(condition) - else: - raise Exception("wrong state") - - def returns(self, val : Union[Void,SetupVal]) -> None: - if self.__state == 'post': - if self.__returns is None: - self.__returns = val - else: - raise ValueError("Return value already specified") - else: - raise ValueError("Not in postcondition") - - def lemma_name(self, hint : Optional[str] = None) -> str: - if hint is None: - hint = self.__class__.__name__ - - name = uniquify('lemma_' + hint, used_lemma_names) - - used_lemma_names.add(name) - - return name - - def definition_lineno(self) -> Optional[int]: - return self.__definition_lineno - - def definition_filename(self) -> Optional[str]: - return self.__definition_filename - - def to_json(self) -> Any: - if self.__cached_json is not None: - return self.__cached_json - else: - if self.__state != 'pre': - raise Exception(f'Internal error: wrong contract state -- expected \'pre\', but got: {self.__state!r}') - - self.specification() - - if self.__state != 'post': - raise Exception(f'Internal error: wrong contract state -- expected \'post\', but got: {self.__state!r}') - - self.__state = 'done' - - if self.__returns is None: - raise Exception("forgot return") - - self.__cached_json = \ - {'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], - 'pre conds': [c.to_json() for c in self.__pre_state.conditions], - 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], - 'pre points tos': [pt.to_json() for pt in self.__pre_state.points_to], - 'argument vals': [a.to_json() for a in self.__arguments] if self.__arguments is not None else [], - 'post vars': [v.to_init_json() for v in self.__post_state.fresh], - 'post conds': [c.to_json() for c in self.__post_state.conditions], - 'post allocated': [a.to_init_json() for a in self.__post_state.allocated], - 'post points tos': [pt.to_json() for pt in self.__post_state.points_to], - 'return val': self.__returns.to_json()} - - return self.__cached_json - - - -# FIXME Is `Any` too permissive here -- can we be a little more precise? -def cryptol(data : Any) -> 'CryptolTerm': - """Returns a ``CryptolTerm`` wrapper around ``data``.""" - return CryptolTerm(data) - -def struct(*fields : SetupVal) -> StructVal: - """Returns a ``StructVal`` with fields ``fields``.""" - return StructVal(list(fields)) diff --git a/python/saw/llvm_types.py b/python/saw/llvm_types.py deleted file mode 100644 index b02ac40f..00000000 --- a/python/saw/llvm_types.py +++ /dev/null @@ -1,60 +0,0 @@ -from abc import ABCMeta, abstractmethod -from typing import Any - -class LLVMType(metaclass=ABCMeta): - @abstractmethod - def to_json(self) -> Any: pass - -class LLVMIntType(LLVMType): - def __init__(self, width : int) -> None: - self.width = width - - def to_json(self) -> Any: - return {'type': 'primitive type', 'primitive': 'integer', 'size': self.width} - -class LLVMArrayType(LLVMType): - def __init__(self, elemtype : 'LLVMType', size : int) -> None: - self.size = size - self.elemtype = elemtype - - def to_json(self) -> Any: - return { 'type': 'array', - 'element type': self.elemtype.to_json(), - 'size': self.size } - -class LLVMPointerType(LLVMType): - def __init__(self, points_to : 'LLVMType') -> None: - self.points_to = points_to - - def to_json(self) -> Any: - return {'type': 'pointer', 'points to': self.points_to.to_json()} - -class LLVMAliasType(LLVMType): - def __init__(self, name : str) -> None: - self.name = name - - def to_json(self) -> Any: - return {'type': 'type alias', - 'alias of': self.name} - - -################################################## -# Convenient helpers with intuitive/short names # -################################################## - -i8 = LLVMIntType(8) -i16 = LLVMIntType(16) -i32 = LLVMIntType(32) -i64 = LLVMIntType(64) - -def array(size : int, ty : 'LLVMType') -> 'LLVMArrayType': - """``[size x ty]``, i.e. an array of ``size`` elements of type ``ty``.""" - return LLVMArrayType(ty, size) - -def ptr(ty : 'LLVMType') -> 'LLVMPointerType': - """``ty*``, i.e. a pointer to a value of type ``ty``.""" - return LLVMPointerType(ty) - -def alias(name : str) -> 'LLVMAliasType': - """An LLVM type alias (i.e., name).""" - return LLVMAliasType(name) diff --git a/python/saw/proofscript.py b/python/saw/proofscript.py deleted file mode 100644 index 7c3c11e7..00000000 --- a/python/saw/proofscript.py +++ /dev/null @@ -1,93 +0,0 @@ -from abc import ABCMeta, abstractmethod -from typing import Any, List - -class Prover(metaclass=ABCMeta): - @abstractmethod - def to_json(self) -> Any: pass - -class ABC(Prover): - def to_json(self) -> Any: - return { "name": "abc" } - -class RME(Prover): - def to_json(self) -> Any: - return { "name": "rme" } - -class UnintProver(Prover): - def __init__(self, name : str, unints : List[str]) -> None: - self.name = name - self.unints = unints - - def to_json(self) -> Any: - return { "name": self.name, "uninterpreted functions": self.unints } - -class CVC4(UnintProver): - def __init__(self, unints : List[str]) -> None: - super().__init__("cvc4", unints) - -class Yices(UnintProver): - def __init__(self, unints : List[str]) -> None: - super().__init__("yices", unints) - -class Z3(UnintProver): - def __init__(self, unints : List[str]) -> None: - super().__init__("z3", unints) - -class ProofTactic(metaclass=ABCMeta): - @abstractmethod - def to_json(self) -> Any: pass - -class UseProver(ProofTactic): - def __init__(self, prover : Prover) -> None: - self.prover = prover - - def to_json(self) -> Any: - return { "tactic": "use prover", - "prover": self.prover.to_json() } - -class Unfold(ProofTactic): - def __init__(self, names : List[str]) -> None: - self.names = names - - def to_json(self) -> Any: - return { "tactic": "unfold", "names": self.names } - -class EvaluateGoal(ProofTactic): - def __init__(self, names : List[str]) -> None: - self.names = names - - def to_json(self) -> Any: - return { "tactic": "evaluate goal", "names": self.names } - -# TODO: add "simplify" - -class AssumeUnsat(ProofTactic): - def to_json(self) -> Any: - return { "tactic": "assume unsat" } - -class BetaReduceGoal(ProofTactic): - def to_json(self) -> Any: - return { "tactic": "beta reduce goal" } - -class Trivial(ProofTactic): - def to_json(self) -> Any: - return { "tactic": "trivial" } - -class ProofScript: - def __init__(self, tactics : List[ProofTactic]) -> None: - self.tactics = tactics - - def to_json(self) -> Any: - return { 'tactics': [t.to_json() for t in self.tactics] } - -abc = UseProver(ABC()) -rme = UseProver(RME()) - -def cvc4(unints : List[str]) -> ProofTactic: - return UseProver(CVC4(unints)) - -def yices(unints : List[str]) -> ProofTactic: - return UseProver(Yices(unints)) - -def z3(unints : List[str]) -> ProofTactic: - return UseProver(Z3(unints)) diff --git a/python/saw/py.typed b/python/saw/py.typed deleted file mode 100644 index e69de29b..00000000 diff --git a/python/setup.cfg b/python/setup.cfg new file mode 100644 index 00000000..d71bc88d --- /dev/null +++ b/python/setup.cfg @@ -0,0 +1,20 @@ +[metadata] +name = argo-client +version = 0.0.1 +url = https://github.com/GaloisInc/argo/python +author = Galois Inc. +author_email = andrew@galois.com +license = BSD 3-Clause License +classifiers = + Programming Language :: Python :: 3 + License :: OSI Approved :: BSD License + Operating System :: OS Independent +description = A JSON RPC client library +long_description = file: README.md +long_description_content_type = text/markdown + +[options] +python_requires = >=3.7 +install_requires = + requests + mypy diff --git a/python/setup.py b/python/setup.py index f4bb3d62..b908cbe5 100644 --- a/python/setup.py +++ b/python/setup.py @@ -1,9 +1,3 @@ -from setuptools import setup, find_packages +import setuptools -setup(name='argo', - version='0.0.1', - packages=['argo', 'cryptol', 'saw'], - package_data={ - '': ['py.typed'] - } -) +setuptools.setup() diff --git a/python/cryptol/py.typed b/python/tests/__init__.py similarity index 100% rename from python/cryptol/py.typed rename to python/tests/__init__.py diff --git a/python/tests/run_test_servers.sh b/python/tests/run_test_servers.sh new file mode 100644 index 00000000..6151d451 --- /dev/null +++ b/python/tests/run_test_servers.sh @@ -0,0 +1,6 @@ +#!/bin/bash + +set -x + +cabal run file-echo-api --verbose=0 -- socket --port 50005 & +cabal run file-echo-api --verbose=0 -- http / --port 8080 & diff --git a/file-echo-api/test-scripts/test-data/hello.txt b/python/tests/test-data/hello.txt similarity index 100% rename from file-echo-api/test-scripts/test-data/hello.txt rename to python/tests/test-data/hello.txt diff --git a/file-echo-api/test-scripts/file-echo-tests.py b/python/tests/test_file-echo-api.py similarity index 95% rename from file-echo-api/test-scripts/file-echo-tests.py rename to python/tests/test_file-echo-api.py index 5675439f..5fcebff0 100644 --- a/file-echo-api/test-scripts/file-echo-tests.py +++ b/python/tests/test_file-echo-api.py @@ -1,15 +1,13 @@ import os from pathlib import Path import requests -import signal import subprocess -import sys import time import json import unittest import atexit -import argo.connection as argo +import argo_client.connection as argo dir_path = Path(os.path.dirname(os.path.realpath(__file__))) @@ -22,40 +20,6 @@ # Test the custom command line argument to load a file at server start hello_file = file_dir.joinpath('hello.txt') -# Test with both sockets and stdio -env = os.environ.copy() - -# Launch a separate process for the RemoteSocketProcess test -p = subprocess.Popen( - ["cabal", "v2-exec", "file-echo-api", "--verbose=0", "--", "socket", "--port", "50005"], - stdout=subprocess.DEVNULL, - stdin=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, - start_new_session=True, - env=env) - -p_http = subprocess.Popen( - ["cabal", "v2-exec", "file-echo-api", "--verbose=0", "--", "http", "/", "--port", "8080"], - stdout=subprocess.DEVNULL, - stdin=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, - start_new_session=True, - env=env) - - -def kill_procs(): - if p: p.kill() - if p_http: p_http.kill() - -atexit.register(kill_procs) - - -time.sleep(5) -assert(p is not None) -assert(p.poll() is None) -assert(p_http is not None) -assert(p_http.poll() is None) - # What the response to "show" looks like def show_res(*,content,uid,state): r = {'result':{'state':state,'stdout':'','stderr':'','answer':{'value':content}},'jsonrpc':'2.0','id':uid} @@ -423,4 +387,5 @@ def test_load_on_launch(self): self.assertEqual(actual, expected) -unittest.main() +if __name__ == '__main__': + unittest.main()