Merge pull request #1596 from goblint/yaml-witness-invariant-set-widen-token

Add YAML `invariant_set` indices to widening tokens

Author: sim642

src/analyses/apron/relationAnalysis.apron.ml

@@ -690,7 +690,7 @@ struct
           Priv.lock ask ctx.global st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask ctx.global ctx.sideg st m
             ) st addr
@@ -701,7 +701,7 @@ struct
       Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped
     | Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp = e; uuids} ->
+    | Events.Unassume {exp = e; tokens} ->
       let e_orig = e in
       let ask = Analyses.ask_of_ctx ctx in
       let e = replace_deref_exps ctx.ask e in
@@ -737,7 +737,7 @@ struct
 
       (* TODO: parallel write_global? *)
       let st =
-        WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+        WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list tokens) (fun () ->
             VH.fold (fun v v_in st ->
                 (* TODO: is this sideg fine? *)
                 write_global ask ctx.global ctx.sideg st v v_in
@@ -771,7 +771,7 @@ struct
       let new_value = RD.join old_value st in
       PCU.RH.replace results ctx.node new_value;
     end;
-    WideningTokens.with_local_side_tokens (fun () ->
+    WideningTokenLifter.with_local_side_tokens (fun () ->
         Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 

src/analyses/base.ml

@@ -445,7 +445,7 @@ struct
     in
     if M.tracing then M.tracel "sync" "sync multi=%B earlyglobs=%B" multi !earlyglobs;
     if !earlyglobs || multi then
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           Priv.sync (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) ctx.local reason
         )
     else
@@ -3060,7 +3060,7 @@ struct
     (* Perform actual [set]-s with final unassumed values.
        This invokes [Priv.write_global], which was suppressed above. *)
     let e_d' =
-      WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+      WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () ->
           CPA.fold (fun x v acc ->
               let addr: AD.t = AD.of_mval (x, `NoOffset) in
               set ~ctx ~invariant:false acc addr x.vtype v
@@ -3079,7 +3079,7 @@ struct
           Priv.lock ask (priv_getg ctx.global) st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m
             ) st addr
@@ -3093,8 +3093,8 @@ struct
       set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
     | Events.Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp; uuids} ->
-      Timing.wrap "base unassume" (unassume ctx exp) uuids
+    | Events.Unassume {exp; tokens} ->
+      Timing.wrap "base unassume" (unassume ctx exp) tokens
     | Events.Longjmped {lval} ->
       begin match lval with
         | Some lval ->

src/analyses/mCP.ml

@@ -156,20 +156,20 @@ struct
     else
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
-  let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) =
+  let do_sideg ctx (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) =
     let side_one v dts =
       let side_one_ts ts d =
         (* Do side effects with the tokens that were active at the time.
            Transfer functions have exited the with_side_token wrappers by now. *)
-        let old_side_tokens = !WideningTokens.side_tokens in
-        WideningTokens.side_tokens := ts;
+        let old_side_tokens = !WideningTokenLifter.side_tokens in
+        WideningTokenLifter.side_tokens := ts;
         Fun.protect (fun () ->
             ctx.sideg v @@ fold_left G.join (G.bot ()) d
           ) ~finally:(fun () ->
-            WideningTokens.side_tokens := old_side_tokens
+            WideningTokenLifter.side_tokens := old_side_tokens
           )
       in
-      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokens.TS.equal dts
+      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokenLifter.TS.equal dts
     in
     iter (uncurry side_one) @@ group_assoc_eq V.equal xs
 
@@ -355,7 +355,7 @@ struct
       | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
-      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
+      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokenLifter.side_tokens, g)) :: !sides)
       | None -> (fun v g       -> failwith ("Cannot \"sideg\" in " ^ tfname ^ " context."))
     in
     let emit = match emits with

src/analyses/unassumeAnalysis.ml

@@ -29,7 +29,7 @@ struct
 
   type inv = {
     exp: Cil.exp;
-    uuid: string;
+    token: WideningToken.t;
   }
 
   let invs: inv NH.t = NH.create 100
@@ -90,7 +90,7 @@ struct
       let uuid = entry.metadata.uuid in
       let target_type = YamlWitnessType.EntryType.entry_type entry.entry_type in
 
-      let unassume_nodes_invariant ~loc ~nodes inv =
+      let unassume_nodes_invariant ~loc ~nodes ?i inv =
         let msgLoc: M.Location.t = CilLocation loc in
         match InvariantParser.parse_cabs inv with
         | Ok inv_cabs ->
@@ -101,7 +101,7 @@ struct
               match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
-                NH.add invs n {exp = inv_exp; uuid}
+                NH.add invs n {exp = inv_exp; token = (uuid, i)}
               | Error e ->
                 M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                 M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -154,7 +154,7 @@ struct
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then
                       NH.replace pre_invs n (EH.create 10);
-                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; uuid}
+                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)}
                   | Error e ->
                     M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                     M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -189,42 +189,42 @@ struct
 
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
-        let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
+        let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
           let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt location_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
+        let unassume_loop_invariant ~i (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
           let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt loop_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
+        let validate_invariant i (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
           let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
           match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with
           | true, LocationInvariant x ->
-            unassume_location_invariant x
+            unassume_location_invariant ~i x
           | true, LoopInvariant x ->
-            unassume_loop_invariant x
+            unassume_loop_invariant ~i x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
         in
 
-        List.iter validate_invariant invariant_set.content
+        List.iteri validate_invariant invariant_set.content
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
@@ -262,9 +262,9 @@ struct
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
-          let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in
-          ctx.emit (Unassume {exp = e; uuids});
-          List.iter WideningTokens.add uuids
+          let tokens = x.token :: List.map (fun {token; _} -> token) xs in
+          ctx.emit (Unassume {exp = e; tokens});
+          List.iter WideningTokenLifter.add tokens
         )
       );
       ctx.local

src/domains/events.ml

@@ -14,7 +14,7 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
-  | Unassume of {exp: CilType.Exp.t; uuids: string list}
+  | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
@@ -45,5 +45,5 @@ let pretty () = function
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
-  | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
+  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval

src/framework/control.ml

@@ -39,7 +39,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
-      |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+      |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)
       |> lift true (module LongjmpLifter.Lifter)
       |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
     )

src/goblint_lib.ml

@@ -180,7 +180,8 @@ module SpecLifters = SpecLifters
 module LongjmpLifter = LongjmpLifter
 module RecursionTermLifter = RecursionTermLifter
 module ContextGasLifter = ContextGasLifter
-module WideningTokens = WideningTokens
+module WideningToken = WideningToken
+module WideningTokenLifter = WideningTokenLifter
 
 module WitnessConstraints = WitnessConstraints
 

src/lifters/wideningToken.ml

@@ -0,0 +1,16 @@
+(** Widening token for {!WideningTokenLifter}. *)
+
+module Uuid =
+struct
+  include Basetype.RawStrings
+  let name () = "uuid"
+end
+
+module Index =
+struct
+  include Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)
+  let name () = "index"
+end
+
+(* Change to variant type if need other tokens than witness UUIDs. *)
+include Printable.Prod (Uuid) (Index)

src/lifters/wideningTokens.ml renamed to src/lifters/wideningTokenLifter.ml

@@ -6,8 +6,7 @@
 
     @see <http://www2.in.tum.de/bib/files/mihaila13widening.pdf> Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *)
 
-(** Widening token. *)
-module Token = Basetype.RawStrings (* Change to variant type if need other tokens than witness UUIDs. *)
+module Token = WideningToken
 
 (** Widening token set. *)
 module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)

tests/regression/56-witness/64-apron-unassume-set-tokens.c

@@ -0,0 +1,18 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 64-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens
+#include <assert.h>
+// Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing.
+// Copied & extended from 56-witness/12-apron-unassume-branch.
+int main() {
+  int i = 0;
+  while (i < 100) {
+    i++;
+  }
+  assert(i == 100);
+
+  int j = 0;
+  while (j < 100) {
+    j++;
+  }
+  assert(j == 100);
+  return 0;
+}

tests/regression/56-witness/64-apron-unassume-set-tokens.yml

@@ -0,0 +1,59 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "0.1"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''64-apron-unassume-set-tokens.c'''
+    task:
+      input_files:
+      - 64-apron-unassume-set-tokens.c
+      input_file_hashes:
+        64-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: 99LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: 99LL - (long long )j >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 64-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: (long long )j >= 0LL
+      format: c_expression

tests/regression/56-witness/dune

@@ -21,7 +21,8 @@
      (run %{update_suite} hh-ex3 -q)
      (run %{update_suite} bh-ex1-poly -q)
      (run %{update_suite} apron-unassume-precheck -q)
-     (run %{update_suite} apron-tracked-global-annot -q)))))
+     (run %{update_suite} apron-tracked-global-annot -q)
+     (run %{update_suite} apron-unassume-set-tokens -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml)))