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

updating array constructs

Browse Source
This commit is contained in:
Edward Chen
2021-10-02 20:01:15 -04:00
parent 193a680eaa
commit 1bbb41126e
5 changed files with 90 additions and 42 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
src/circify/mem.rs
View File

@@ -6,7 +6,7 @@ use std::cell::RefCell;
use std::collections::{BTreeMap, HashMap};
use std::rc::Rc;
type AllocId = usize;
pub type AllocId = usize;
struct Alloc {
id: AllocId,
@@ -99,15 +99,12 @@ impl MemManager {
let v = alloc.var().clone();
// TODO change for MPC to store array inside allocs structure (somehow..)
if let Op::Var(n, _) = &v.op {
self.cs.borrow_mut().eval_and_save(&n, &array);
} else {
unreachable!()
}
// if let Op::Var(n, _) = &v.op {
// self.cs.borrow_mut().eval_and_save(&n, &array);
// } else {
// unreachable!()
// }
self.assert(term![Op::Eq; v, array]);
self.allocs.insert(id, alloc);
@@ -151,7 +148,7 @@ impl MemManager {
}
/// Write the value `val` to index `offset` in the allocation `id`.
pub fn store(&mut self, id: AllocId, offset: Term, val: Term) {
pub fn store(&mut self, id: AllocId, offset: Term, val: Term, cond: bool) {
let alloc = self.allocs.get_mut(&id).expect("Missing allocation");
assert_eq!(alloc.addr_width, check(&offset).as_bv());
assert_eq!(alloc.val_width, check(&val).as_bv());
@@ -160,20 +157,30 @@ impl MemManager {
// add new field to alloc? cur_var
// Add ite here with condition
// if true, update circ_ctx with new ref with store
// else return original arr
// Expose Store in circify
let new = term![Op::Store; alloc.var().clone(), offset, val];
alloc.next_var();
let v = alloc.var().clone();
if let Op::Var(n, _) = &v.op {
self.cs.borrow_mut().eval_and_save(&n, &new);
if cond {
// if true, update circ_ctx with new ref with store
let new = term![Op::Store; alloc.var().clone(), offset, val];
alloc.next_var();
let v = alloc.var().clone();
self.assert(term![Op::Eq; v, new]);
} else {
unreachable!()
// else return original arr
let new = term![Op::Store; alloc.var().clone(), offset, val];
let old_v = alloc.var().clone();
alloc.next_var();
let v = alloc.var().clone();
self.assert(term![Op::Eq; v, old_v]);
}
self.assert(term![Op::Eq; v, new]);
// if let Op::Var(n, _) = &v.op {
// self.cs.borrow_mut().eval_and_save(&n, &new);
// } else {
// unreachable!()
// }
}
/// Is `offset` in bounds for the allocation `id`?

6
src/circify/mod.rs
View File

@@ -1,5 +1,6 @@
//! A library for building front-ends
use crate::circify::mem::AllocId;
use crate::ir::term::*;
use std::cell::RefCell;
@@ -717,6 +718,11 @@ impl<E: Embeddable> Circify<E> {
self.break_(RET_BREAK_NAME)
}
/// Store a value in an array at a defined offset
pub fn store_(&mut self, id: AllocId, offset: Term, val: Term, cond: bool) {
self.cir_ctx.mem.store(id, offset, val, cond);
}
/// Assert something
pub fn assert(&mut self, t: Term) {
self.cir_ctx.cs.borrow_mut().assert(t);

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

@@ -9,13 +9,11 @@ use super::FrontEnd;
use crate::circify::{Circify, Loc, Val};
use crate::front::c::ast_utils::*;
use crate::front::c::term::*;
use crate::front::c::types::Ty;
use crate::ir::proof;
use crate::ir::proof::ConstraintMetadata;
use crate::ir::term::*;
use lang_c::ast::*;
// use std::collections::HashMap;
use std::fmt::{self, Display, Formatter};
use std::path::PathBuf;
@@ -196,25 +194,20 @@ impl CGen {
self.unwrap(res)
}
fn gen_init(&mut self, decl: InitDeclarator, ty: Option<Ty>) {
let name = name_from_decl(&decl.declarator.node);
let mut expr: Option<CTerm> = None;
if let Some(i) = decl.initializer {
match i.node {
Initializer::Expression(e) => {
expr = Some(cast(ty.clone(), self.gen_expr(e.node)));
}
Initializer::List(l) => {
println!("LIST INIT?: {:#?}", l);
for li in l {
println!("LIST ITEM: {:#?}", li);
}
unimplemented!("list type not implemented yet.");
fn gen_init(&mut self, init: Initializer) -> CTerm {
match init {
Initializer::Expression(e) => {
self.gen_expr(e.node)
}
Initializer::List(l) => {
let mut values: Vec<CTerm> = Vec::new();
for li in l {
let expr = self.gen_init(li.node.initializer.node);
values.push(expr)
}
unimplemented!("list type not implemented yet.");
}
}
let res = self.circ.declare_init(name.clone(), ty.unwrap(), Val::Term(expr.unwrap()));
self.unwrap(res);
}
fn gen_stmt(&mut self, stmt: Statement) {
@@ -224,9 +217,13 @@ impl CGen {
match node.node {
BlockItem::Declaration(node) => {
let decl = node.node;
let ty = decl_type(decl.clone());
let ty = decl_type(decl.clone()).unwrap();
assert!(decl.declarators.len() == 1);
self.gen_init(decl.declarators.first().unwrap().node.clone(), ty);
let d = decl.declarators.first().unwrap().node.clone();
let name = name_from_decl(&d.declarator.node);
let expr = self.gen_init(d.initializer.unwrap().node);
let res = self.circ.declare_init(name, ty.clone(), Val::Term(cast(Some(ty), expr)));
self.unwrap(res);
}
BlockItem::Statement(stmt) => {
self.gen_stmt(stmt.node);

34
src/front/c/term.rs
View File

@@ -11,6 +11,7 @@ use std::fmt::{self, Display, Formatter};
pub enum CTermData {
CBool(Term),
CInt(usize, Term),
CArray(Ty, Vec<CTerm>),
}
impl CTermData {
@@ -18,6 +19,7 @@ impl CTermData {
match self {
Self::CBool(_) => Ty::Bool,
Self::CInt(w, _) => Ty::Uint(*w),
Self::CArray(b, v) => Ty::Array(v.len(), Box::new(b.clone())),
}
}
/// Get all IR terms inside this value, as a list.
@@ -27,16 +29,26 @@ impl CTermData {
match term {
CTermData::CBool(b) => output.push(b.clone()),
CTermData::CInt(_, b) => output.push(b.clone()),
CTermData::CArray(_, v) => v.iter().for_each(|v| terms_tail(&v.term, output)),
}
}
terms_tail(self, &mut output);
output
}
pub fn unwrap_array(self) -> Result<Vec<CTerm>, String> {
match self {
CTermData::CArray(_, v) => Ok(v),
s => Err(format!("Not an array: {}", s)),
}
}
pub fn new_array(v: Vec<CTerm>) -> Result<CTerm, String> {
array(v)
}
pub fn term(&self) -> Term {
match self {
CTermData::CBool(b) => b.clone(),
CTermData::CInt(_, b) => b.clone(),
_ => unimplemented!("Haven't implemented return terms for arrays"),
}
}
}
@@ -101,6 +113,9 @@ pub fn cast(to_ty: Option<Ty>, t: CTerm) -> CTerm {
None => panic!("Bad cast from {} to {:?}", ty, to_ty)
}
}
CTermData::CArray(_n, _ty) => {
unimplemented!("Haven't implemented casting for arrays");
}
// _ => panic!("Bad cast from {} to {}", ty, to_ty)
}
}
@@ -352,6 +367,23 @@ pub fn cond(c: CTerm, a: CTerm, b: CTerm) -> Result<CTerm, String> {
ite(bool(c)?, a, b)
}
fn array<I: IntoIterator<Item = CTerm>>(elems: I) -> Result<CTerm, String> {
let v: Vec<CTerm> = elems.into_iter().collect();
if let Some(e) = v.first() {
let ty = e.term.type_();
if v.iter().skip(1).any(|a| a.term.type_() != ty) {
Err(format!("Inconsistent types in array"))
} else {
Ok( CTerm {
term: CTermData::CArray(ty, v),
udef: false
})
}
} else {
Err(format!("Empty array"))
}
}
pub struct Ct {
values: Option<HashMap<String, Integer>>,
}

8
src/front/c/types.rs
View File

@@ -9,6 +9,7 @@ use std::fmt::{self, Display, Formatter};
pub enum Ty {
Bool,
Uint(usize),
Array(usize, Box<Ty>)
}
impl Ty {
@@ -21,7 +22,11 @@ impl Ty {
Self::Uint(w) => CTerm {
term: CTermData::CInt(*w, bv_lit(0, *w)),
udef: false,
}
},
Self::Array(n, b) => CTerm {
term: CTermData::CArray((**b).clone(), vec![b.default(); *n]),
udef: false,
}
}
}
}
@@ -31,6 +36,7 @@ impl Display for Ty {
match self {
Ty::Bool => write!(f, "bool"),
Ty::Uint(w) => write!(f, "u{}", w),
Ty::Array(n, b) => write!(f, "{}[{}]", b, n),
}
}
}