diff --git a/README.md b/README.md index 911d3434..09ad36c9 100644 --- a/README.md +++ b/README.md @@ -67,18 +67,3 @@ and [cvc5](https://cvc5.github.io/) by setting the [RSMT2_CVC4_CMD](https://docs.rs/rsmt2/latest/rsmt2/conf/constant.CVC4_ENV_VAR.html) environmental variable to the SMT solver's invocation command (`cvc4` or `cvc5`). - -## Todo List - -- [ ] Intern variable names -- [ ] Tweak log system to expect exact target match -- [ ] C front-end -- [ ] Tune R1CS optimizer - - [ ] Less hash maps - - [ ] Consider using ff/ark-ff instead of gmp - - [ ] Consider a lazy merging strategy -- [ ] remove synchronization from term representation (or explore parallelism!) -- [ ] More SMT solver support - - [ ] Parse cvc4 models -- [ ] A more configurable term distribution (for fuzzing) -- [ ] Add user-defined (aka opaque) operator to IR diff --git a/TODO.md b/TODO.md index 695c99be..33031864 100644 --- a/TODO.md +++ b/TODO.md @@ -1,10 +1,8 @@ -Passes to write: - +Concrete: [ ] shrink bit-vectors using range analysis. * IR analysis infrastructure * shrink comparisons too * generalized version of constant comparison? -[ ] FE analysis infrastructure [ ] common sub-expression grouping * for commutative/associative ops? * after flattening @@ -22,14 +20,33 @@ Passes to write: [ ] Improving/parameterizing our IR term distribution * We use it to fuzz IR passes * General problem: Fuzzing language FEs +[ ] Implement sorts using hash-consing. + +Vague: +[ ] FE analysis infrastructure [ ] Recursive proving. [ ] Incorporate verifier challenges. [ ] Support functions in the compiler. [ ] Equality saturation/e-graphs? +Small research questions: +[ ] Model a RAM-extraction pass in Coq and prove it correct. + * input: a term-graph computation that uses functional arrays + * output: a term-graph computation that has RAM transcripts attached, has + *no* array sorts, and is provably equivalent. + * Passes that are likely important: + * Replace array variables with mass stores + * Lift tuples out of arrays with AoS -> SoA transformation + * Scalarize array equality with a big AND of EQ + * Flatten nested arrays? I haven't though this out. Requires scalarizing some stores/selects. + * Do a RAM extraction pass that assumes all arrays have primitive keys and value. +[ ] Model a RAM-extraction pass in Coq and prove it correct. + * pretty printing term DAGs with letification + * Like LaTeX meets letification. + Bigger research questions: [ ] SoK: compiling to R1CS * focus on embedding complex datatypes: * use lookups -[ ] Compiling to branching programs +[ ] Compiling to branching programs \ No newline at end of file diff --git a/examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c b/examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c index 2576b423..fab58cef 100644 --- a/examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c +++ b/examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c @@ -1,5 +1,3 @@ -#include "util.c" - int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b) { - return add(a, b); + return a + b; } \ No newline at end of file diff --git a/examples/C/mpc/unit_tests/function_tests/2pc_function_add.c b/examples/C/mpc/unit_tests/function_tests/2pc_function_add.c new file mode 100644 index 00000000..ddd5b5f3 --- /dev/null +++ b/examples/C/mpc/unit_tests/function_tests/2pc_function_add.c @@ -0,0 +1,9 @@ +#include "../util.c" + +int add_(int a, int b) { + return a + b; +} + +int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b) { + return add(a, b) + add_(a, b); +} \ No newline at end of file diff --git a/examples/C/mpc/unit_tests/arithmetic_tests/util.c b/examples/C/mpc/unit_tests/util.c similarity index 100% rename from examples/C/mpc/unit_tests/arithmetic_tests/util.c rename to examples/C/mpc/unit_tests/util.c diff --git a/examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_sum.zok b/examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_add.zok similarity index 53% rename from examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_sum.zok rename to examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_add.zok index 80036f70..2b2fdb4c 100644 --- a/examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_sum.zok +++ b/examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_add.zok @@ -1,5 +1,5 @@ -def sum(u32 a, u32 b) -> u32: +def add(u32 a, u32 b) -> u32: return a + b def main(private<1> u32 a, private<2> u32 b) -> u32: - return sum(a, b) + return add(a, b) + add(a, b) diff --git a/scripts/aby_tests/c_test_aby.py b/scripts/aby_tests/c_test_aby.py index ee73cf3c..a42fe70b 100755 --- a/scripts/aby_tests/c_test_aby.py +++ b/scripts/aby_tests/c_test_aby.py @@ -4,22 +4,21 @@ from utils import run_tests from test_suite import * if __name__ == "__main__": - # tests = arithmetic_tests + \ - # mod_tests + \ - # arithmetic_boolean_tests + \ - # nary_arithmetic_tests + \ - # bitwise_tests + \ - # boolean_tests + \ - # nary_boolean_tests + \ - # const_arith_tests + \ - # const_bool_tests + \ - # ite_tests + \ - # c_array_tests + \ - # div_tests + \ - # array_tests + tests = arithmetic_tests + \ + mod_tests + \ + arithmetic_boolean_tests + \ + nary_arithmetic_tests + \ + bitwise_tests + \ + boolean_tests + \ + nary_boolean_tests + \ + const_arith_tests + \ + const_bool_tests + \ + ite_tests + \ + c_array_tests + \ + div_tests + \ + function_tests + \ + array_tests # shift_tests - - test = add_tests # TODO: add support for return value - int promotion # unsigned_arithmetic_tests + \ diff --git a/scripts/aby_tests/test_suite.py b/scripts/aby_tests/test_suite.py index 64dfe555..4715b1bb 100644 --- a/scripts/aby_tests/test_suite.py +++ b/scripts/aby_tests/test_suite.py @@ -1,20 +1,3 @@ -add_tests = [ - [ - "Add two numbers - 1", - 3, - "./third_party/ABY/build/bin/2pc_add", - {"a": 1, "b": 0}, - {"a": 0, "b": 2}, - ], - [ - "Add two numbers - 2", - 2, - "./third_party/ABY/build/bin/2pc_add", - {"a": 0, "b": 0}, - {"a": 0, "b": 2}, - ], -] - arithmetic_tests = [ [ "Add two numbers - 1", @@ -579,21 +562,20 @@ loop_tests = [ ] function_tests = [ - [ - "Sum() two numbers - 1", - 3, - "./third_party/ABY/build/bin/2pc_function_sum", + [ + "Function add two numbers - 1", + 6, + "./third_party/ABY/build/bin/2pc_function_add", {"a": 1, "b": 0}, {"a": 0, "b": 2}, ], [ - "Sum() two numbers - 2", - 2, - "./third_party/ABY/build/bin/2pc_function_sum", + "Function add two numbers - 2", + 4, + "./third_party/ABY/build/bin/2pc_function_add", {"a": 0, "b": 0}, {"a": 0, "b": 2}, ], - ] shift_tests = [ diff --git a/scripts/build_mpc_c_test.zsh b/scripts/build_mpc_c_test.zsh index 170b842d..2ba0eb3f 100755 --- a/scripts/build_mpc_c_test.zsh +++ b/scripts/build_mpc_c_test.zsh @@ -26,57 +26,60 @@ function mpc_test { # build mpc arithmetic tests mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_sub.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mult.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mult_add_pub.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mod.c -# # mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_add_unsigned.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_sub.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mult.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mult_add_pub.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_mod.c +# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_add_unsigned.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_equals.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_greater_than.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_greater_equals.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_less_than.c -# mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_less_equals.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_equals.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_greater_than.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_greater_equals.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_less_than.c +mpc_test 2 ./examples/C/mpc/unit_tests/arithmetic_tests/2pc_int_less_equals.c -# # build mpc nary arithmetic tests -# mpc_test 2 ./examples/C/mpc/unit_tests/nary_arithmetic_tests/2pc_nary_arithmetic_add.c +# build mpc nary arithmetic tests +mpc_test 2 ./examples/C/mpc/unit_tests/nary_arithmetic_tests/2pc_nary_arithmetic_add.c -# # build mpc bitwise tests -# mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_and.c -# mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_or.c -# mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_xor.c +# build mpc bitwise tests +mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_and.c +mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_or.c +mpc_test 2 ./examples/C/mpc/unit_tests/bitwise_tests/2pc_bitwise_xor.c -# # build mpc boolean tests -# mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_and.c -# mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_or.c -# mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_equals.c +# build mpc boolean tests +mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_and.c +mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_or.c +mpc_test 2 ./examples/C/mpc/unit_tests/boolean_tests/2pc_boolean_equals.c -# # build mpc nary boolean tests -# mpc_test 2 ./examples/C/mpc/unit_tests/nary_boolean_tests/2pc_nary_boolean_and.c +# build mpc nary boolean tests +mpc_test 2 ./examples/C/mpc/unit_tests/nary_boolean_tests/2pc_nary_boolean_and.c -# # build mpc const tests -# mpc_test 2 ./examples/C/mpc/unit_tests/const_tests/2pc_const_arith.c -# mpc_test 2 ./examples/C/mpc/unit_tests/const_tests/2pc_const_bool.c +# build mpc const tests +mpc_test 2 ./examples/C/mpc/unit_tests/const_tests/2pc_const_arith.c +mpc_test 2 ./examples/C/mpc/unit_tests/const_tests/2pc_const_bool.c -# # build if statement tests -# mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_ret_bool.c -# mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_ret_int.c -# mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_only_if.c +# build if statement tests +mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_ret_bool.c +mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_ret_int.c +mpc_test 2 ./examples/C/mpc/unit_tests/ite_tests/2pc_ite_only_if.c -# # build div tests -# mpc_test 2 ./examples/C/mpc/unit_tests/div_tests/2pc_div.c +# build div tests +mpc_test 2 ./examples/C/mpc/unit_tests/div_tests/2pc_div.c -# # build array tests -# mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_sum.c -# mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_index.c -# mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_index_2.c +# build array tests +mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_sum.c +mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_index.c +mpc_test 2 ./examples/C/mpc/unit_tests/array_tests/2pc_array_index_2.c -# # build circ/compiler array tests -# mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array.c -# mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_1.c -# mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_2.c -# mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_3.c -# mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_sum_c.c +# build circ/compiler array tests +mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array.c +mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_1.c +mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_2.c +mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_3.c +mpc_test 2 ./examples/C/mpc/unit_tests/c_array_tests/2pc_array_sum_c.c + +# build function tests +mpc_test 2 ./examples/C/mpc/unit_tests/function_tests/2pc_function_add.c # # # build shift tests # # mpc_test 2 ./examples/C/mpc/unit_tests/shift_tests/2pc_lhs.c diff --git a/scripts/build_mpc_zokrates_test.zsh b/scripts/build_mpc_zokrates_test.zsh index 0d7b46cc..826f4c88 100755 --- a/scripts/build_mpc_zokrates_test.zsh +++ b/scripts/build_mpc_zokrates_test.zsh @@ -68,7 +68,7 @@ mpc_test 2 ./examples/ZoKrates/mpc/unit_tests/ite_tests/2pc_ite_ret_int.zok mpc_test 2 ./examples/ZoKrates/mpc/unit_tests/loop_tests/2pc_loop_sum.zok # build mpc function tests -mpc_test 2 ./examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_sum.zok +mpc_test 2 ./examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_add.zok # build mpc shift tests # mpc_test 2 ./examples/ZoKrates/mpc/unit_tests/shift_tests/2pc_lhs.zok diff --git a/src/circify/mem.rs b/src/circify/mem.rs index 86ac7228..e0d4299c 100644 --- a/src/circify/mem.rs +++ b/src/circify/mem.rs @@ -1,7 +1,6 @@ //! The stack-allocation memory manager use crate::ir::term::*; -use rug::Integer; use std::collections::HashMap; /// Identifier for an Allocation block in memory @@ -115,7 +114,7 @@ impl MemManager { pub fn in_bounds(&self, id: AllocId, offset: Term) -> Term { let alloc = self.allocs.get(&id).expect("Missing allocation"); assert_eq!(alloc.addr_width, check(&offset).as_bv()); - term![Op::BvBinPred(BvBinPred::Ult); offset, bv_lit(Integer::from(alloc.size), alloc.addr_width)] + term![Op::BvBinPred(BvBinPred::Ult); offset, bv_lit(alloc.size, alloc.addr_width)] } /// Get size of the array at the allocation `id` @@ -143,12 +142,12 @@ mod test { let _id1 = mem.zero_allocate(6, 4, 8); mem.store( id0, - bv_lit(Integer::from(3), 4), - bv_lit(Integer::from(2), 8), + bv_lit(3, 4), + bv_lit(2, 8), leaf_term(Op::Const(Value::Bool(true))), ); - let a = mem.load(id0, bv_lit(Integer::from(3), 4)); - let b = mem.load(id0, bv_lit(Integer::from(1), 4)); + let a = mem.load(id0, bv_lit(3, 4)); + let b = mem.load(id0, bv_lit(1, 4)); let t = term![Op::BvBinPred(BvBinPred::Ugt); a, b]; cs.borrow_mut().assert(t); let sys = term( @@ -166,12 +165,12 @@ mod test { let _id1 = mem.zero_allocate(6, 4, 8); mem.store( id0, - bv_lit(Integer::from(3), 4), + bv_lit(3, 4), bv_var("a", 8), leaf_term(Op::Const(Value::Bool(true))), ); - let a = mem.load(id0, bv_lit(Integer::from(3), 4)); - let b = mem.load(id0, bv_lit(Integer::from(3), 4)); + let a = mem.load(id0, bv_lit(3, 4)); + let b = mem.load(id0, bv_lit(3, 4)); let t = term![Op::Not; term![Op::Eq; a, b]]; cs.borrow_mut().assert(t); let sys = term( diff --git a/src/front/c/ast_utils.rs b/src/front/c/ast_utils.rs index f2bb57ea..c4627e75 100644 --- a/src/front/c/ast_utils.rs +++ b/src/front/c/ast_utils.rs @@ -31,6 +31,14 @@ impl Display for FnInfo { } } +pub fn name_from_expr(node: Node) -> String { + if let Identifier(i) = node.node { + i.node.name.clone() + } else { + panic!("Expression is not an identifier '{:#?}'", node.node); + } +} + pub fn name_from_decl(decl: &Declarator) -> String { match decl.kind.node { DeclaratorKind::Identifier(ref id) => id.node.name.clone(), @@ -38,14 +46,6 @@ pub fn name_from_decl(decl: &Declarator) -> String { } } -pub fn name_from_ident(ident: &Expression) -> String { - match ident { - Identifier(i) => i.node.name.clone(), - //TODO: make this Option - _ => "".to_string(), - } -} - pub fn d_type_(ds: Vec>) -> Option { assert!(!ds.is_empty()); let res: Vec> = ds diff --git a/src/front/c/mod.rs b/src/front/c/mod.rs index 3e7d6aee..1ed49837 100644 --- a/src/front/c/mod.rs +++ b/src/front/c/mod.rs @@ -109,7 +109,7 @@ impl CGen { r.unwrap_or_else(|e| self.err(e)) } - fn array_select(&mut self, array: CTerm, idx: CTerm) -> Result { + fn array_select(&self, array: CTerm, idx: CTerm) -> Result { match (array.clone().term, idx.term) { (CTermData::CArray(ty, id), CTermData::CInt(_, _, idx)) => { let i = id.unwrap_or_else(|| panic!("Unknown AllocID: {:#?}", array)); @@ -160,14 +160,14 @@ impl CGen { fn lval(&mut self, expr: Node) -> CLoc { match expr.node { Expression::Identifier(_) => { - let base_name = name_from_ident(&expr.node); + let base_name = name_from_expr(expr); CLoc::Var(Loc::local(base_name)) } Expression::BinaryOperator(node) => { let bin_op = node.node; match bin_op.operator.node { BinaryOperator::Index => { - let base_name = name_from_ident(&bin_op.lhs.node); + let base_name = name_from_expr(*bin_op.lhs); let idx = self.gen_expr(bin_op.rhs.node); CLoc::Idx(Box::new(CLoc::Var(Loc::local(base_name))), idx) } @@ -251,7 +251,7 @@ impl CGen { panic!("Bad visibility declaration."); } - fn const_(&mut self, c: Constant) -> CTerm { + fn const_(&self, c: Constant) -> CTerm { match c { // TODO: move const integer function out to separate function Constant::Integer(i) => cterm(CTermData::CInt( @@ -263,7 +263,7 @@ impl CGen { } } - fn get_bin_op(&mut self, op: BinaryOperator) -> fn(CTerm, CTerm) -> Result { + fn get_bin_op(&self, op: BinaryOperator) -> fn(CTerm, CTerm) -> Result { match op { BinaryOperator::Plus => add, BinaryOperator::AssignPlus => add, @@ -288,7 +288,7 @@ impl CGen { } } - fn get_u_op(&mut self, op: UnaryOperator) -> fn(CTerm, CTerm) -> Result { + fn get_u_op(&self, op: UnaryOperator) -> fn(CTerm, CTerm) -> Result { match op { UnaryOperator::PostIncrement => add, _ => unimplemented!("UnaryOperator {:#?} hasn't been implemented", op), @@ -371,8 +371,49 @@ impl CGen { Ok(cast(to_ty, expr)) } Expression::Call(node) => { - println!("{:#?}", node); - unimplemented!(); + let CallExpression { callee, arguments } = node.node; + let fname = name_from_expr(*callee); + + let f = self + .functions + .get(&fname) + .unwrap_or_else(|| panic!("No function '{}'", fname)) + .clone(); + + let FnInfo { + name, + ret_ty, + args: parameters, + body, + } = f; + + // Add parameters + let args = arguments + .iter() + .map(|e| self.gen_expr(e.node.clone())) + .collect::>(); + + // setup stack frame for entry function + self.circ.enter_fn(name, ret_ty.clone()); + assert_eq!(parameters.len(), args.len()); + + for (p, a) in parameters.iter().zip(args) { + let base_ty = d_type_(p.specifiers.to_vec()); + let d = &p.declarator.as_ref().unwrap().node; + let derived_ty = self.derived_type_(base_ty.unwrap(), d.derived.to_vec()); + let name = name_from_decl(d); + let d_res = self.circ.declare_init(name, derived_ty, Val::Term(a)); + self.unwrap(d_res); + } + + self.gen_stmt(body); + + let ret = self + .circ + .exit_fn() + .map(|a| a.unwrap_term()) + .unwrap_or_else(|| cterm(CTermData::CBool(bool_lit(false)))); + Ok(cast(ret_ty, ret)) } _ => unimplemented!("Expr {:#?} hasn't been implemented", expr), }; diff --git a/src/target/aby/trans.rs b/src/target/aby/trans.rs index 983b2b29..e095df55 100644 --- a/src/target/aby/trans.rs +++ b/src/target/aby/trans.rs @@ -127,7 +127,7 @@ impl ToABY { let name = ToABY::get_var_name(t.clone(), true); let s_circ = self.get_sharetype_circ(t); format!( - "s_{} = {}->PutCONSGate((uint64_t){}, bitlen);\n", + "s_{} = {}->PutCONSGate((uint32_t){}, bitlen);\n", name, s_circ, name ) }