From ed289bda6f78e3078cbe48e29245f469bf5d1f1a Mon Sep 17 00:00:00 2001
From: Karuna Grewal <karunagrewal98@gmail.com>
Date: Tue, 22 Sep 2020 15:23:10 +0530
Subject: [PATCH] Encode Predicate Definitions for Ghost Types

---
 prusti-viper/src/encoder/encoder.rs      |  8 +++
 prusti-viper/src/encoder/type_encoder.rs | 68 +++++++++++++++++++++++-
 2 files changed, 75 insertions(+), 1 deletion(-)

diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs
index 809576875bf..e20178840f9 100644
--- a/prusti-viper/src/encoder/encoder.rs
+++ b/prusti-viper/src/encoder/encoder.rs
@@ -1289,6 +1289,14 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
         expr
     }
 
+    pub fn get_native_adt_item_name(&self, def_id: DefId) -> String {
+        if config::disable_name_mangling() {
+            self.env.get_item_name(def_id)
+        } else {
+            self.env.get_item_def_path(def_id)
+        }
+    }
+
     pub fn encode_item_name(&self, def_id: DefId) -> String {
         // Rule: the rhs must always have an even number of "$"
         let mut final_name = "m_".to_string();
diff --git a/prusti-viper/src/encoder/type_encoder.rs b/prusti-viper/src/encoder/type_encoder.rs
index 2c024671920..29a3a5e0b32 100644
--- a/prusti-viper/src/encoder/type_encoder.rs
+++ b/prusti-viper/src/encoder/type_encoder.rs
@@ -231,6 +231,59 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
         }
     }
 
+    fn is_ghost_adt(ghost_adt_def: &ty::AdtDef, item_name: String) -> Option<String> {
+        // check if Crate: prusti_contracts and Module: ghost
+        let item_name: Vec<&str> = item_name.split("::").collect();
+        let crate_name = item_name[0];
+        let mod_name = item_name[1];
+        let adt_identifier = item_name[2];
+        if crate_name.eq("prusti_contracts") && mod_name.contains("ghost"){
+            let ghost_name = ghost_adt_def.non_enum_variant().ident.as_str();
+            if ghost_name.contains("Ghost") {
+                return Some(ghost_name.to_string());
+            }
+        }
+        None
+    }
+
+    fn encode_ghost_predicate(ghost_type: &str, value_field: vir::Field) -> Vec<vir::Predicate> {
+        match ghost_type {
+            "GhostInt" => vec![vir::Predicate::new_primitive_value(
+                vir::Type::Int,
+                value_field,
+                None,
+                false
+            )],
+            "GhostBool" => vec![vir::Predicate::new_primitive_value(
+                vir::Type::Bool,
+                value_field,
+                None,
+                false
+            )],
+            "GhostSeq" => vec![vir::Predicate::new_primitive_value(
+                vir::Type::Seq,
+                value_field,
+                None,
+                false
+            )],
+            "GhostSet" => vec![vir::Predicate::new_primitive_value(
+                vir::Type::Set,
+                value_field,
+                None,
+                false
+            )],
+
+            "GhostMultiSet" => vec![vir::Predicate::new_primitive_value(
+                vir::Type::MultiSet,
+                value_field,
+                None,
+                false
+            )],
+            // Is there any marker predicate for undefined viper types?
+            &_ => vec![],
+        }
+    }
+
     pub fn encode_predicate_def(self) -> Vec<vir::Predicate> {
         debug!("Encode type predicate '{:?}'", self.ty);
         // will panic if attempting to encode unsupported type
@@ -302,7 +355,20 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
                                 self.encoder.encode_struct_field(&field_name, field_ty)
                             })
                             .collect();
-                        vec![vir::Predicate::new_struct(typ, fields)]
+                        if adt_def.is_struct() && self.ty.is_zst(self.encoder.env().tcx(), adt_def.did)
+                        {   
+                                let item_name = self.encoder.get_native_adt_item_name(adt_def.did);
+                                if let Some(ghost_type) = TypeEncoder::is_ghost_adt(adt_def, item_name) {
+                                    debug!("Ghost Type {}", ghost_type);
+                                    TypeEncoder::encode_ghost_predicate(&ghost_type, self.encoder.encode_value_field(self.ty))
+                                }
+                                else {
+                                    vec![vir::Predicate::new_struct(typ, fields)]
+                                }
+                        }
+                        else {
+                            vec![vir::Predicate::new_struct(typ, fields)]
+                        }
                     } else {
                         debug!("ADT {:?} has {} variants", adt_def, num_variants);
                         let discriminant_field = self.encoder.encode_discriminant_field();