added initial fix for atomicity check ghost field bug

nyu-acsys · Nov 7, 2024 · 0f99587 · 0f99587
1 parent 0fbdd7c
commit 0f99587
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git a/lib/frontend/rewrites/rewrites.ml b/lib/frontend/rewrites/rewrites.ml
@@ -2159,9 +2159,17 @@ module AtomicityAnalysis = struct
                     in
                     match symbol with
                     | VarDef v -> Rewriter.return v.var_decl.var_ghost
-                    | _ -> Error.error stmt.stmt_loc "Expected a var_def")
+                    | _ -> Error.error stmt.stmt_loc "Expected a var_def"
+                )
                 | App (Read, [ loc_expr; field_expr ], _) ->
-                    Rewriter.return false
+                    let* field_symbol = Rewriter.find_and_reify loc (Expr.to_qual_ident field_expr) in
+
+                    begin match field_symbol with
+                    | FieldDef f ->
+                      Rewriter.return @@ f.field_is_ghost
+                    | _ ->
+                      Rewriter.return false
+                    end
                 | _ -> Error.error stmt.stmt_loc "Expected a variable")
           in
 

diff --git a/test/bugs/atomicity_check_ghost_field_bug.rav b/test/bugs/atomicity_check_ghost_field_bug.rav
@@ -6,6 +6,7 @@ inv inv1() { true }
 proc p1(x: Ref) 
     requires inv1()
     requires exists nn:Int :: own(x, f1, nn, 1.0)
+    requires exists nn:Int :: own(x, g1, nn, 1.0)
 {
     unfold inv1();
         var f: Int := x.f1;