Project

General

Profile

« Previous | Next » 

Revision 4240dfcb

Added by LĂ©lio Brun 10 months ago

add basic support to protect against some ACSL keywords

View differences:

src/backends/C/c_backend.ml
121 121
      Header.pp_header_from_header header_fmt basename lusic.contents)
122 122

  
123 123
let translate_to_c generate_c_header basename prog machines dependencies =
124
  let header_m, source_m, source_main_m, makefile_m =
124
  let header_m, source_m, source_main_m, makefile_m, machines =
125 125
    let open Options in
126 126
    match !spec with
127 127
    | SpecNo ->
128 128
      ( C_backend_header.((module EmptyMod : MODIFIERS_HDR)),
129 129
        C_backend_src.((module EmptyMod : MODIFIERS_SRC)),
130 130
        C_backend_main.((module EmptyMod : MODIFIERS_MAINSRC)),
131
        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)) )
131
        C_backend_makefile.((module EmptyMod : MODIFIERS_MKF)),
132
        machines )
132 133
    | SpecACSL ->
133 134
      let open C_backend_spec in
134 135
      ( C_backend_header.((module HdrMod : MODIFIERS_HDR)),
135 136
        C_backend_src.((module SrcMod : MODIFIERS_SRC)),
136 137
        C_backend_main.((module MainMod : MODIFIERS_MAINSRC)),
137
        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)) )
138
        C_backend_makefile.((module MakefileMod : MODIFIERS_MKF)),
139
        sanitize_machines machines)
138 140
    | SpecC ->
139 141
      assert false
140 142
    (* not implemented yet *)
src/backends/C/c_backend_spec.ml
1849 1849
    fprintf fmt "@."
1850 1850
end
1851 1851

  
1852
(* TODO: complete this list *)
1853
let acsl_keywords = ISet.of_list ["set"]
1854

  
1855
let sanitize x = if ISet.mem x acsl_keywords then "__" ^ x else x
1856

  
1857
let sanitize_var_decl vd = { vd with var_id = sanitize vd.var_id }
1858

  
1859
let sanitize_var_decls = List.map sanitize_var_decl
1860

  
1861
let rec sanitize_value v =
1862
  let value_desc = match v.value_desc with
1863
    | Machine_code_types.Var vd -> Machine_code_types.Var (sanitize_var_decl vd)
1864
    | Fun (f, vs) -> Fun (f, sanitize_values vs)
1865
    | Array vs -> Array (sanitize_values vs)
1866
    | Access (v1, v2) -> Access (sanitize_value v1, sanitize_value v2)
1867
    | Power (v1, v2) -> Power (sanitize_value v1, sanitize_value v2)
1868
    | v -> v
1869
  in
1870
  { v with value_desc }
1871

  
1872
and sanitize_values vs = List.map sanitize_value vs
1873

  
1874
let sanitize_expr = function
1875
  | Val v -> Val (sanitize_value v)
1876
  | Var v -> Var (sanitize_var_decl v)
1877
  | e -> e
1878

  
1879
let sanitize_predicate = function
1880
  | Transition (st, f, inst, i, vs, r, mf, mfinsts) ->
1881
    Transition (st, f, inst, i, List.map sanitize_expr vs, r, mf, mfinsts)
1882
  | p -> p
1883

  
1884
let rec sanitize_formula = function
1885
  | Equal (e1, e2) -> Equal (sanitize_expr e1, sanitize_expr e2)
1886
  | GEqual (e1, e2) -> GEqual (sanitize_expr e1, sanitize_expr e2)
1887
  | And fs -> And (sanitize_formulae fs)
1888
  | Or fs -> Or (sanitize_formulae fs)
1889
  | Imply (f1, f2) -> Imply (sanitize_formula f1, sanitize_formula f2)
1890
  | Exists (vs, f) -> Exists (sanitize_var_decls vs, sanitize_formula f)
1891
  | Forall (vs, f) -> Forall (sanitize_var_decls vs, sanitize_formula f)
1892
  | Ternary (e, t, f) -> Ternary (sanitize_expr e, sanitize_formula t, sanitize_formula f)
1893
  | Predicate p -> Predicate (sanitize_predicate p)
1894
  | ExistsMem (m, f1, f2) -> ExistsMem (m, sanitize_formula f1, sanitize_formula f2)
1895
  | Value v -> Value (sanitize_value v)
1896
  | f -> f
1897

  
1898
and sanitize_formulae fs = List.map sanitize_formula fs
1899

  
1900
let rec sanitize_instr i =
1901
  let sanitize_instr_desc = function
1902
    | MLocalAssign (x, v) ->
1903
      MLocalAssign (sanitize_var_decl x, sanitize_value v)
1904
    | MStateAssign (x, v) ->
1905
      MStateAssign (x, sanitize_value v)
1906
    | MStep (xs, f, vs) ->
1907
      MStep (sanitize_var_decls xs, f, sanitize_values vs)
1908
    | MBranch (v, brs) ->
1909
      MBranch (sanitize_value v, List.map (fun (t, instrs) -> t, sanitize_instrs instrs) brs)
1910
    | i -> i
1911
  in
1912
  { i with
1913
    instr_desc = sanitize_instr_desc i.instr_desc;
1914
    instr_spec = sanitize_formulae i.instr_spec
1915
  }
1916

  
1917
and sanitize_instrs instrs = List.map sanitize_instr instrs
1918

  
1919
let sanitize_step s =
1920
  { s with
1921
    step_inputs = sanitize_var_decls s.step_inputs;
1922
    step_outputs = sanitize_var_decls s.step_outputs;
1923
    step_locals = sanitize_var_decls s.step_locals;
1924
    step_instrs = sanitize_instrs s.step_instrs
1925
  }
1926

  
1927
let sanitize_transition t =
1928
  { t with
1929
    tvars = sanitize_var_decls t.tvars;
1930
    tformula = sanitize_formula t.tformula
1931
  }
1932

  
1933
let sanitize_transitions = List.map sanitize_transition
1934

  
1935
let sanitize_memory_pack mp =
1936
  { mp with
1937
    mpformula = sanitize_formula mp.mpformula
1938
  }
1939

  
1940
let sanitize_memory_packs = List.map sanitize_memory_pack
1941

  
1942
let sanitize_spec s =
1943
  { s with
1944
    mtransitions = sanitize_transitions s.mtransitions;
1945
    mmemory_packs = sanitize_memory_packs s.mmemory_packs
1946
  }
1947
let sanitize_machine m =
1948
  { m with
1949
    mstep = sanitize_step m.mstep;
1950
    mspec = sanitize_spec m.mspec
1951
  }
1952

  
1953
let sanitize_machines = List.map sanitize_machine
1954

  
1852 1955
(* Local Variables: *)
1853 1956
(* compile-command:"make -C ../../.." *)
1854 1957
(* End: *)
src/backends/C/c_backend_spec.mli
5 5
module MakefileMod : C_backend_makefile.MODIFIERS_MKF
6 6

  
7 7
module MainMod : C_backend_main.MODIFIERS_MAINSRC
8

  
9
val sanitize_machines: Machine_code_types.machine_t list -> Machine_code_types.machine_t list

Also available in: Unified diff