Merge branch 'feature/lhost-metavar' into 'master'

Metavariables referencing lhost of location read or written

Closes #11

See merge request frama-c/meta!79

README.md

@@ -132,16 +132,21 @@ hold. It can be one of the following :
     `meta lenient` to its contract, in case the invariant needs to be locally
     broken.
 - `\writing` : `P` is to be valid each time the memory is written to in the body
-  of the target function. In this context, `P` can use the `\written`
-  meta-variable, which is the address of the location (or set of locations) being modified.
-  + By default, if `f` calls `g` and `g` has no definition, every state 
+  of the target function. In this context, `P` can use the following metavariables:
+  - `\written`, which is the address of the location (or set of locations) being modified;
+  - `\lhost_written`, which is the address of the base object (i.e with fields and array
+    indices removed) of the location(s) being modified.
+  
+  Prototypes without a definition lead to a special treatment:
+  + By default, if `f` calls `g` and `g` has no definition, every state
     modification that could happen in `g` (according to its `assigns`
     specification) is considered by being **equivalent to assignements in the
     body of `f`** and thus will be checked.
   + In that case, if `g` does not specify a memory footprint, it is **assumed** that it
     respects all related meta-properties.
   + This can be disabled with option `-meta-no-check-ext`
-- `\reading` : symmetrical to `\writing`. `P` can use the `\read` variable.
+- `\reading` : symmetrical to `\writing`. `P` can use the `\read` and `\lhost_read`
+    meta-variables.
   + Undefined callees are checked using their `\from` specification if existing.
 - `\calling` : the property must hold at each function call and can refer to the
   `\called` variable.

meta_annotate.ml

@@ -236,6 +236,8 @@ let addr_of_tlval tlval =
   let typ = Cil.typeOfTermLval tlval in
   Logic_utils.mk_logic_AddrOf tlval typ
 
+let addr_of_tlhost (h,_) = addr_of_tlval (h, TNoOffset)
+
 (* Instantiate properties at any call site, replacing \called by
  * the called function. *)
 class calling_visitor flags all_mp table = object (self)
@@ -337,7 +339,12 @@ class writing_visitor flags all_mp table = object(self)
     | TVar lv, _ when flags.simpl && Meta_simplify.is_not_orig_variable lv -> ()
     | written ->
       let addr_term = addr_of_tlval written in
-      let assoc_list = [("\\written", RepVariable addr_term)] in
+      let base_addr_term = addr_of_tlhost written in
+      let assoc_list =
+        [ "\\written", RepVariable addr_term;
+          "\\lhost_written", RepVariable base_addr_term
+        ]
+      in
       List.iter (self # instantiate ~post stmt assoc_list) mp_todo
 
   (* Inspect function specs to see what it assigns and instantiate the
@@ -402,9 +409,13 @@ class reading_visitor flags all_mp table = object (self)
   inherit context_visitor flags all_mp table
 
   (* Instantiates the property while replacing \read terms *)
-  method reading_instance ?post stmt written =
-    let addr_term = addr_of_tlval written in
-    let assoc_list = [("\\read", RepVariable addr_term)] in
+  method reading_instance ?post stmt read =
+    let addr_term = addr_of_tlval read in
+    let base_addr_term = addr_of_tlhost read in
+    let assoc_list =
+      ["\\read", RepVariable addr_term;
+       "\\lhost_read", RepVariable base_addr_term ]
+    in
     List.iter (self#instantiate ~post stmt assoc_list) mp_todo
 
   (* Hashtable : stmt -> set of tlvals used in it. Used to avoid duplicate

meta_parse.ml

@@ -88,7 +88,9 @@ let mp_contexts = [
 ]
 let mp_metavariables = [
   "\\written";
+  "\\lhost_written";
   "\\read";
+  "\\lhost_read";
   "\\called";
   "\\called_arg";
   "\\func";

tests/meta/lhost.c

+/* run.config
+OPT: @META@ @PRINT@
+*/
+
+struct S {
+  unsigned owner;
+  int data;
+};
+
+extern unsigned current_id;
+
+int read(struct S* s) {
+  if (s->owner != current_id) return -1;
+  return s->data;
+}
+
+int write(struct S* s, int val) {
+  if (s->owner != current_id) return -1;
+  s->data = val;
+  return 0;
+}
+
+/*@ meta \prop,
+  \name(only_owner_reads),
+  \targets(\ALL),
+  \context(\reading),
+  \tguard(
+    \assert_type((struct S*)\lhost_read) &&
+    (!\separated(&(\lhost_read->data),\read) ==>
+     \lhost_read->owner == current_id));
+*/
+
+/*@ meta \prop,
+  \name(only_owner_writes),
+  \targets(\ALL),
+  \context(\writing),
+  \tguard(
+    \assert_type((struct S*)\lhost_written) &&
+    (!\separated(&(\lhost_written->data),\written) ==>
+     \lhost_written->owner == current_id));
+*/

tests/meta/oracle/lhost.res.oracle

+[kernel] Parsing lhost.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+struct S {
+   unsigned int owner ;
+   int data ;
+};
+extern unsigned int current_id;
+
+int read(struct S *s)
+{
+  int __retres;
+  /*@ assert
+      only_owner_reads: meta:
+        ¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
+  */
+  if (s->owner != current_id) {
+    __retres = -1;
+    goto return_label;
+  }
+  /*@ assert only_owner_reads: meta: s->owner ≡ current_id; */
+  __retres = s->data;
+  return_label: return __retres;
+}
+
+int write(struct S *s, int val)
+{
+  int __retres;
+  /*@ assert
+      only_owner_reads: meta:
+        ¬\separated(&s->data, &s->owner) ⇒ s->owner ≡ current_id;
+  */
+  if (s->owner != current_id) {
+    __retres = -1;
+    goto return_label;
+  }
+  /*@ assert only_owner_writes: meta: s->owner ≡ current_id; */
+  s->data = val;
+  __retres = 0;
+  return_label: return __retres;
+}
+
+/*@ meta "only_owner_reads"; */
+/*@ meta "only_owner_writes";
+*/
+

tests/wp-cache/cache/0588e618c975117e3785fa4d66fed46f.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }

tests/wp-cache/cache/13d660fa98b598e2134cd946b0ba2a8a.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0042,
+  "steps": 20 }

tests/wp-cache/cache/2d96805770b0ec5c2f9255ad9a5d7276.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0127,
+  "steps": 157 }

tests/wp-cache/cache/490d75cd8dab49c2df21e84795e3b74e.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0092,
+  "steps": 158 }

tests/wp-cache/cache/512ef9917d88325cb9e069a736fc68f1.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }

tests/wp-cache/cache/561ca350c5a578955503471a70e73595.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }

tests/wp-cache/cache/7f825a3f0d00a2b9dd277996970ab2b8.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }

tests/wp-cache/cache/85080d53aa62a2fdd83edcfe01fea489.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.0129,
+  "steps": 47 }

tests/wp-cache/cache/8774631f76e90ef51813133252fbb84c.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.005,
+  "steps": 29 }

tests/wp-cache/cache/920df4df73bbe741b5b8449893a70e1e.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "valid", "time": 0.008,
+  "steps": 20 }

tests/wp-cache/cache/f20dcefc53944c4ad0a5f8cf9d78a9b5.json

+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }