Skip to content

Commit a6b7578

Browse files
gebnergebner
committed
Fix array example.
1 parent 2226c89 commit a6b7578

8 files changed

Lines changed: 237 additions & 104 deletions

File tree

‎examples/c2pulse.h‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,10 @@
1414
#define _assert(p) ({ __attribute__((annotate("c2pulse-assert", __capture_args(p)))) {} })
1515
#define _ghost_stmt(args) ({ __attribute__((annotate("c2pulse-ghost-stmt", __capture_args(args)))) {} })
1616

17-
#define _plain [[clang::annotate("c2pulse-plain")]]
18-
#define _consumes [[clang::annotate("c2pulse-consumes")]]
19-
#define _array [[clang::annotate("c2pulse-array")]]
20-
#define _pure [[clang::annotate("c2pulse-pure")]]
17+
#define _plain __attribute__((annotate("c2pulse-plain")))
18+
#define _consumes __attribute__((annotate("c2pulse-consumes")))
19+
#define _array __attribute((annotate("c2pulse-array")))
20+
#define _pure __attribute((annotate("c2pulse-pure")))
2121

2222
#define _inline_pulse(args) _inline_pulse(__capture_args(args))
2323

‎src/env.rs‎

Lines changed: 138 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
use crate::{ir::*, mayberc::MaybeRc};
1+
use crate::impl_display_using_prettyir;
2+
use crate::{ir::pretty::PrettyIR, ir::*, mayberc::MaybeRc};
23
use std::{collections::HashMap, rc::Rc};
34

45
#[derive(Clone, Debug, Default)]
@@ -39,6 +40,68 @@ macro_rules! both_sides {
3940
};
4041
}
4142

