Inject ghost global variables from YAML witness into Cil file during init (#1998)

* Reject witness on duplicate ghost variable declarations

* Fix ghost global initinfo construction

* Fix Formatcil.cType partial application compilation error

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/28884c57-57a6-4417-9509-264ab8dba17f

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Add cram test for ghost variable injection from YAML witness

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/9da67fc2-69ae-48ea-904b-4e7ae68c4735

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Move YamlWitness.init() before justcil check and update cram test to verify CIL output

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/86acd990-3af7-4033-b7b4-95622c8d6391

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Fix cram test: match actual CIL printer output with extra spaces around initializer

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/6246b7e7-f321-48b7-83ce-3fb435a854f5

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Author: michael-schwarz

src/framework/control.ml

@@ -370,7 +370,6 @@ struct
     (* real beginning of the [analyze] function *)
     if get_bool "ana.sv-comp.enabled" then
       Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *)
-    YamlWitness.init ();
 
     AnalysisState.global_initialization := true;
     GobConfig.earlyglobs := get_bool "exp.earlyglobs";

src/maingoblint.ml

@@ -541,6 +541,7 @@ let do_analyze change_info merged_AST =
     Messages.out := Legacy.open_out (get_string "outfile"));
 
   let module L = Printable.Liszt (CilType.Fundec) in
+  YamlWitness.init ();
   if get_bool "justcil" then
     (* if we only want to print the output created by CIL: *)
     Cilfacade.print merged_AST

src/witness/yamlWitness.ml

@@ -415,7 +415,71 @@ let init () =
     if not (Sys.file_exists path) then (
       Logs.error "witness.yaml.validate: %s not found" path;
       Svcomp.errorwith "witness missing"
-    )
+    );
+    let file = !Cilfacade.current_file in
+    let global_vars =
+      file.globals
+      |> List.filter_map (function
+          | Cil.GVar (v, _, _)
+          | Cil.GVarDecl (v, _)
+          | Cil.GFun ({svar = v; _}, _) -> Some (v.vname, Cil.Fv v)
+          | _ -> None
+        )
+    in
+    let has_global name =
+      List.exists (function
+          | Cil.GVar (v, _, _)
+          | Cil.GVarDecl (v, _)
+          | Cil.GFun ({svar = v; _}, _) -> String.equal v.vname name
+          | _ -> false
+        ) file.globals
+    in
+    let parse_type (type_: string): Cil.typ option =
+      try Some (Formatcil.cType type_ []) with
+      | exn when GobExn.catch_all_filter exn ->
+        M.warn_noloc ~category:Witness "ghost variable type parse failed: %s" type_;
+        None
+    in
+    let parse_init (init: string): Cil.exp option =
+      try Some (Formatcil.cExp init global_vars) with
+      | exn when GobExn.catch_all_filter exn ->
+        M.warn_noloc ~category:Witness "ghost variable initializer parse failed: %s" init;
+        None
+    in
+    let instrument_ghost_variable (variable: YamlWitnessType.GhostInstrumentation.Variable.t): unit =
+      if not (String.equal variable.scope "global") then (
+        M.warn_noloc ~category:Witness "unsupported ghost variable scope: %s" variable.scope
+      )
+      else if has_global variable.name then (
+        M.error_noloc ~category:Witness "ghost variable already declared in program: %s" variable.name;
+        Svcomp.errorwith "witness error"
+      )
+      else
+        match parse_type variable.type_, parse_init variable.initial.value with
+        | Some typ, Some init ->
+          let v = makeGlobalVar variable.name typ in
+          let g = GVar (v, {init = Some (SingleInit init)}, locUnknown) in
+          file.globals <- g :: file.globals
+        | _ ->
+          M.error_noloc ~category:Witness "failed to instrument ghost variable declaration: %s" variable.name
+    in
+    let instrument_ghost_variables yaml_entry =
+      match YamlWitnessType.Entry.of_yaml yaml_entry with
+      | Ok {entry_type = YamlWitnessType.EntryType.GhostInstrumentation {ghost_variables; _}; _} ->
+        List.iter instrument_ghost_variable ghost_variables
+      | Ok _ ->
+        ()
+      | Error (`Msg m) ->
+        M.error_noloc ~category:Witness "couldn't parse entry while extracting ghost instrumentation: %s" m
+    in
+    let yaml = match GobResult.Syntax.(Fpath.of_string path >>= Yaml_unix.of_file) with
+      | Ok yaml -> yaml
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
+    in
+    let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
+    List.iter instrument_ghost_variables yaml_entries
 
 let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
   file = location.file_name;

tests/regression/witness/ghost.t/ghost.c

@@ -0,0 +1,3 @@
+int main() {
+  return 0;
+}

tests/regression/witness/ghost.t/ghost.yml

@@ -0,0 +1,24 @@
+- entry_type: ghost_instrumentation
+  metadata:
+    format_version: "2.1-goblint"
+    uuid: 00000000-0000-0000-0000-000000000001
+    creation_time: 2024-01-01T00:00:00Z
+    producer:
+      name: Test
+      version: "0.0"
+    task:
+      input_files:
+      - ghost.c
+      input_file_hashes:
+        ghost.c: "0000000000000000000000000000000000000000000000000000000000000000"
+      data_model: LP64
+      language: C
+  content:
+    ghost_variables:
+    - name: m_locked
+      scope: global
+      type: int
+      initial:
+        value: "0"
+        format: c_expression
+    ghost_updates: []

tests/regression/witness/ghost.t/run.t

@@ -0,0 +1,4 @@
+Ghost variables declared in a YAML witness are injected into the CIL file before analysis:
+
+  $ goblint --enable justcil --set dbg.justcil-printer clean --set witness.yaml.validate ghost.yml ghost.c | grep -E "m_locked"
+  int m_locked  =    0;