Unsafe: Raw pointers#148
Conversation
|
I guess this branch should really be rebased? I see |
Yes, I wanted to do that anyway since I started with the raw-ptr branch when the prusti_reals branch had not yet been merged. However, I was only able to complete the rebase today but this PR should only contain changes that are directly related to raw-ptrs now. |
| self.deps.require_dep::<TyUseImpureEnc>(ty_task).unwrap() | ||
| } | ||
|
|
||
| fn encode_offsetof( |
There was a problem hiding this comment.
Why is this in the impure encoder and not ty use?
| let body = Self::handle_bin_op_float(vcx, lhs, rhs, op, float, *prim_res_ty); | ||
| Ok(vcx.mk_function(function, (lhs_decl, rhs_decl), &[], &[], None, Some(body))) | ||
| if let ty::TyKind::RawPtr(_, _) = l_ty.kind() | ||
| && let ty::TyKind::RawPtr(_, _) = r_ty.kind() |
There was a problem hiding this comment.
This huge branch seems unnecessary.
| { | ||
| // TODO other operations | ||
| vir::with_vcx(|vcx| { | ||
| let l_ty_task = RustTyDecomposition::from_ty(l_ty, GParams::empty()); // TODO: Is this really correct |
There was a problem hiding this comment.
Probably not? Test with raw pointers to generic structs (where the generic is a type parameter of the containing method).
| let name_p = "_tmp_ref"; | ||
| start_stmts.push( | ||
| vcx.mk_local_decl_stmt(vir::vir_local_decl! { vcx; [name_p] : Ref }, None), | ||
| ); |
There was a problem hiding this comment.
Why? We have a mechanism for creating temporaries already.
| type EncodeResult<'vir, T, E> = Result<T, EncodeFullError<'vir, E>>; | ||
|
|
||
| struct EncodedRvalue<'vir> { | ||
| pre_assign_stmts: Vec<vir::Stmt<'vir>>, |
There was a problem hiding this comment.
This feels very ad hoc, I would expect we generate these from the PCG annotations already (or at the same place). If we keep it: add a comment and maybe make this and the post folds more coherent.
| // TODO: add raw pointer support | ||
| ty::TyKind::RawPtr(..) => TySpecifics::mk_opaque(()), | ||
| ty::TyKind::RawPtr(..) => { | ||
| TySpecifics::mk_rawptr(LazyRustTy(TySpecifics::new_param_ty(1))) |
There was a problem hiding this comment.
Shouldn't this be 0? A raw pointer does not have a lifetime parameter.
| Ok(update) | ||
| } | ||
|
|
||
| fn encode_offsetof( |
There was a problem hiding this comment.
Same comment as in impure -- why here?
| } | ||
| } | ||
|
|
||
| enum EncodeCfgRes<'vir> { |
There was a problem hiding this comment.
Don't think this really makes sense -- what if you have a conjunction of two accs? The CFG should then encode both, plus updates to local variables, which you can't express using this setup.
accs in Viper can be seen as side-effectful Boolean expressions, so you can accumulate their effects in a vector that's part of Update (and then you don't have to rip open all of the pure encoder).
| IsInfinite(ty::FloatTy), | ||
| FlAbs(ty::FloatTy), | ||
| FlToReal, | ||
| NewReal, |
There was a problem hiding this comment.
| NewReal, | |
| RealNew, |
|
|
||
| pub trait ExprApply<'vir, A: core::marker::Tuple, Ty: CompType> { | ||
| fn expr_apply(self, vcx: &'vir crate::VirCtxt, args: A) -> crate::Expr<'vir, Ty>; | ||
| fn expr_apply_with_frac( |
There was a problem hiding this comment.
Can't you just add more implementations of ExprApply with a different arity?
…d without handling access to p_frac)
2 participants
This PR implements support of reasoning about raw pointers