43+
#[derive(Debug, Clone)]
44+
pub enum InferError {
45+
CannotDeref(MaybeRc<Type>),
46+
CannotAccessMember(MaybeRc<Type>),
47+
VariableNotFound(Rc<Ident>),
48+
NotAField(Rc<Ident>, Rc<Ident>),
49+
NotAFunction(Rc<Ident>),
50+
CannotIndex(MaybeRc<Type>),
51+
}
52+
53+
impl_display_using_prettyir!(InferError);
54+
impl PrettyIR for InferError {
55+
fn to_doc(&self) -> ::pretty::RcDoc<'_, ()> {
56+
use ::pretty::*;
57+
(match self {
58+
InferError::CannotDeref(ty) => docs![
59+
&RcAllocator,
60+
"cannot dereference",
61+
RcDoc::line(),
62+
ty.to_doc(),
63+
],
64+
InferError::CannotAccessMember(ty) => docs![
65+
&RcAllocator,
66+
ty.to_doc(),
67+
RcDoc::line(),
68+
"has no members (not a structure)",
69+
],
70+
InferError::VariableNotFound(name) => docs![
71+
&RcAllocator,
72+
"variable",
73+
RcDoc::line(),
74+
name.to_doc(),
75+
RcDoc::line(),
76+
"not found",
77+
],
78+
InferError::NotAField(struct_name, field_name) => docs![
79+
&RcAllocator,
80+
struct_name.to_doc(),
81+
RcDoc::line(),
82+
"does not have a field",
83+
RcDoc::line(),
84+
field_name.to_doc(),
85+
],
86+
InferError::NotAFunction(name) => docs![
87+
&RcAllocator,
88+
name.to_doc(),
89+
RcDoc::line(),
90+
"is not a function",
91+
],
92+
InferError::CannotIndex(ty) => docs![
93+
&RcAllocator,
94+
"cannot index into",
95+
RcDoc::line(),
96+
ty.to_doc(),
97+
],
98+
})
99+
.group()
100+
.nest(2)
101+
.into_doc()
102+
}
103+
}
104+
42105
impl Env {
43106
pub fn new() -> Env {
44107
Env::default()
@@ -159,73 +222,73 @@ impl Env {
159222
id
160223
}
161224

162-
pub fn infer_rvalue(&self, rvalue: &Expr) -> Option<MaybeRc<Type>> {
163-
self.infer_expr(rvalue)
164-
}
165-
166-
pub fn infer_lvalue(&self, lvalue: &Expr) -> Option<MaybeRc<Type>> {
167-
self.infer_expr(lvalue)
168-
}
169-
170-
pub fn infer_expr(&self, expr: &Expr) -> Option<MaybeRc<Type>> {
225+
pub fn infer_expr(&self, expr: &Expr) -> Result<MaybeRc<Type>, InferError> {
171226
match &expr.val {
172-
ExprT::Var(ident) => Some(self.lookup_var_type(ident)?.clone().into()),
227+
ExprT::Var(ident) => {
228+
let Some(var_type) = self.lookup_var_type(ident) else {
229+
return Err(InferError::VariableNotFound(ident.clone()));
230+
};
231+
Ok(var_type.clone().into())
232+
}
173233
ExprT::Deref(x) => {
174234
let x_ty = self.vtype_whnf(self.infer_expr(x)?);
175235
match &x_ty.val {
176-
TypeT::Pointer(to, _) => Some(to.clone().into()),
177-
_ => None,
236+
TypeT::Pointer(to, _) => Ok(to.clone().into()),
237+
_ => Err(InferError::CannotDeref(x_ty)),
178238
}
179239
}
180240
ExprT::Member(x, a) => {
181241
let x_ty = self.vtype_whnf(self.infer_expr(x)?);
182242
match &x_ty.val {
183243
TypeT::Pointer(_, PointerKind::Array) if &*a.val == "_length" => {
184-
Some(TypeT::SpecInt.with_loc_core(expr.loc.clone()).into())
244+
Ok(TypeT::SpecInt.with_loc_core(expr.loc.clone()).into())
185245
}
186-
TypeT::TypeRef(TypeRefKind::Struct(s)) => {
187-
Some(self.lookup_struct(s)?.get_field(a)?.clone().into())
246+
TypeT::TypeRef(TypeRefKind::Struct(s_name)) => {
247+
let Some(s) = self.lookup_struct(s_name) else {
248+
return Err(InferError::CannotAccessMember(x_ty.clone()));
249+
};
250+
let Some(f) = s.get_field(a) else {
251+
return Err(InferError::NotAField(s_name.clone(), a.clone()));
252+
};
253+
Ok(f.clone().into())
188254
}
189-
_ => None,
255+
_ => Err(InferError::CannotAccessMember(x_ty)),
190256
}
191257
}
192258
ExprT::Index(arr, _idx) => {
193259
let arr_ty = self.vtype_whnf(self.infer_expr(arr)?);
194260
match &arr_ty.val {
195-
TypeT::Pointer(elem, PointerKind::Array) => Some(elem.clone().into()),
196-
_ => None,
261+
TypeT::Pointer(elem, PointerKind::Array) => Ok(elem.clone().into()),
262+
_ => Err(InferError::CannotIndex(arr_ty)),
197263
}
198264
}
199-
ExprT::IntLit(_, ty) => Some(ty.clone().into()),
200-
ExprT::Ref(v) => Some(
201-
expr.reuse_loc(TypeT::Pointer(
265+
ExprT::IntLit(_, ty) => Ok(ty.clone().into()),
266+
ExprT::Ref(v) => Ok(expr
267+
.reuse_loc(TypeT::Pointer(
202268
self.infer_expr(v)?.to_rc(),
203269
PointerKind::Ref,
204270
))
205-
.into(),
206-
),
271+
.into()),
207272
ExprT::FnCall(f, _args) => match self.globals.fns.get(&f.val) {
208-
Some(f_decl) => Some(f_decl.ret_type.clone().into()),
209-
None => None,
273+
Some(f_decl) => Ok(f_decl.ret_type.clone().into()),
274+
None => Err(InferError::NotAFunction(f.clone())),
210275
},
211-
ExprT::Cast(_, ty) => Some(ty.clone().into()),
212-
ExprT::Error(ty) => Some(ty.clone().into()),
213-
ExprT::Malloc(ty) => Some(
214-
expr.reuse_loc(TypeT::Pointer(ty.clone(), PointerKind::Ref))
215-
.into(),
216-
),
217-
ExprT::MallocArray(ty, _) => Some(
218-
expr.reuse_loc(TypeT::Pointer(ty.clone(), PointerKind::Array))
219-
.into(),
220-
),
221-
ExprT::Free(_) => Some(TypeT::Void.with_loc_core(expr.loc.clone()).into()),
222-
ExprT::InlinePulse(_, ty) => Some(ty.clone().into()),
276+
ExprT::Cast(_, ty) => Ok(ty.clone().into()),
277+
ExprT::Error(ty) => Ok(ty.clone().into()),
278+
ExprT::Malloc(ty) => Ok(expr
279+
.reuse_loc(TypeT::Pointer(ty.clone(), PointerKind::Ref))
280+
.into()),
281+
ExprT::MallocArray(ty, _) => Ok(expr
282+
.reuse_loc(TypeT::Pointer(ty.clone(), PointerKind::Array))
283+
.into()),
284+
ExprT::Free(_) => Ok(TypeT::Void.with_loc_core(expr.loc.clone()).into()),
285+
ExprT::InlinePulse(_, ty) => Ok(ty.clone().into()),
223286
ExprT::UnOp(UnOp::Not, _)
224287
| ExprT::BinOp(
225288
BinOp::Eq | BinOp::LEq | BinOp::Lt | BinOp::LogOr | BinOp::Implies,
226289
_,
227290
_,
228-
) => Some(TypeT::Bool.with_loc_core(expr.loc.clone()).into()),
291+
) => Ok(TypeT::Bool.with_loc_core(expr.loc.clone()).into()),
229292
ExprT::UnOp(UnOp::Neg | UnOp::BitNot, lhs)
230293
| ExprT::BinOp(
231294
BinOp::LogAnd
@@ -242,14 +305,13 @@ impl Env {
242305
lhs,
243306
_,
244307
) => self.infer_expr(lhs),
245-
ExprT::BoolLit(_) => Some(TypeT::Bool.with_loc_core(expr.loc.clone()).into()),
246-
ExprT::Live(_) => Some(TypeT::SLProp.with_loc_core(expr.loc.clone()).into()),
308+
ExprT::BoolLit(_) => Ok(TypeT::Bool.with_loc_core(expr.loc.clone()).into()),
309+
ExprT::Live(_) => Ok(TypeT::SLProp.with_loc_core(expr.loc.clone()).into()),
247310
ExprT::Old(v) => self.infer_expr(v),
248311
ExprT::Forall(_, _, body) | ExprT::Exists(_, _, body) => self.infer_expr(body),
249-
ExprT::StructInit(name, _) => Some(
250-
expr.reuse_loc(TypeT::TypeRef(TypeRefKind::Struct(name.clone())))
251-
.into(),
252-
),
312+
ExprT::StructInit(name, _) => Ok(expr
313+
.reuse_loc(TypeT::TypeRef(TypeRefKind::Struct(name.clone())))
314+
.into()),
253315
}
254316
}
255317

@@ -403,3 +465,34 @@ impl Env {
403465
}
404466
}
405467
}
468+
469+
impl_display_using_prettyir!(Env);
470+
471+
impl PrettyIR for Env {
472+
fn to_doc(&self) -> ::pretty::RcDoc<'_, ()> {
473+
use ::pretty::*;
474+
RcDoc::intersperse(
475+
self.locals.iter().map(|(local, LocalDecl { ty, kind })| {
476+
local
477+
.to_doc()
478+
.append(RcDoc::space())
479+
.append(":")
480+
.append(RcDoc::line())
481+
.append(ty.to_doc())
482+
.group()
483+
.append(
484+
RcDoc::line()
485+
.append(match kind {
486+
LocalDeclKind::LValue => "(lvalue)",
487+
LocalDeclKind::RValue => "(rvalue)",
488+
})
489+
.group(),
490+
)
491+
.nest(2)
492+
.group()
493+
}),
494+
RcDoc::hardline(),
495+
)
496+
.group()
497+
}
498+
}

‎src/ir/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use num_bigint::BigInt;
22
use std::fmt::{Debug, Display};
33
use std::rc::Rc;
4-
mod pretty;
4+
pub mod pretty;
55

66
#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)]
77
pub struct Position {

‎src/ir/pretty.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,10 @@ fn inline_pulse_code_to_doc<'a>(code: &'a InlinePulseCode) -> RcDoc<'a, ()> {
1919
}))
2020
}
2121

