github/circ
1
1
Fork 0
mirror of https://github.com/circify/circ.git synced 2026-04-21 03:00:54 -04:00
Code Issues Packages Projects Releases Wiki Activity

Added function and import support for C frontend

Browse Source
This commit is contained in:
Edward Chen
2022-02-07 03:03:04 -05:00
parent e05c49270d 09c9f032ce
commit 58ef4dd291
14 changed files with 165 additions and 132 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
README.md
View File

@@ -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

25
TODO.md
View File

@@ -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

4
examples/C/mpc/unit_tests/arithmetic_tests/2pc_add.c
View File

@@ -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;
}

9
examples/C/mpc/unit_tests/function_tests/2pc_function_add.c Normal file
View File

@@ -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);
}

0
examples/C/mpc/unit_tests/arithmetic_tests/util.c → examples/C/mpc/unit_tests/util.c
View File

4
examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_sum.zok → examples/ZoKrates/mpc/unit_tests/function_tests/2pc_function_add.zok
View File

@@ -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)

29
scripts/aby_tests/c_test_aby.py
View File

@@ -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 + \

32
scripts/aby_tests/test_suite.py
View File

@@ -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 = [

85
scripts/build_mpc_c_test.zsh
View File

@@ -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

2
scripts/build_mpc_zokrates_test.zsh
View File

@@ -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

17
src/circify/mem.rs
View File

@@ -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(

16
src/front/c/ast_utils.rs
View File

@@ -31,6 +31,14 @@ impl Display for FnInfo {
}
}
pub fn name_from_expr(node: Node<Expression>) -> 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<Node<DeclarationSpecifier>>) -> Option<Ty> {
assert!(!ds.is_empty());
let res: Vec<Option<Ty>> = ds

57
src/front/c/mod.rs
View File

@@ -109,7 +109,7 @@ impl CGen {
r.unwrap_or_else(|e| self.err(e))
}
fn array_select(&mut self, array: CTerm, idx: CTerm) -> Result<CTerm, String> {
fn array_select(&self, array: CTerm, idx: CTerm) -> Result<CTerm, String> {
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<Expression>) -> 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<CTerm, String> {
fn get_bin_op(&self, op: BinaryOperator) -> fn(CTerm, CTerm) -> Result<CTerm, String> {
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<CTerm, String> {
fn get_u_op(&self, op: UnaryOperator) -> fn(CTerm, CTerm) -> Result<CTerm, String> {
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::<Vec<_>>();
// 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),
};

2
src/target/aby/trans.rs
View File

@@ -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
)
}