Merge pull request SoftwareFoundationGroupAtKyotoU#22 from SoftwareFo…

…undationGroupAtKyotoU/fix-by-koba

fix for the problem in handling dereferences

src/flowInference.ml

@@ -1380,20 +1380,14 @@ module RecursiveRefinements = struct
      that code for details.
   *)
   let unfold_to ~with_havoc ?(out_mapping=PPMap.id_map) ~e_id ref_ty root target in_rel out_rel ctxt =
-
     (** Normalize the paths to be havoced/stabilized *)
-    let normalize_havoc pset = P.PathSet.filter (fun p ->
-        PPMap.mem p out_mapping
-      ) pset |> P.PathSet.map (fun p ->
-          PPMap.find p out_mapping
-        )
-    in
     let normalize_ap p =
       if PPMap.mem p out_mapping then
         PPMap.find p out_mapping
       else
         p
     in
+    let normalize_havoc pset = P.PathSet.map normalize_ap pset in
     (** Normalize a substitution, walking into keyed choices as necessary *)
     let rec deep_normalize = function
       | Ap p -> Ap (normalize_ap p)

src/negative-tests/recursive-tests/havoc_alias.imp

@@ -0,0 +1,23 @@
+/*
+    Test whether values in a recursive data structure are havocked correctly at an alias statement.
+*/
+
+create_list() {
+    if _ then
+        null
+    else
+        let tail = create_list() in
+        let tup = (1, tail) in
+        mkref tup
+}
+
+{
+    let l = create_list() in
+    let (_, l1) = *l in
+    {
+        alias(l1 = (*l).1);
+        l1 := (99, null);
+        alias(l1 = (*l).1);
+        assert(1 = 2)
+    }
+}

src/negative-tests/recursive-tests/havoc_deref.imp

@@ -0,0 +1,26 @@
+/*
+    Test whether values in a recursive data structure are havocked correctly at a deref expression.
+    If values (under references whose ownerships are 0) are not havocked correctly, 
+    then our alias assumption 
+    (i.e. two references point to the same memory location = they have the same value) 
+    becomes wrong. The verification will become unsound.
+*/
+
+create_list() {
+    if _ then
+        null
+    else
+        let tail = create_list() in
+        let tup = (1, tail) in
+        mkref tup
+}
+
+{
+    let l = create_list() in
+    let (v1, l1) = *l in
+    {
+        l1 := (999, null);
+        alias(l1 = (*l).1);
+        assert(1 = 2)
+    }
+}

src/positive-tests/recursive-tests/partial_havoc.imp

@@ -0,0 +1,14 @@
+/*
+    Test that we are not havocking everything at let expressions.
+    (Although this cannot be verified in the formalization of ConSORT.)
+*/
+
+{
+    let x = mkref 1 in 
+    let y = x in 
+    let x1 = *x in 
+    let x2 = *x in {
+        y := 2;
+        assert(x1 = x2)
+    }
+}

src/positive-tests/recursive-tests/stable_alias.imp

@@ -0,0 +1,22 @@
+/*
+    Test that nothing is wrongly havocked.
+*/
+
+create_list() {
+    if _ then
+        null
+    else
+        let tail = create_list() in
+        let tup = (1, tail) in
+        mkref tup
+}
+
+{
+    let l = create_list() in
+    let (v1, l1) = *l in
+    {
+        alias(l1 = (*l).1);
+        let (v2, _) = *l in 
+        assert(v2 = 1)
+    }
+}

src/surfaceAst.ml

@@ -82,6 +82,13 @@ let tag_fresh pos t =
 let tag_with i t =
   (i, t)  
 
+(** NK: added **)
+let sanity_check_alias (v1:Paths.path) (v2:Paths.path) =
+  let (root1,_,_)= (v1 :> Paths.root * Paths.steps list * Paths.suff) in
+  let (root2,_,_)= (v2 :> Paths.root * Paths.steps list * Paths.suff) in
+  if root1=root2 then
+    (print_string "Warning: found an alias statement that contains more than one occurrence of the same variable.\nThe analysis may be unsound\n";flush stdout)
+
 (* This rewriting is fairly standard, but it helps to understand some key components.
    First, count determines the number of temporary variables in scope, this ensures
    temporary variables are unique when they are created. This count is thus threaded through
@@ -164,6 +171,7 @@ let rec simplify_expr ?next ~is_tail count e : pos * A.raw_exp =
         |> tag_with i
       )
   | Alias (i,v1,v2) -> 
+     sanity_check_alias v1 v2; (* NK: added *)
     A.Alias (v1,v2, get_continuation ~ctxt:i count)
     |> tag_with i
   | Assert (i,{ op1; cond; op2 }) ->