- minor fixes in error reporting

- optimize ep term generation
- make matching filters for user-defined term generators more restrictive
- improve command line option documentation

src/formulas/grass.ml

@@ -119,7 +119,7 @@ module TermMap = Map.Make(struct
 type filter =
   | FilterTrue
   | FilterSymbolNotOccurs of symbol
-  | FilterTermNotOccurs of term
+  | FilterNameNotOccurs of string * arity
   | FilterGeneric of (subst_map -> term -> bool)
 
 (** matching guards for term generators *)
@@ -294,7 +294,12 @@ let extract_name smt ann =
 let rec extract_src_pos = function
   | SrcPos pos :: _ -> Some pos
   | _ :: ann -> extract_src_pos ann
-  | [] -> None  
+  | [] -> None
+
+let rec extract_label = function
+  | Label lbl :: _ -> Some lbl
+  | _ :: ann -> extract_label ann
+  | [] -> None
 
 let rec pr_form ppf = function
   | Binder (b, vs, f, a) -> 
@@ -467,11 +472,14 @@ let rec pr_form ppf = function
 and pr_annot ppf a =
   let name = extract_name false a in
   let pos = extract_src_pos a in
-  (match name, pos with
-  | "", None -> fprintf ppf ""
-  | "", Some pos -> fprintf ppf "@ /* %s */" (string_of_src_pos pos)
-  | n, Some pos -> fprintf ppf "@ /* %s: %s */" (string_of_src_pos pos) n
-  | n, None -> fprintf ppf "@ /* %s */" n)
+  let lbl = extract_label a in
+  (match name, pos, lbl with
+  | "", None, None -> fprintf ppf ""
+  | "", Some pos, None -> fprintf ppf "@ /* %s */" (string_of_src_pos pos)
+  | "", Some pos, Some lbl -> fprintf ppf "@ /* %s -> %s */" (string_of_ident lbl) (string_of_src_pos pos)
+  | n, Some pos, None -> fprintf ppf "@ /* %s: %s */" (string_of_src_pos pos) n
+  | n, Some pos, Some lbl -> fprintf ppf "@ /* %s -> %s: %s */" (string_of_ident lbl) (string_of_src_pos pos) n
+  | n, None, _ -> fprintf ppf "@ /* %s */" n)
 
 
 and pr_ands ppf = function

src/formulas/grassUtil.ml

@@ -694,8 +694,8 @@ let subst_id subst_map f =
         | FilterSymbolNotOccurs (FreeSym id) ->
             (try FilterSymbolNotOccurs (FreeSym (IdMap.find id subst_map))
             with Not_found -> f)
-        | FilterTermNotOccurs t ->
-            FilterTermNotOccurs (subt t)
+        (*| FilterTermNotOccurs t ->
+            FilterTermNotOccurs (subt t)*)
         | _ -> f
       in
       Match (t1, f1)
@@ -757,8 +757,8 @@ let subst_consts subst_map f =
                             FilterSymbolNotOccurs (FreeSym id1)
                         | _ -> f
                       with Not_found -> f)
-                  | FilterTermNotOccurs t ->
-                      FilterTermNotOccurs (subst_consts_term subst_map t)
+                  (*| FilterTermNotOccurs t ->
+                      FilterTermNotOccurs (subst_consts_term subst_map t)*)
                   | _ -> f
                   in
                   sorted_fv_term_acc sign t1, Match (t1, f1) :: guards1)

src/formulas/slUtil.ml

@@ -48,13 +48,13 @@ let mk_sep_plus ?pos a b =
   | _, _ -> SepOp (SepPlus, a, b, pos)
 let mk_sep_incl ?pos a b = SepOp (SepIncl, a, b, pos)
 let mk_atom ?pos s args = Atom (s, args, pos)
-let mk_emp = mk_atom Emp []
+let mk_emp pos = mk_atom ?pos:pos Emp []
 let mk_cell ?pos t = mk_atom ?pos:pos Region [GrassUtil.mk_setenum [t]]
 let mk_region ?pos r = mk_atom ?pos:pos Region [r]
 let mk_pred ?pos p ts = mk_atom ?pos:pos (Pred p) ts
 let mk_pts ?pos f a b = 
   mk_sep_star ?pos:pos (mk_eq ?pos:pos (GrassUtil.mk_read f a) b) (mk_cell ?pos:pos a)
-let mk_sep_star_lst ?pos:pos args = List.fold_left (mk_sep_star ?pos:pos) mk_emp args
+let mk_sep_star_lst ?pos:pos args = List.fold_left (mk_sep_star ?pos:pos) (mk_emp None) args
 let mk_exists ?pos vs f = Binder (Grass.Exists, vs, f, pos)
 let mk_forall ?pos vs f = Binder (Grass.Forall, vs, f, pos)
 

src/frontends/spl/splTranslator.ml

@@ -671,7 +671,7 @@ let convert cu =
     in
     let rec convert_expr locals = function
       | Null _ -> FOL_term (GrassUtil.mk_null, LocType)
-      | Emp _ -> SL_form SlUtil.mk_emp
+      | Emp pos -> SL_form (SlUtil.mk_emp (Some pos))
       | Setenum (ty, es, pos) ->
           let ts, ty = 
             List.fold_right (fun e (ts, ty) ->
@@ -980,11 +980,11 @@ let convert cu =
                               then FilterSymbolNotOccurs (FreeSym sym)
                               else FilterTrue
                           | flt -> flt)
-                    | App (Read, (App (FreeSym sym, [], _) as t :: _ as ts), _) ->
+                    | App (Read, (App (FreeSym sym, [], srt) :: _ as ts), _) ->
                         (function 
                           | FilterTrue ->
                               if ce_occur_below ts
-                              then FilterTermNotOccurs t
+                              then FilterNameNotOccurs (GrassUtil.name sym, ([], srt))
                               else FilterTrue
                           | flt -> flt)
                     | _ -> function flt -> flt)

src/main/config.ml

@@ -55,28 +55,28 @@ let optSelfFrame = ref false
 
 
 let cmd_options =
