Merge branch 'feature/called_arg' into 'master'

Add \called_arg

See merge request frama-c/meta!36

README.md

@@ -226,6 +226,27 @@ particular function, and throw a typing error otherwise. Hence, the expression
 using `\formal` should be surrounded by a
 [guard](#guarding-against-type-errors).
 
+### Referring to call parameters
+
+When using the `\calling` context and targetting a specific called function, it
+is possible to refer to the value provided for a formal at every call site,
+using `\called_arg(parameter_name)`. It throws a type error when the called
+function does not have the specified formal, is indirectly called (through a
+function pointer) or is a variadic function. Thus it should be surrounded by a
+[guard](#guarding-against-type-errors). 
+
+For example, the following meta-property states that parameter `x` of
+`float sqrt(float x)`
+should never be provided with a negative value.
+
+```
+meta \prop,
+    \name(sqrt_pos),
+    \targets(\ALL),
+    \context(\calling),
+    \tguard(\called == sqrt ==> \fguard(\called_arg(x) >= 0.));
+```
+
 ### Referring to bound names (experimental)
 
 If it is not possible to rely on a consistent naming of formals across

meta_annotate.ml

@@ -240,17 +240,36 @@ let addr_of_tlval tlval =
 class calling_visitor flags all_mp table = object (self)
   inherit context_visitor flags all_mp table
 
-  method calling_instance stmt called =
+  method calling_instance stmt called called_kf args =
     let addr_term = addr_of_tlval called in
-    let assoc_list = [("\\called", addr_term)] in
+    let main_assoc = ("\\called", RepVariable addr_term) in
+    let assoc_list = match called_kf with
+      | None ->
+        Self.warning ~once:true
+          "\\called_arg cannot be used with indirect calls" ;
+        [main_assoc]
+      | Some kf ->
+        let formals = Kernel_function.get_formals kf in
+        try
+          let param_assocs = List.map2 (fun formal given ->
+              let given_term = Logic_utils.expr_to_term given in
+              (formal.vorig_name, given_term)
+            ) formals args
+          in [main_assoc; ("\\called_arg", RepApp param_assocs)]
+        with Invalid_argument _ ->
+          Self.warning ~once:true "\\called_arg cannot be used with variadic \
+                                   functions. Please use the Instantiate plugin" ;
+          [main_assoc]
+    in
     List.iter (self # instantiate stmt assoc_list) mp_todo
 
   method! vinst = function
-    | Call (_, fexpr, _, _) -> 
+    | Call (_, fexpr, args, _) -> 
       let lv = match fexpr.enode with Lval lv -> lv | _ -> assert false in
       let stmt = Option.get self # current_stmt in
+      let called_kf = Kernel_function.get_called fexpr in
       let tlval = Logic_utils.lval_to_term_lval lv in
-      self#calling_instance stmt tlval ;
+      self#calling_instance stmt tlval called_kf args ;
       Cil.DoChildren
     | _ -> Cil.SkipChildren
 end
@@ -317,7 +336,7 @@ 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", addr_term)] in
+      let assoc_list = [("\\written", RepVariable addr_term)] in
       List.iter (self # instantiate ~post stmt assoc_list) mp_todo
 
   (* Inspect function specs to see what it assigns and instantiate the
@@ -384,7 +403,7 @@ class reading_visitor flags all_mp table = object (self)
   (* 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", addr_term)] in
+    let assoc_list = [("\\read", RepVariable 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_deduce.ml

@@ -118,7 +118,7 @@ let dummy_term loc = {
 
 let dummy_unpack mp =
   let terms = ["\\written"; "\\read"; "\\called"] in
-  let assoc = List.map (fun t -> (t, dummy_term mp.mp_loc)) terms in
+  let assoc = List.map (fun t -> (t, RepVariable (dummy_term mp.mp_loc))) terms in
   mp.mp_property (Kernel_function.dummy ()) assoc
 
 let predicate_counter = ref 1

meta_dispatch.ml

@@ -26,7 +26,7 @@ open Meta_options
 
 type unpacked_metaproperty = {
   ump_emitter : Emitter.t;
-  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
   ump_ip : Property.t;
   ump_counter : int ref;
   ump_admit : bool;

meta_dispatch.mli

@@ -26,7 +26,7 @@ open Meta_options
 
 type unpacked_metaproperty = {
   ump_emitter : Emitter.t;
-  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
   ump_ip : Property.t;
   ump_counter : int ref;
   ump_admit : bool;

meta_parse.ml

@@ -59,11 +59,16 @@ type mp_translation =
   | MtDefault (* translation activated, with unspecified mode *)
   | MtNone
 
+(* Kinds of keywords that can be replaced in a MP instantiation *)
+type replaced_kind =
+  | RepVariable of term (* replace variable by term *)
+  | RepApp of (string * term) list (* replace application with arg by associated term *)
+
 type metaproperty = {
   mp_name : string;
   mp_target : target;
   mp_context : context;
-  mp_property : Kernel_function.t -> (string * term) list -> predicate;
+  mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
   mp_proof_method : mp_proof_method;
   mp_translation : mp_translation;
   mp_loc : Cil_types.location
@@ -83,7 +88,8 @@ let mp_contexts = [
 let mp_metavariables = [
   "\\written";
   "\\read";
-  "\\called"
+  "\\called";
+  "\\called_arg"
 ]
 let mp_utils = [
   "\\diff";
@@ -141,10 +147,28 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
       end
     | PLapp ("\\bound", _, [bound]) ->
       Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
+    | PLapp (app_name, _, [{lexpr_node = PLvar arg}])
+      when List.mem app_name mp_terms ->
+      begin match List.assoc_opt app_name termassoc with
+        | Some RepApp l ->
+          begin match List.assoc_opt arg l with
+            | Some term -> term
+            | None -> meta_ctxt.error loc
+                        "%s is not a valid argument for %s here" arg app_name
+          end
+        | None -> meta_ctxt.error loc
+                    "Application of %s forbidden in this context" app_name
+        | _ -> meta_ctxt.error loc
+                 "%s expects no arguments but has been provided with one"
+                 app_name
+      end
     | PLvar vname when List.mem vname mp_terms ->
-      begin try List.assoc vname termassoc
-      with _ -> meta_ctxt.error loc
+      begin match List.assoc_opt vname termassoc with
+        | Some RepVariable a -> a
+        | None -> meta_ctxt.error loc
                   "Variable %s forbidden in this context" vname
+        | _ -> meta_ctxt.error loc
+                 "%s expects one argument but has been provided with none" vname
       end
     | _ -> orig_ctxt.type_term meta_ctxt env expr
 
@@ -197,8 +221,15 @@ let rec process_targets tc expr = match expr.lexpr_node with
   | _ -> TgSet (StrSet.singleton @@ process_single_target tc expr)
 
 let pp_aslist fmt l =
+  let pp_replaced_kind fmt = function
+    | RepVariable v -> Printer.pp_term fmt v
+    | RepApp l ->
+      let pp_singular fmt (a, b) =
+        Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+      in Format.pp_print_list pp_singular fmt l
+  in
   let pp_assoc fmt (a, b) =
-    Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+    Format.fprintf fmt "(%s, %a)" a pp_replaced_kind b
   in Format.pp_print_list pp_assoc fmt l
 
 let delay_prop tc name lexpr kf aslist =

meta_parse.mli

@@ -53,11 +53,15 @@ type mp_translation =
   | MtDefault
   | MtNone
 
+type replaced_kind =
+  | RepVariable of term (** replace variable by term *)
+  | RepApp of (string * term) list (** replace application with arg by associated term *)
+
 type metaproperty = {
   mp_name : string;
   mp_target : target;
   mp_context : context;
-  mp_property : Kernel_function.t -> (string * term) list -> predicate;
+  mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
   mp_proof_method : mp_proof_method;
   mp_translation : mp_translation;
   mp_loc : Cil_types.location
@@ -65,5 +69,5 @@ type metaproperty = {
 
 val register_parsing : unit -> unit
 
-(* The list of meta-properties in the file, in the same order *)
+(** The list of meta-properties in the file, in the same order *)
 val metaproperties : unit -> metaproperty list

tests/meta-wp/oracle/uncalled.res.oracle

 [kernel] Parsing tests/meta-wp/uncalled.c (with preprocessing)
 [meta] Translation is enabled
 [meta] Will process 2 properties
+[meta] Warning: \called_arg cannot be used with indirect calls
 [meta] Successful translation
 [wp] Running WP plugin...
 [wp] tests/meta-wp/uncalled.c:21: Warning: Missing 'calls' for default behavior

tests/meta/called_arg.c

+/* run.config
+   OPT: @META@ @PRINT@
+*/
+
+void g1(int x, float y);
+void g2(int y);
+void g3(int x);
+
+void f(int x) {
+    g1(0, 42);
+    g2(1 + 1);
+    g3(x + 2);
+}
+
+/*@ meta \prop,
+        \name(p42_not_used_as_y),
+        \targets(\ALL),
+        \context(\calling),
+        \tguard(\called_arg(y) != 42);
+*/
+
+/*@ meta \prop,
+        \name(p42_not_used_as_y_for_g2),
+        \targets(\ALL),
+        \context(\calling),
+        \tguard(\called == g2 ==> \fguard(\called_arg(y) != 42));
+*/

tests/meta/oracle/called_arg.res.oracle

+[kernel] Parsing tests/meta/called_arg.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+void g1(int x, float y);
+
+void g2(int y);
+
+void g3(int x);
+
+void f(int x)
+{
+  /*@ assert p42_not_used_as_y: meta: (float)42 ≢ 42; */
+  g1(0,(float)42);
+  /*@ assert p42_not_used_as_y: meta: (int)(1 + 1) ≢ 42; */
+  /*@ assert p42_not_used_as_y_for_g2: meta: (int)(1 + 1) ≢ 42; */
+  g2(1 + 1);
+  /*@ assert p42_not_used_as_y_for_g2: meta: ¬(&g3 ≡ &g2); */
+  g3(x + 2);
+  return;
+}
+
+/*@ meta "p42_not_used_as_y"; */
+/*@ meta "p42_not_used_as_y_for_g2";
+*/
+