22+
#[macro_export]
2223
macro_rules! impl_display_using_prettyir {
2324
($t:ty) => {
24-
impl Display for $t {
25+
impl ::std::fmt::Display for $t {
2526
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
2627
write!(f, "{}", self.to_doc().pretty(80))
2728
}

‎src/pass/check.rs‎

Lines changed: 19 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -22,18 +22,17 @@ impl<'a> Checker<'a> {
2222
});
2323
}
2424

25-
fn infer_rvalue(&mut self, env: &Env, rval: &Expr) -> Option<MaybeRc<Type>> {
26-
env.infer_rvalue(rval).or_else(|| {
27-
self.report(format!("cannot infer type of {}", rval), &rval.loc);
28-
None
29-
})
30-
}
31-
32-
fn infer_lvalue(&mut self, env: &Env, lval: &Expr) -> Option<MaybeRc<Type>> {
33-
env.infer_lvalue(lval).or_else(|| {
34-
self.report(format!("cannot infer type of {}", lval), &lval.loc);
35-
None
36-
})
25+
fn infer_expr(&mut self, env: &Env, rval: &Expr) -> Option<MaybeRc<Type>> {
26+
match env.infer_expr(rval) {
27+
Ok(ty) => Some(ty),
28+
Err(error) => {
29+
self.report(
30+
format!("cannot infer type of {}: {}\n{}", rval, error, env),
31+
&rval.loc,
32+
);
33+
None
34+
}
35+
}
3736
}
3837

3938
fn check_type_eq(&mut self, env: &Env, actual: MaybeRc<Type>, expected: MaybeRc<Type>) {
@@ -47,7 +46,7 @@ impl<'a> Checker<'a> {
4746

4847
fn check_has_type(&mut self, env: &Env, rval: &Expr, expected: MaybeRc<Type>) {
4948
if self.check_types
50-
&& let Some(ty) = self.infer_rvalue(env, rval)
49+
&& let Some(ty) = self.infer_expr(env, rval)
5150
&& !env.vtype_eq(ty.clone().into(), expected.clone())
5251
{
5352
self.report(
@@ -135,7 +134,7 @@ impl<'a> Checker<'a> {
135134
ExprT::Deref(inner) => {
136135
self.check_rvalue(env, inner);
137136
if self.check_types
138-
&& let Some(rval_ty) = self.infer_rvalue(env, inner)
137+
&& let Some(rval_ty) = self.infer_expr(env, inner)
139138
&& !self.is_pointer_type(env, rval_ty.clone())
140139
{
141140
self.report(format!("not a pointer type: {}", rval_ty), &inner.loc)
@@ -144,7 +143,7 @@ impl<'a> Checker<'a> {
144143
ExprT::Member(x, a) => {
145144
self.check_rvalue(env, x);
146145
if self.check_types
147-
&& let Some(t) = self.infer_rvalue(env, x)
146+
&& let Some(t) = self.infer_expr(env, x)
148147
{
149148
let t = env.vtype_whnf(t);
150149
match &t.val {
@@ -170,15 +169,15 @@ impl<'a> Checker<'a> {
170169
self.check_rvalue(env, arr);
171170
self.check_rvalue(env, idx);
172171
if self.check_types {
173-
if let Some(arr_ty) = self.infer_rvalue(env, arr) {
172+
if let Some(arr_ty) = self.infer_expr(env, arr) {
174173
let arr_ty = env.vtype_whnf(arr_ty);
175174
match &arr_ty.val {
176175
TypeT::Pointer(_, PointerKind::Array) => {}
177176
TypeT::Error => {}
178177
_ => self.report(format!("not an array type: {}", arr_ty), &rval.loc),
179178
}
180179
}
181-
if let Some(idx_ty) = self.infer_rvalue(env, idx) {
180+
if let Some(idx_ty) = self.infer_expr(env, idx) {
182181
let idx_ty = env.vtype_whnf(idx_ty);
183182
match &idx_ty.val {
184183
TypeT::SizeT => {}
@@ -200,7 +199,7 @@ impl<'a> Checker<'a> {
200199
ExprT::UnOp(un_op, arg) => {
201200
self.check_rvalue(env, arg);
202201
if self.check_types
203-
&& let Some(arg_ty) = self.infer_rvalue(env, arg)
202+
&& let Some(arg_ty) = self.infer_expr(env, arg)
204203
{
205204
match un_op {
206205
UnOp::Not => match &env.vtype_whnf(arg_ty.clone().into()).val {
@@ -219,7 +218,7 @@ impl<'a> Checker<'a> {
219218
self.check_rvalue(env, rhs);
220219
if self.check_types
221220
&& let (Some(lhs_ty), Some(rhs_ty)) =
222-
(self.infer_rvalue(env, lhs), self.infer_rvalue(env, rhs))
221+
(self.infer_expr(env, lhs), self.infer_expr(env, rhs))
223222
{
224223
let check_eq = {
225224
let lhs_ty = lhs_ty.clone();
@@ -387,7 +386,7 @@ impl<'a> Checker<'a> {
387386
self.check_rvalue(env, v);
388387
if self.check_types
389388
&& let (Some(x_ty), Some(v_ty)) =
390-
(self.infer_lvalue(env, x), self.infer_rvalue(env, v))
389+
(self.infer_expr(env, x), self.infer_expr(env, v))
391390
{
392391
self.check_type_eq(env, v_ty.into(), x_ty.into());
393392
}

0 commit comments

Comments
 (0)