-  [("-basedir", Arg.Set_string base_dir, "<string>  Base directory for resolving include directives");
-   ("-procedure", Arg.String (fun p -> procedure := Some p), "<string>  Only check the specified procedure");
+  [("-basedir", Arg.Set_string base_dir, "<string>  Base directory for resolving include directives. Default: current working directory\n\nOptions for controlling error reporting and debug output:");
+   ("-v", Arg.Unit Debug.more_verbose, " Display more messages");
+   ("-q", Arg.Unit Debug.less_verbose, " Display fewer messages");
+   ("-stats", Arg.Set print_stats, " Print statistics");
+   ("-lint", Arg.Set flycheck_mode, " Print single line error messages for on-the-fly checking");
    ("-model", Arg.Set_string model_file, "<file>  Produce counterexample model for the first failing verification condition");
-   ("-trace", Arg.Set_string trace_file, "<file> Produce counterexample trace for the first failing verification condition");
-   ("-lint", Arg.Set flycheck_mode, " Print error messages for on-the-fly checking");
+   ("-trace", Arg.Set_string trace_file, "<file>  Produce counterexample trace for the first failing verification condition");
    ("-dumpghp", Arg.Set_int dump_ghp, "<num>  Print intermediate program after specified simplification stage (num=0,1,2,3)");
    ("-dumpvcs", Arg.Set dump_smt_queries, " Generate SMT-LIB 2 files for all verification conditions");
-   ("-core", Arg.Set unsat_cores, " Produce unsat cores with every unsat SMT query");
-   ("-noverify", Arg.Clear verify, " Do not check the generated verification conditions");
-   ("-robust", Arg.Set robust, " Continue even if some verification condition cannot be checked");
+   ("-dumpcores", Arg.Set unsat_cores, " Produce unsat cores with every unsat SMT query\n\nOptions for controlling what is checked:");
+   ("-procedure", Arg.String (fun p -> procedure := Some p), "<string>  Only check the specified procedure");
+   ("-noverify", Arg.Clear verify, " Only type-check the program and generate verification conditions without checking");
+   ("-robust", Arg.Set robust, " Continue even if some verification condition cannot be checked\n\nOptions for controlling verification condition generation:");
+   ("-types", Arg.Set keep_types, " Keep type information when translating to intermediate representation");
+   ("-nomodifiesopt", Arg.Clear opt_field_mod, " Disable mod set analysis optimization for fields\n\nOptions for controlling the GRASS prover:");
+   ("-noreach", Arg.Clear with_reach_axioms, " Omit axioms for reachability predicates");
+   ("-noep", Arg.Clear with_ep, " Omit axioms for entry points");
+   ("-noinst", Arg.Clear instantiate, " Let the SMT solver deal with the quantifiers without prior instantiation");
+   ("-nostratify", Arg.Clear stratify, " Instantiate quantifiers that satisfy stratified sort restrictions\n\nOptions for controlling backend solver:");
    ("-smtsolver", Arg.Set_string smtsolver, "<solver> Choose SMT solver (z3, cvc4, cvc4mf), e.g., 'z3+cvc4mf'");
    ("-smtpatterns", Arg.Set smtpatterns, " Always add pattern annotations to quantifiers in SMT queries");
    ("-smtsets", Arg.Set use_set_theory, " Use solver's set theory to encode sets (if supported)");
-   ("-smtarrays", Arg.Set encode_fields_as_arrays, " Use array theory of SMT solver to encode fields");
-   ("-types", Arg.Set keep_types, " Keep type information in intermediate program");
-   ("-noreach", Arg.Clear with_reach_axioms, " Omit axioms for reachability predicates");
-   ("-noep", Arg.Clear with_ep, " Omit entry points");
-   ("-noinst", Arg.Clear instantiate, " Let the SMT solver deal with the quantifiers without prior instantiation");
-   ("-nostratify", Arg.Clear stratify, " Instantiate quantifiers that satisfy stratified sort restrictions");
-   ("-noOptFieldMod", Arg.Clear opt_field_mod, " Disable mod set analysis optimization for fields");
+   ("-smtarrays", Arg.Set encode_fields_as_arrays, " Use solver's array theory to encode fields\n");
    (*("-optSelfFrame", Arg.Set optSelfFrame, " enable generation of self-framing clauses for SL predicates");*)
-   ("-stats", Arg.Set print_stats, " Print statistics");
-   ("-v", Arg.Unit Debug.more_verbose, " Display more messages");
-   ("-q", Arg.Unit Debug.less_verbose, " Display less messages");
   ]

src/main/grasshopper.ml

@@ -11,7 +11,7 @@ let usage_message =
   " <input file> [options]\n"
 
 let cmd_line_error msg =
-  Arg.usage Config.cmd_options usage_message;
+  Arg.usage (Arg.align Config.cmd_options) usage_message;
   failwith ("Command line option error: " ^ msg)
 
 (** Output JSON file with error trace *)

src/prover/instGen.ml

@@ -131,14 +131,19 @@ let generate_terms generators ground_terms =
           | App (_, ts, _) -> List.for_all not_occurs ts
           | _ -> true
         in not_occurs t
-    | FilterTermNotOccurs t1 ->
-        let ts = ground_terms_term t in
-        let res = not (TermSet.mem t1 ts) in
-        if false && res then begin
-          print_endline ("Filtering " ^ string_of_term t ^ " for occurrence of " ^ string_of_term t1);
-          print_endline ("Result: " ^ string_of_bool res);
-        end;
-        res
+    | FilterNameNotOccurs (name, (arg_srts, res_srt)) ->
+        let rec not_occurs = function
+          | App (FreeSym (name1, _), ts, res_srt1) ->
+              let ok =
+                try
+                  name1 <> name ||
+                  res_srt1 <> res_srt ||
+                  List.fold_left2 (fun acc t1 srt -> acc || sort_of t1 <> srt) false ts arg_srts 
+                with Invalid_argument _ -> true
+              in ok && List.for_all not_occurs ts
+          | App (_, ts, _) -> List.for_all not_occurs ts
+          | _ -> true
+        in not_occurs t
     | FilterGeneric fn -> fn sm t
   in
   let rec generate new_terms old_terms = function

src/prover/model.ml

@@ -660,7 +660,7 @@ let output_graphviz chan model terms =
 	    let label = get_label f in
 	    Printf.fprintf chan "\"%s\" -> \"%s\" [%s]\n" 
 	      (string_of_loc_value l) (string_of_loc_value r) label
-          with Undefined -> ())
+          with Not_found -> ())
           locs)
       flds
   in

