Merge pull request #823 from xldenis/sound-ghost-type

Avoid unsound type definitions with ghost fields

Author: voidc

creusot-contracts/src/logic/ops.rs

@@ -33,10 +33,9 @@ impl<T> IndexLogic<Int> for Ghost<Seq<T>> {
     type Item = T;
 
     #[logic]
-    #[trusted]
-    #[open(self)]
-    #[creusot::builtins = "seq.Seq.get"]
-    fn index_logic(self, _: Int) -> Self::Item {
-        absurd
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, ix: Int) -> Self::Item {
+        pearlite! { (*self)[ix] }
     }
 }

creusot/src/backend/ty.rs

@@ -372,7 +372,7 @@ fn build_ty_decl<'tcx>(
                 .fields
                 .iter()
                 .map(|f| {
-                    let ty = field_ty(ctx, names, param_env, f, substs);
+                    let ty = field_ty(ctx, names, param_env, did, f, substs);
                     Field { ty, ghost: false }
                 })
                 .collect();
@@ -410,14 +410,34 @@ fn field_ty<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     names: &mut CloneMap<'tcx>,
     param_env: ParamEnv<'tcx>,
+    adt_did: DefId,
     field: &FieldDef,
     substs: SubstsRef<'tcx>,
 ) -> MlT {
     let ty = field.ty(ctx.tcx, substs);
     let ty = ctx.try_normalize_erasing_regions(param_env, ty).unwrap_or(ty);
+
+    if !validate_field_ty(ctx, adt_did, ty) {
+        ctx.crash_and_error(ctx.def_span(field.did), "Illegal use of the Ghost type")
+    }
+
     translate_ty_inner(TyTranslation::Declaration, ctx, names, ctx.def_span(field.did), ty)
 }
 
+fn validate_field_ty<'tcx>(ctx: &mut Why3Generator<'tcx>, adt_did: DefId, ty: Ty<'tcx>) -> bool {
+    let tcx = ctx.tcx;
+    let bg = ctx.binding_group(adt_did);
+
+    !ty.walk().filter_map(ty::GenericArg::as_type).any(|ty| {
+        util::is_ghost_ty(tcx, ty)
+            && ty.walk().filter_map(ty::GenericArg::as_type).any(|ty| match ty.kind() {
+                TyKind::Adt(adt_def, _) => bg.contains(&adt_def.did()),
+                // TyKind::Param(_) => true,
+                _ => false,
+            })
+    })
+}
+
 pub(crate) fn translate_accessor(
     ctx: &mut Why3Generator<'_>,
     adt_did: DefId,
@@ -457,7 +477,8 @@ pub(crate) fn translate_accessor(
     let acc_name = format!("{}_{}", variant.name.as_str().to_ascii_lowercase(), field.name);
 
     let param_env = ctx.param_env(adt_did);
-    let target_ty = field_ty(ctx, &mut names, param_env, &variant.fields[ix.into()], substs);
+    let target_ty =
+        field_ty(ctx, &mut names, param_env, adt_did, &variant.fields[ix.into()], substs);
 
     let variant_arities: Vec<_> = adt_def
         .variants()

creusot/src/util.rs

@@ -75,6 +75,15 @@ pub(crate) fn is_ghost_closure<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> Option<
     } else { None }
 }
 
+pub(crate) fn is_ghost_ty<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool {
+    let r: Option<bool> = try {
+        let adt = ty.ty_adt_def()?;
+        let builtin = get_builtin(tcx, adt.did())?;
+        builtin.as_str() == "prelude.Ghost.ghost_ty"
+    };
+    r.unwrap_or(false)
+}
+
 pub(crate) fn is_spec_logic(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "spec_logic"]).is_some()
 }

creusot/tests/should_fail/bug/436.rs renamed to creusot/tests/should_fail/bug/436_0.rs

@@ -1,5 +1,5 @@
 error[creusot]: called Logic function in Ghost context "creusot_contracts::__stubs::fin"
-  --> 436.rs:10:5
+  --> 436_0.rs:10:5
    |
 10 |     pearlite! { *(^x).g }
    |     ^^^^^^^^^^^^^^^^^^^^^

creusot/tests/should_fail/bug/436.stderr renamed to creusot/tests/should_fail/bug/436_0.stderr

@@ -1,5 +1,5 @@
 error[creusot]: called Logic function in Ghost context "prophecy"
-  --> 436-1.rs:15:21
+  --> 436_1.rs:15:21
    |
 15 |     b.g = ghost! { !prophecy(b) };
    |                     ^^^^^^^^

creusot/tests/should_fail/bug/436-1.rs renamed to creusot/tests/should_fail/bug/436_1.rs

@@ -0,0 +1,18 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+enum Bad<'a> {
+    None,
+    Some(Ghost<&'a mut Bad<'a>>),
+}
+
+pub fn test_bad() {
+    let mut x = Bad::None;
+    let m = &mut x;
+    let g = ghost!(m);
+    *m = Bad::Some(ghost!(*g));
+    proof_assert!(*m == Bad::Some(g));
+    proof_assert!(^*g == ^m);
+    let _ = m;
+    proof_assert!(^*g == Bad::Some(g));
+}

creusot/tests/should_fail/bug/436-1.stderr renamed to creusot/tests/should_fail/bug/436_1.stderr

@@ -0,0 +1,8 @@
+error[creusot]: Illegal use of the Ghost type
+ --> 436_2.rs:6:10
+  |
+6 |     Some(Ghost<&'a mut Bad<'a>>),
+  |          ^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to previous error
+

creusot/tests/should_fail/bug/436_2.rs

@@ -7,7 +7,7 @@
 <path name=".."/><path name="100doors.mlcfg"/>
 <theory name="C100doors_F" proved="true">
  <goal name="f&#39;vc" expl="VC for f" proved="true">
- <proof prover="1"><result status="valid" time="0.220000" steps="45798"/></proof>
+ <proof prover="1"><result status="valid" time="0.220000" steps="45466"/></proof>
  </goal>
 </theory>
 </file>