Merge pull request #1804 from herd/fix-new-location-in-postcondition

[herd] Fix "Post-condition introduces new symbolic location" error.

Symbols referred from code are part of symbols defined by a test and can appear in the post-condition.

More specifically, the following test is now accepted again:
```
X86_64 A012
(* Implicit initialsation of int x=0; *)
{ }
  P0         ;
 movl $1,(x) ;
forall [x]=1
```
Note: the error was introduced by PR #1607 to flag missing symbols in post-condition, a very useful check. Unfortunately, the X86 and X86_64 tests generated by **diy7** were rejected. This problem is now fixed.

Author: maranget

herd/test_herd.ml

@@ -129,6 +129,15 @@ module Make(A:Arch_herd.S) =
             | Some c -> add_constant_symbols acc c) in
       ConstrGen.fold_constr add_atom constr acc
 
+    let locs_in_ins =
+      A.pseudo_fold
+        (A.fold_addrs
+           (fun v acc -> add_constant_symbols acc v))
+
+    let locs_in_code =
+       List.fold_left
+          (fun locs (_,code) -> List.fold_left locs_in_ins locs code)
+
     let check_post_condition_symbols_exist test =
       let { MiscParser.init; condition; prog; _ } = test in
       let init_symbols =
@@ -137,10 +146,11 @@ module Make(A:Arch_herd.S) =
             let acc = add_location_symbols loc acc in
             add_constant_symbols acc v)
           StringSet.empty init in
+      let code_symbols = locs_in_code init_symbols prog in
       let prog_init_symbols =
         List.fold_left
           (fun acc lbl -> StringSet.add (Label.Full.pp lbl) acc)
-           init_symbols (A.all_labels prog) in
+           code_symbols (A.all_labels prog) in
       let postcondition_symbols =
         add_postcondition_symbols condition StringSet.empty in
       let unexpected_symbols =
@@ -246,7 +256,7 @@ module Make(A:Arch_herd.S) =
         match v with
         | A.V.Val (Symbolic (Virtual {name=Symbol.Label(p,s); _}))
           -> begin
-          if not (Label.Map.mem s prog) then 
+          if not (Label.Map.mem s prog) then
             Warn.user_error
               "Label %s not found on P%d, yet it is used in the initialization list" s p end
         | _ -> ()) init ;

herd/tests/instructions/X86_64/A012.litmus

@@ -0,0 +1,7 @@
+X86_64 A012
+(* Implicit initialsation of int x=0; *)
+{ }
+  P0         ;
+ movl $1,(x) ;
+forall [x]=1
+

herd/tests/instructions/X86_64/A012.litmus.expected

@@ -0,0 +1,10 @@
+Test A012 Required
+States 1
+[x]=1;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall ([x]=1)
+Observation A012 Always 1 0
+Hash=3b021e40517dcff1f1cb8894d645b677
+