src/prover/reduction.ml

@@ -299,8 +299,8 @@ let add_set_axioms fs =
   rev_concat [fs1; Axioms.set_axioms elem_srts]
 
 
-(** Adds theory axioms for the entry point function to formula f.
- ** Assumes that f is typed and that all frame predicates have been reduced. *)
+(** Adds theory axioms for the entry point function to formulas [fs].
+ ** Assumes that all frame predicates have been reduced in formulas [fs]. *)
 let add_ep_axioms fs =
   let gts = ground_terms (smk_and fs) in
   let flds = btwn_fields fs gts in

src/verifier/grassifier.ml

@@ -225,6 +225,8 @@ let elim_sl prog =
       let frame_preds =
         IdSet.fold
           (fun var frames ->
+            if !Config.opt_field_mod && not (IdSet.mem var (modifies_proc prog proc))
+            then frames else
             let old_var = oldify var in
             let srt = (find_global prog var).var_sort in
             mk_framecond (mk_frame init_footprint_set init_alloc_set 

src/verifier/verifier.ml

@@ -240,7 +240,10 @@ let vcgen prog proc =
             let vc_msg = (vc_msg, pp.pp_pos) in
             let f =
               match s.spec_form with
-              | FOL f -> annotate_aux_msg vc_aux_msg (unoldify_form (mk_not f))
+              | FOL f ->
+                  let f1 = unoldify_form (mk_not f) in
+                  let f2 = annotate_aux_msg vc_aux_msg f1 in
+                  f2
               | _ -> failwith "vcgen: found SL formula that should have been desugared"
             in
             let vc_name = 
@@ -263,10 +266,10 @@ let check_proc prog proc =
       if errors <> [] && not !Config.robust then errors else
       let vc_and_preds = add_pred_insts prog vc in
       let labels, vc_and_preds = add_labels vc_and_preds in
-      (*IdMap.iter (fun id (pos, c) -> Printf.printf ("%s -> %s: %s\n") 
-          (string_of_ident id) (string_of_src_pos pos) c) labels;*)
       Debug.info (fun () -> "Checking VC: " ^ vc_name ^ ".\n");
       Debug.debug (fun () -> (string_of_form vc_and_preds) ^ "\n");
+      (*IdMap.iter (fun id (pos, c) -> Printf.printf ("%s -> %s: %s\n") 
+          (string_of_ident id) (string_of_src_pos pos) c) labels;*)
       let sat_means = 
         Str.global_replace (Str.regexp "\n\n") "\n  " (ProgError.error_to_string pp vc_msg)
       in

tests/spl/nested_sl/nested_def.spl

@@ -30,13 +30,17 @@ function nlseg_outer_footprint(x: OuterNode, y: OuterNode)
 function nlseg_inner_footprint(x: OuterNode, y: OuterNode) 
   returns (FP: Set<Loc>)
 {
-  (forall z: Loc :: z in FP ==> z in InnerNode) &&
+  (forall z: Loc, zh: Loc :: z in FP ==>
+   z.head in nlseg_outer_footprint(x, y)) &&
   (forall z: Loc, zh: Loc :: z in FP && zh == z.head ==>
-   (zh in nlseg_outer_footprint(x, y) && z in lseg_footprint(zh.down, null))
-   @(matching z in InnerNode yields z.head)
-   @(matching zh in OuterNode yields zh.down)) &&
+   /* z in lseg_footprint(zh.down, null) */
+   Btwn(inext, zh.down, z, null) && z != null && z in InnerNode
+   @(matching z yields z.head)
+   @(matching zh yields zh.down)) &&
   (forall zh: Loc, z: Loc :: 
-   zh in nlseg_outer_footprint(x, y) && z in lseg_footprint(zh.down, null) ==> z in FP)
+   zh in nlseg_outer_footprint(x, y) &&
+   /*z in lseg_footprint(zh.down, null)*/
+   Btwn(inext, zh.down, z, null) && z != null && z in InnerNode ==> z in FP)
 }
 
 predicate nlseg(x: OuterNode, y: OuterNode, FP: Set<Loc>) {

tests/spl/nested_sl/nested_def2.spl

@@ -0,0 +1,59 @@
+// Structure and predicate declarations for nested lists with head pointers
+
+struct OuterNode {
+  var onext: OuterNode;
+  var down: InnerNode;
+}
+
+struct InnerNode {
+  var inext: InnerNode;
+  var head: OuterNode;
+}
+
+function lseg_footprint(x: InnerNode, y: InnerNode)
+  returns (FP: Set<Loc>)
+{
+  forall z: Loc :: z in FP == (Btwn(inext, x, z, y) && z != y && z in InnerNode)
+}
+
+predicate lseg(x: InnerNode, y: InnerNode, FP: Set<Loc>) {
+  Reach(inext, x, y) && 
+  FP == lseg_footprint(x, y)
+}
+
+function nlseg_outer_footprint(x: OuterNode, y: OuterNode) 
+  returns (FP: Set<Loc>) 
+{
+  forall z: Loc :: z in FP == (Btwn(onext, x, z, y) && z != y && z in OuterNode)
+}
+
+function dinext() returns(m: Map<Loc, Loc>) {
+  forall x: Loc, y: Loc :: x.m == y == (x.down == y || x.inext == y)
+    @(matching x.down yields m[x])
+    @(matching x.inext yields m[x])
+}
+
+function nlseg_inner_footprint(x: OuterNode, y: OuterNode) 
+  returns (FP: Set<Loc>)
+{
+  (forall z: Loc, zh: Loc :: z in FP ==>
+   z.head in nlseg_outer_footprint(x, y)) &&
+  (forall z: Loc, zh: Loc :: z in FP && zh == z.head ==>
+   /* z in lseg_footprint(zh.down, null) */
+   Btwn(inext, zh.down, z, null) && z != null && z in InnerNode
+   @(matching z yields z.head)
+   @(matching zh yields zh.down)) &&
+  (forall zh: Loc, z: Loc :: 
+   zh in nlseg_outer_footprint(x, y) &&
+   /*z in lseg_footprint(zh.down, null)*/
+   Btwn(inext, zh.down, z, null) && z != null && z in InnerNode ==> z in FP)
+}
+
+predicate nlseg(x: OuterNode, y: OuterNode, FP: Set<Loc>) {
+  Reach(onext, x, y) &&
+  (forall u: OuterNode, v: InnerNode ::
+     u in nlseg_outer_footprint(x, y) && v in nlseg_inner_footprint(x, y) && 
+     Reach(inext, u.down, v) ==> v.head == u) &&
+  (forall u: OuterNode :: u in nlseg_outer_footprint(x, y) ==> Reach(inext, u.down, null)) &&
+  FP == nlseg_outer_footprint(x, y) ++ nlseg_inner_footprint(x, y)
+}