Revert unnecessary changes

model-checking · Apr 14, 2023 · 24ca8d2 · 24ca8d2
1 parent 13e5f09
commit 24ca8d2
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 45 deletions.
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
@@ -131,7 +131,7 @@ pub enum ExprValue {
     StringConstant {
         s: InternedString,
     },
-    /// Struct initializer
+    /// Struct initializer  
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     Struct {
         values: Vec<Expr>,
@@ -142,7 +142,7 @@ pub enum ExprValue {
     },
     /// `(typ) self`. Target type is in the outer `Expr` struct.
     Typecast(Expr),
-    /// Union initializer
+    /// Union initializer  
     /// `union foo the_foo = >>> {.field = value } <<<`
     Union {
         value: Expr,
@@ -681,7 +681,7 @@ impl Expr {
         expr!(StatementExpression { statements: ops }, typ)
     }
 
-    /// Internal helper function for Struct initalizer
+    /// Internal helper function for Struct initalizer  
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// ALL fields must be given, including padding
     fn struct_expr_with_explicit_padding(
@@ -698,7 +698,7 @@ impl Expr {
         expr!(Struct { values }, typ)
     }
 
-    /// Struct initializer
+    /// Struct initializer  
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -719,7 +719,7 @@ impl Expr {
             "Error in struct_expr; mismatch in number of fields and components.\n\t{typ:?}\n\t{components:?}"
         );
 
-        // Check that each formal field has a value
+        // Check that each formal field has an value
         for field in non_padding_fields {
             let field_typ = field.field_typ().unwrap();
             let value = components.get(&field.name()).unwrap();
@@ -764,7 +764,7 @@ impl Expr {
         Expr::struct_expr_from_values(typ, values, symbol_table)
     }
 
-    /// Struct initializer
+    /// Struct initializer  
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -800,7 +800,7 @@ impl Expr {
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
     }
 
-    /// Struct initializer
+    /// Struct initializer  
     /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<`
     /// Note that padding fields should be explicitly given.
     /// This would be used when the values and padding have already been combined,
@@ -859,7 +859,7 @@ impl Expr {
         self.transmute_to(t, st)
     }
 
-    /// Union initializer
+    /// Union initializer  
     /// `union foo the_foo = >>> {.field = value } <<<`
     pub fn union_expr<T: Into<InternedString>>(
         typ: Type,

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -231,17 +231,6 @@ impl<'tcx> TypeOrVariant<'tcx> {
             }
         }
     }
-
-    #[allow(dead_code)]
-    pub fn expect_gen_variant(&self) -> VariantIdx {
-        match self {
-            TypeOrVariant::Type(t) => panic!("expect a generator but found type: {t:?}"),
-            TypeOrVariant::Variant(v) => {
-                panic!("expect a generator but found variant: {v:?}")
-            }
-            TypeOrVariant::GeneratorVariant(v) => *v,
-        }
-    }
 }
 
 impl<'tcx> GotocCtx<'tcx> {

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -31,30 +31,27 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?stmt, kind=?stmt.kind, "handling_statement");
         let location = self.codegen_span(&stmt.source_info.span);
         match &stmt.kind {
-            StatementKind::Assign(box (lhs, rhs)) => {
-                let lty = self.place_ty(lhs);
-                let rty = self.rvalue_ty(rhs);
+            StatementKind::Assign(box (l, r)) => {
+                let lty = self.place_ty(l);
+                let rty = self.rvalue_ty(r);
                 // we ignore assignment for all zero size types
                 if self.is_zst(lty) {
                     Stmt::skip(location)
+                } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() {
+                    // implicit address of a function pointer, e.g.
+                    // let fp: fn() -> i32 = foo;
+                    // where the reference is implicit.
+                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
+                        .goto_expr
+                        .assign(self.codegen_rvalue(r, location).address_of(), location)
+                } else if rty.is_bool() {
+                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
+                        .goto_expr
+                        .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location)
                 } else {
-                    let rvalue = self.codegen_rvalue(rhs, location);
-                    if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() {
-                        // implicit address of a function pointer, e.g.
-                        // let fp: fn() -> i32 = foo;
-                        // where the reference is implicit.
-                        unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs))
-                            .goto_expr
-                            .assign(rvalue.address_of(), location)
-                    } else if rty.is_bool() {
-                        unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs))
-                            .goto_expr
-                            .assign(rvalue.cast_to(Type::c_bool()), location)
-                    } else {
-                        unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs))
-                            .goto_expr
-                            .assign(rvalue, location)
-                    }
+                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
+                        .goto_expr
+                        .assign(self.codegen_rvalue(r, location), location)
                 }
             }
             StatementKind::Deinit(place) => self.codegen_deinit(place, location),
@@ -206,6 +203,8 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Create a statement that sets the variable discriminant to the value that corresponds to the
+    /// variant index.
     pub fn codegen_set_discriminant(
         &mut self,
         dest_ty: Ty<'tcx>,

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1101,12 +1101,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     variants,
                     ..
                 } => (tag_field, variants),
-                Variants::Multiple { .. } => unreachable!(
-                    "Expected generator with direct encoding, got: {type_and_layout:?}"
-                ),
-                Variants::Single { .. } => unreachable!(
-                    "Expected generator with multiple variants, got: {type_and_layout:?}"
-                ),
+                _ => unreachable!("Generators have more than one variant and use direct encoding"),
             };
             // generate a struct for the direct fields of the layout (fields that don't occur in the variants)
             let direct_fields = DatatypeComponent::Field {