<commit_before>(** Analysis by specification file. *)

open Prelude.Ana
open Analyses

module SC = SpecCore

module Spec =
struct
  include Analyses.DefaultSpec

  let name()  = "spec"
  module D = SpecDomain.Dom
  module C = SpecDomain.Dom
  module G = Lattice.Unit

  (* special variables *)
  let return_var    = Goblintutil.create_var @@ Cil.makeVarinfo false "@return"    Cil.voidType, `NoOffset
  let global_var    = Goblintutil.create_var @@ Cil.makeVarinfo false "@global"    Cil.voidType, `NoOffset

  (* spec data *)
  let nodes = ref []
  let edges = ref []

  let load_specfile () =
    let specfile = GobConfig.get_string "ana.spec.file" in
    if String.length specfile < 1 then failwith "You need to specify a specification file using --set ana.spec.file path/to/file.spec when using the spec analysis!";
    if not (Sys.file_exists specfile) then failwith @@ "The given spec-file ("^specfile^") doesn't exist (CWD is "^Sys.getcwd ()^").";
    let _nodes, _edges = SpecUtil.parseFile specfile in
    nodes := _nodes; edges := _edges (* don't change -> no need to save them in domain *)

  (* module for encapsulating general spec checking functions used in multiple transfer functions (assign, special) *)
  (*
  .spec-format:
  - The file contains two types of definitions: nodes and edges. The labels of nodes are output. The labels of edges are the constraints.
  - The given nodes are warnings, which have an implicit back edge to the previous node if used as a target.
  - Alternatively warnings can be specified like this: "node1 -w1,w2,w3> node2 ...1" (w1, w2 and w3 will be output when the transition is taken).
  - The start node of the first transition is the start node of the automaton.
  - End nodes are specified by "node -> end _".
  - "_end" is the local warning for nodes that are not in an end state, _END is the warning at return ($ is the list of keys).
  - An edge with '_' matches everything.
  - Edges with "->>" (or "-w1,w2>>" etc.) are forwarding edges, which will continue matching the same statement for the target node.
  *)
  module SpecCheck =
  struct
    (* custom goto (D.goto is just for modifying) that checks if the target state is a warning and acts accordingly *)
    let goto ?may:(may=false) ?change_state:(change_state=true) key state m ws =
      let loc = !Tracing.current_loc::(D.callstack m) in
      let warn key m msg =
        Str.global_replace (Str.regexp_string "$") (D.string_of_key key) msg
        |> D.warn ~may:(D.is_may key m || D.is_unknown key m)
      in
      (* do transition warnings *)
      List.iter (fun state -> match SC.warning state !nodes with Some msg -> warn key m msg | _ -> ()) ws;
      match SC.warning state !nodes with
      | Some msg ->
        warn key m msg;
        m (* no goto == implicit back edge *)
      | None ->
        M.debug "GOTO %s: %s -> %s" (D.string_of_key key) (D.string_of_state key m) state;
        if not change_state then m
        else if may then D.may_goto key loc state m else D.goto key loc state m

    (* match spec_exp, cil_exp *)
    let equal_exp ctx spec_exp cil_exp = match spec_exp, cil_exp with
      (* TODO match constants right away to avoid queries? *)
      | `String a, Const(CStr b) -> M.debug "EQUAL String Const: %s = %s" a b; a=b
      (* | `String a, Const(CWStr xs as c) -> failwith "not implemented" *)
      (* CWStr is done in base.ml, query only returns `Str if it's safe *)
      | `String a, e -> (match ctx.ask (Queries.EvalStr e) with
          | `Lifted b -> M.debug "EQUAL String Query: %s = %s" a b; a=b
          | _      -> M.debug "EQUAL String Query: no result!"; false
        )
      | `Regex a, e -> (match ctx.ask (Queries.EvalStr e) with
          | `Lifted b -> M.debug "EQUAL Regex String Query: %s = %s" a b; Str.string_match (Str.regexp a) b 0
          | _      -> M.debug "EQUAL Regex String Query: no result!"; false
        )
      | `Bool a, e -> (match ctx.ask (Queries.EvalInt e) with
          | b -> (match Queries.ID.to_bool b with Some b -> a=b | None -> false)
        )
      | `Int a, e  -> (match ctx.ask (Queries.EvalInt e) with
          | b -> (match Queries.ID.to_int b with Some b -> (Int64.of_int a)=(IntOps.BigIntOps.to_int64 b) | None -> false)
        )
      | `Float a, Const(CReal (b, fkind, str_opt)) -> a=b
      | `Float a, _ -> M.warn "EQUAL Float: unsupported!"; false
      (* arg is a key. currently there can only be one key per constraint, so we already used it for lookup. TODO multiple keys? *)
      | `Var a, b  -> true
      (* arg is a identifier we use for matching constraints. TODO save in domain *)
      | `Ident a, b -> true
      | `Error s, b -> failwith @@ "Spec error: "^s
      (* wildcard matches anything *)
      | `Free, b    -> true
      | a,b -> M.warn "EQUAL? Unmatched case - assume true..."; true

    let check_constraint ctx get_key matches m new_a old_key (a,ws,fwd,b,c as edge) =<commit_msg>Remove unnecessary signature comment in Spec<commit_after>(** Analysis by specification file. *)

open Prelude.Ana
open Analyses

module SC = SpecCore

module Spec =
struct
  include Analyses.DefaultSpec

  let name()  = "spec"
  module D = SpecDomain.Dom
  module C = SpecDomain.Dom
  module G = Lattice.Unit

  (* special variables *)
  let return_var    = Goblintutil.create_var @@ Cil.makeVarinfo false "@return"    Cil.voidType, `NoOffset
  let global_var    = Goblintutil.create_var @@ Cil.makeVarinfo false "@global"    Cil.voidType, `NoOffset

  (* spec data *)
  let nodes = ref []
  let edges = ref []

  let load_specfile () =
    let specfile = GobConfig.get_string "ana.spec.file" in
    if String.length specfile < 1 then failwith "You need to specify a specification file using --set ana.spec.file path/to/file.spec when using the spec analysis!";
    if not (Sys.file_exists specfile) then failwith @@ "The given spec-file ("^specfile^") doesn't exist (CWD is "^Sys.getcwd ()^").";
    let _nodes, _edges = SpecUtil.parseFile specfile in
    nodes := _nodes; edges := _edges (* don't change -> no need to save them in domain *)

  (* module for encapsulating general spec checking functions used in multiple transfer functions (assign, special) *)
  (*
  .spec-format:
  - The file contains two types of definitions: nodes and edges. The labels of nodes are output. The labels of edges are the constraints.
  - The given nodes are warnings, which have an implicit back edge to the previous node if used as a target.
  - Alternatively warnings can be specified like this: "node1 -w1,w2,w3> node2 ...1" (w1, w2 and w3 will be output when the transition is taken).
  - The start node of the first transition is the start node of the automaton.
  - End nodes are specified by "node -> end _".
  - "_end" is the local warning for nodes that are not in an end state, _END is the warning at return ($ is the list of keys).
  - An edge with '_' matches everything.
  - Edges with "->>" (or "-w1,w2>>" etc.) are forwarding edges, which will continue matching the same statement for the target node.
  *)
  module SpecCheck =
  struct
    (* custom goto (D.goto is just for modifying) that checks if the target state is a warning and acts accordingly *)
    let goto ?may:(may=false) ?change_state:(change_state=true) key state m ws =
      let loc = !Tracing.current_loc::(D.callstack m) in
      let warn key m msg =
        Str.global_replace (Str.regexp_string "$") (D.string_of_key key) msg
        |> D.warn ~may:(D.is_may key m || D.is_unknown key m)
      in
      (* do transition warnings *)
      List.iter (fun state -> match SC.warning state !nodes with Some msg -> warn key m msg | _ -> ()) ws;
      match SC.warning state !nodes with
      | Some msg ->
        warn key m msg;
        m (* no goto == implicit back edge *)
      | None ->
        M.debug "GOTO %s: %s -> %s" (D.string_of_key key) (D.string_of_state key m) state;
        if not change_state then m
        else if may then D.may_goto key loc state m else D.goto key loc state m

    let equal_exp ctx spec_exp cil_exp = match spec_exp, cil_exp with
      (* TODO match constants right away to avoid queries? *)
      | `String a, Const(CStr b) -> M.debug "EQUAL String Const: %s = %s" a b; a=b
      (* | `String a, Const(CWStr xs as c) -> failwith "not implemented" *)
      (* CWStr is done in base.ml, query only returns `Str if it's safe *)
      | `String a, e -> (match ctx.ask (Queries.EvalStr e) with
          | `Lifted b -> M.debug "EQUAL String Query: %s = %s" a b; a=b
          | _      -> M.debug "EQUAL String Query: no result!"; false
        )
      | `Regex a, e -> (match ctx.ask (Queries.EvalStr e) with
          | `Lifted b -> M.debug "EQUAL Regex String Query: %s = %s" a b; Str.string_match (Str.regexp a) b 0
          | _      -> M.debug "EQUAL Regex String Query: no result!"; false
        )
      | `Bool a, e -> (match ctx.ask (Queries.EvalInt e) with
          | b -> (match Queries.ID.to_bool b with Some b -> a=b | None -> false)
        )
      | `Int a, e  -> (match ctx.ask (Queries.EvalInt e) with
          | b -> (match Queries.ID.to_int b with Some b -> (Int64.of_int a)=(IntOps.BigIntOps.to_int64 b) | None -> false)
        )
      | `Float a, Const(CReal (b, fkind, str_opt)) -> a=b
      | `Float a, _ -> M.warn "EQUAL Float: unsupported!"; false
      (* arg is a key. currently there can only be one key per constraint, so we already used it for lookup. TODO multiple keys? *)
      | `Var a, b  -> true
      (* arg is a identifier we use for matching constraints. TODO save in domain *)
      | `Ident a, b -> true
      | `Error s, b -> failwith @@ "Spec error: "^s
      (* wildcard matches anything *)
      | `Free, b    -> true
      | a,b -> M.warn "EQUAL? Unmatched case - assume true..."; true

    let check_constraint ctx get_key matches m new_a old_key (a,ws,fwd,b,c as edge) =
{'fraction_non_alphanumeric': 0.11253170979198376, 'fraction_numerical': 0.003450025367833587, 'mean_word_length': 2.6762402088772848, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 77, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4852413', 'n_tokens_mistral': 3121, 'n_tokens_neox': 3034, 'n_words': 1260}