not sure if circify frontend for c is implemented correctly..

src/front/c/mod.rs

@@ -6,12 +6,13 @@ mod term;
 mod types;
 
 use super::FrontEnd;
+use crate::circify::Circify;
+
 use crate::front::c::term::*;
 use crate::ir::proof;
+use crate::ir::proof::ConstraintMetadata;
 use crate::ir::term::*;
-use lang_c::ast::{
-    BinaryOperator, BlockItem, Expression, ExternalDeclaration, Statement, TranslationUnit,
-};
+use lang_c::ast::*;
 
 // use std::collections::HashMap;
 use std::fmt::{self, Display, Formatter};
@@ -60,7 +61,7 @@ impl FrontEnd for C {
     fn gen(i: Inputs) -> Computation {
         let parser = parser::CParser::new();
         let p = parser.parse_file(&i.file).unwrap();
-        let mut g = CGen::new(p.source, p.unit, i.mode);
+        let mut g = CGen::new(i.inputs, i.mode, p.source, p.unit);
         g.gen();
         // g.circ.consume().borrow().clone()
 
@@ -73,25 +74,37 @@ impl FrontEnd for C {
 }
 
 struct CGen {
+    circ: Circify<Ct>,
+    mode: Mode,
     source: String,
     tu: TranslationUnit,
-    mode: Mode,
 }
 
 impl CGen {
-    fn new(source: String, tu: TranslationUnit, mode: Mode) -> Self {
-        Self { source, tu, mode }
+    fn new(inputs: Option<PathBuf>, mode: Mode, source: String, tu: TranslationUnit) -> Self {
+        let this = Self { 
+            circ: Circify::new(Ct::new(inputs.map(|i| parser::parse_inputs(i)))),
+            mode,
+            source, 
+            tu, 
+        };
+        this.circ
+            .cir_ctx()
+            .cs
+            .borrow_mut()
+            .metadata
+            .add_prover_and_verifier();
+        this
     }
 
     /// Unwrap a result with a span-dependent error
-    fn err<E: Display>(&self, e: E, expr: Expression) -> ! {
+    fn err<E: Display>(&self, e: E) -> ! {
         println!("Error: {}", e);
-        println!("In: {:#?}", expr);
         std::process::exit(1)
     }
 
-    fn unwrap<CTerm, E: Display>(&self, r: Result<CTerm, E>, expr: Expression) -> CTerm {
-        r.unwrap_or_else(|e| self.err(e, expr))
+    fn unwrap<CTerm, E: Display>(&self, r: Result<CTerm, E>) -> CTerm {
+        r.unwrap_or_else(|e| self.err(e))
     }
 
     fn get_bin_op(&self, op: BinaryOperator) -> fn(CTerm, CTerm) -> Result<CTerm, String> {
@@ -103,6 +116,9 @@ impl CGen {
 
     fn gen_expr(&self, expr: Expression) -> CTerm {
         let res = match expr.clone() {
+            // Expression::Identifier(node) => {
+            //     Ok(self.unwrap(self.circ.get_value(Loc::local(node.name.clone()))).unwrap_term()),
+            // }
             Expression::BinaryOperator(node) => {
                 let bin_expr = node.node;
                 println!("{:#?}", bin_expr);
@@ -116,7 +132,7 @@ impl CGen {
             }
             _ => unimplemented!("Expr {:#?} hasn't been implemented", expr),
         };
-        self.unwrap(res, expr)
+        self.unwrap(res)
     }
 
     fn gen_stmt(&self, stmt: Statement) {

src/front/c/parser.rs

@@ -2,7 +2,35 @@
 
 use lang_c::driver::Error;
 use lang_c::driver::{parse, Config, Parse};
+use rug::Integer;
+use std::fs::File;
+use std::io::{BufRead, BufReader};
 use std::path::PathBuf;
+use std::collections::HashMap;
+
+
+/// Parse an inputs file where each line has format: `no-withespace integer`.
+///
+/// Permits blank lines and ignores non-separating whitespace.
+///
+/// ```ignore
+/// x 5
+/// x.y -7
+/// ```
+pub fn parse_inputs(p: PathBuf) -> HashMap<String, Integer> {
+    let mut m = HashMap::new();
+    for l in BufReader::new(File::open(p).unwrap()).lines() {
+        let l = l.unwrap();
+        let l = l.trim();
+        if l.len() > 0 {
+            let mut s = l.split_whitespace();
+            let key = s.next().unwrap().to_owned();
+            let value = Integer::from(Integer::parse_radix(&s.next().unwrap(), 10).unwrap());
+            m.insert(key, value);
+        }
+    }
+    m
+}
 
 pub struct CParser {
     config: Config,
@@ -19,3 +47,5 @@ impl CParser {
         Ok(parse(&self.config, path)?)
     }
 }
+
+

src/front/c/term.rs

@@ -1,18 +1,23 @@
 //! C Terms
-use crate::front::c::types::Type;
+use crate::circify::{CirCtx, Embeddable};
+use crate::front::c::types::Ty;
 use crate::ir::term::*;
+use rug::Integer;
+use std::collections::HashMap;
 use std::fmt::{self, Display, Formatter};
 
+
+#[derive(Clone)]
 pub enum CTermData {
     CBool(Term),
     CInt(usize, Term),
 }
 
 impl CTermData {
-    pub fn type_(&self) -> Type {
+    pub fn type_(&self) -> Ty {
         match self {
-            Self::CBool(_) => Type::Bool,
-            Self::CInt(w, _) => Type::Uint(*w),
+            Self::CBool(_) => Ty::Bool,
+            Self::CInt(w, _) => Ty::Uint(*w),
         }
     }
 }
@@ -26,9 +31,23 @@ impl Display for CTermData {
     }
 }
 
+impl fmt::Debug for CTermData {
+    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+        write!(f, "{}", self)
+    }
+}
+
+
+#[derive(Clone, Debug)]
 pub struct CTerm {
-    term: CTermData,
-    udef: bool,
+    pub term: CTermData,
+    pub udef: bool,
+}
+
+impl Display for CTerm {
+    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+        write!(f, "Term: {:#?},\nudef: {}", self.term, self.udef)
+    }
 }
 
 fn wrap_bin_op(
@@ -59,18 +78,124 @@ pub fn add(a: CTerm, b: CTerm) -> Result<CTerm, String> {
     wrap_bin_op("+", Some(add_uint), None, a, b)
 }
 
-// fn sub_uint(a: Term, b: Term) -> Term {
-//     term![Op::BvBinOp(BvBinOp::Sub); a, b]
-// }
+pub struct Ct {
+    values: Option<HashMap<String, Integer>>,
+}
 
-// pub fn sub(a: Term, b: Term) -> Result<Term, String> {
-//     wrap_bin_op("-", Some(sub_uint), None, a, b)
-// }
+impl Ct {
+    pub fn new(values: Option<HashMap<String, Integer>>) -> Self {
+        Self {
+            values,
+        }
+    }
+}
 
-// fn mul_uint(a: Term, b: Term) -> Term {
-//     term![Op::BvNaryOp(BvNaryOp::Mul); a, b]
-// }
+impl Embeddable for Ct {
+    type T = CTerm;
+    type Ty = Ty;
+    fn declare(
+        &self,
+        ctx: &mut CirCtx,
+        ty: &Self::Ty,
+        raw_name: String,
+        user_name: Option<String>,
+        visibility: Option<PartyId>,
+    ) -> Self::T {
+        let get_int_val = || -> Integer {
+            self.values
+                .as_ref()
+                .and_then(|vs| {
+                    user_name
+                        .as_ref()
+                        .and_then(|n| vs.get(n))
+                        .or_else(|| vs.get(&raw_name))
+                })
+                .cloned()
+                .unwrap_or_else(|| Integer::from(0))
+        };
+        match ty {
+            Ty::Bool => {
+                Self::T {
+                    term: CTermData::CBool(
+                            ctx.cs.borrow_mut().new_var(
+                            &raw_name,
+                            Sort::Bool,
+                            || Value::Bool(get_int_val() != 0),
+                            visibility,
+                        )
+                    ),
+                    udef: false,
+                }
+            },
+            Ty::Uint(w) => {
+                Self::T {
+                    term: CTermData::CInt(
+                            *w,
+                            ctx.cs.borrow_mut().new_var(
+                            &raw_name,
+                            Sort::BitVector(*w),
+                            || Value::BitVector(BitVector::new(get_int_val(), *w)),
+                            visibility,
+                        ),
+                    ),
+                    udef: false,
+                }
+            }
+        }
+    }
+    fn ite(&self, ctx: &mut CirCtx, cond: Term, t: Self::T, f: Self::T) -> Self::T {
+        match (t.term, f.term) {
+            (CTermData::CBool(a), CTermData::CBool(b)) => {
+                Self::T {
+                    term: CTermData::CBool(term![Op::Ite; cond, a, b]),
+                    udef: false,
+                }
+            }
+            (CTermData::CInt(wa, a), CTermData::CInt(wb, b)) if wa == wb => {
+                Self::T {
+                    term: CTermData::CInt(wa, term![Op::Ite; cond, a, b]),
+                    udef: false,
+                }
+            }
+            (t, f) => panic!("Cannot ITE {} and {}", t, f),
+        }
+    }
 
-// pub fn mul(a: Term, b: Term) -> Result<Term, String> {
-//     wrap_bin_op("*", Some(mul_uint), None, a, b)
-// }
+    fn assign(
+        &self,
+        ctx: &mut CirCtx,
+        ty: &Self::Ty,
+        name: String,
+        t: Self::T,
+        visibility: Option<PartyId>,
+    ) -> Self::T {
+        assert!(&t.term.type_() == ty);
+        match (ty, t.term) {
+            (_, CTermData::CBool(b)) => {
+                Self::T {
+                    term: CTermData::CBool(ctx.cs.borrow_mut().assign(&name, b, visibility)),
+                    udef: false,
+                }
+            }
+            (_, CTermData::CInt(w, b)) => {
+                Self::T {
+                    term: CTermData::CInt(w, ctx.cs.borrow_mut().assign(&name, b, visibility)),
+                    udef: false,
+                }
+            }
+            _ => unimplemented!(),
+        }
+    }
+
+    fn values(&self) -> bool {
+        self.values.is_some()
+    }
+
+    fn type_of(&self, cterm: &Self::T) -> Self::Ty {
+        cterm.term.type_()
+    }
+
+    fn initialize_return(&self, ty: &Self::Ty, _ssa_name: &String) -> Self::T {
+        ty.default()
+    }
+}

src/front/c/types.rs

@@ -1,20 +1,42 @@
 //! C Types
+use crate::front::c::term::CTerm;
 use crate::front::c::term::CTermData;
-use crate::front::c::term::CTermData::{CBool, CInt};
-
 use crate::ir::term::*;
 
+use std::fmt::{self, Display, Formatter};
+
 #[derive(Clone, PartialEq, Eq)]
-pub enum Type {
+pub enum Ty {
     Bool,
     Uint(usize),
 }
 
-impl Type {
-    fn default(&self) -> CTermData {
+impl Ty {
+    pub fn default(&self) -> CTerm {
         match self {
-            Self::Bool => CBool(leaf_term(Op::Const(Value::Bool(false)))),
-            Self::Uint(w) => CInt(*w, bv_lit(0, *w)),
+            Self::Bool => CTerm {
+                term: CTermData::CBool(leaf_term(Op::Const(Value::Bool(false)))),
+                udef: false,
+            },
+            Self::Uint(w) => CTerm {
+                term: CTermData::CInt(*w, bv_lit(0, *w)),
+                udef: false,
+            }
         }
     }
 }
+
+impl Display for Ty {
+    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+        match self {
+            Ty::Bool => write!(f, "bool"),
+            Ty::Uint(w) => write!(f, "u{}", w),
+        }
+    }
+}
+
+impl fmt::Debug for Ty {
+    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+        write!(f, "{}", self)
+    }
+}