Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/backends/C/c_backend_spec.ml
195 195
    pp_var_decl
196 196

  
197 197
let pp_forall pp_l pp_r fmt (l, r) =
198
  fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
198
  fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
199 199

  
200 200
let pp_exists pp_l pp_r fmt (l, r) =
201 201
  fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r
......
240 240
let pp_initialization pp_mem fmt (name, mem) =
241 241
  fprintf fmt "%s_initialization(%a)" name pp_mem mem
242 242

  
243
let pp_init pp_mem fmt (name, mem) =
244
  fprintf fmt "%s_init(%a)" name pp_mem mem
245

  
243 246
let pp_initialization' = pp_initialization pp_print_string
244 247

  
245 248
let pp_local m =
......
628 631
let pp_lemma pp_l pp_r fmt (l, r) =
629 632
  fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r
630 633

  
634
let pp_axiomatic pp_l pp_r fmt (l, r) =
635
  fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r
636

  
637
let pp_axiom pp_l pp_r fmt (l, r) =
638
  fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r
639

  
631 640
let pp_mem_valid_def fmt m =
632 641
  if not (fst (get_stateless_status m)) then
633 642
    let name = m.mname.node_id in
......
991 1000
      fmt
992 1001
      ()
993 1002

  
994
  let pp_node_spec m fmt = function
995
    | Contract c
996
    | NodeSpec (_, Some c) ->
997
      PrintSpec.pp_spec PrintSpec.TransitionMode m fmt
998
        (Spec_common.red (Imply (c.mc_pre, c.mc_post)))
999
    | NodeSpec (f, None) ->
1000
      pp_print_string fmt f
1003
  let spec_from_contract c =
1004
    Spec_common.red (Imply (c.mc_pre, c.mc_post))
1005

  
1006
  let pp_contract m fmt c =
1007
    PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c)
1008

  
1009
  let contract_of machines m =
1010
    match m.mspec.mnode_spec with
1011
    | Some spec ->
1012
      begin match spec with
1013
        | Contract c ->
1014
          Some c, None
1015
        | NodeSpec f ->
1016
          let m_f = find_machine f machines in
1017
          begin match m_f.mspec.mnode_spec with
1018
            | Some (Contract c) ->
1019
              Some c, Some m_f
1020
            | _ ->
1021
              None, None
1022
          end
1023
      end
1024
    | None ->
1025
      None, None
1026

  
1027
  let pp_init_def fmt m =
1028
    let name = m.mname.node_id in
1029
    let mem = mk_mem m in
1030
    pp_predicate
1031
      (pp_init (pp_machine_decl' ~ghost:true))
1032
      (pp_and pp_initialization' (pp_reset_flag' ~indirect:false))
1033
      fmt
1034
      ((name, (name, mem)), ((name, mem), mem))
1035

  
1036
  let rename n x = sprintf "%s_%d" x n
1037

  
1038
  let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
1039

  
1040
  let rec rename_value n v =
1041
    { v with value_desc =
1042
                match v.value_desc with
1043
                  | Machine_code_types.Var v -> Machine_code_types.Var (rename_var_decl n v)
1044
                  | Fun (f, vs) -> Fun (f, List.map (rename_value n) vs)
1045
                  | Array vs -> Array (List.map (rename_value n) vs)
1046
                  | Access (v1, v2) -> Access (rename_value n v1, rename_value n v2)
1047
                  | Power (v1, v2) -> Power (rename_value n v1, rename_value n v2)
1048
                  | v -> v
1049
    }
1050

  
1051
  let rename_expression: type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t =
1052
    fun n -> function
1053
    | Val v -> Val (rename_value n v)
1054
    | Var v -> Var (rename_var_decl n v)
1055
    | e -> e
1056

  
1057
  let rename_predicate n = function
1058
    | Transition (f, inst, i, es, r, mf, mif) ->
1059
      Transition (f, inst, i, List.map (rename_expression n) es, r, mf, mif)
1060
    | p -> p
1061

  
1062
  let rec rename_formula n = function
1063
    | Equal (e1, e2) -> Equal (rename_expression n e1, rename_expression n e2)
1064
    | And fs -> And (List.map (rename_formula n) fs)
1065
    | Or fs -> Or (List.map (rename_formula n) fs)
1066
    | Imply (f1, f2) -> Imply (rename_formula n f1, rename_formula n f2)
1067
    | Exists (xs, f) -> Exists (List.map (rename_var_decl n) xs, rename_formula n f)
1068
    | Forall (xs, f) -> Forall (List.map (rename_var_decl n) xs, rename_formula n f)
1069
    | Ternary (e, t, f) -> Ternary (rename_expression n e, rename_formula n t, rename_formula n f)
1070
    | Predicate p -> Predicate (rename_predicate n p)
1071
    | ExistsMem (x, f1, f2) -> ExistsMem (rename n x, rename_formula n f1, rename_formula n f2)
1072
    | Value v -> Value (rename_value n v)
1073
    | f -> f
1074

  
1075
    
1076
  let rename_contract n c =
1077
    { c with
1078
      mc_pre = rename_formula n c.mc_pre;
1079
      mc_post = rename_formula n c.mc_post; }
1080

  
1081
  let but_last l =
1082
    List.(rev (tl (rev l)))
1083

  
1084
  let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt (n, mem_in, mem_out) =
1085
    let name = m.mname.node_id in
1086
    let inputs = m.mstep.step_inputs in
1087
    let outputs = m.mstep.step_outputs in
1088
    fprintf fmt "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])"
1089
      name
1090
      case
1091
      n
1092
      pp_mem_in
1093
      mem_in
1094
      pp_vars
1095
      (inputs @ outputs)
1096
      pp_mem_out
1097
      mem_out
1098

  
1099
  let pp_k_induction_base_case m =
1100
    pp_k_induction_case "base" m
1101

  
1102
  let pp_k_induction_inductive_case m =
1103
    pp_k_induction_case "inductive" m
1104

  
1105
  let pp_base_cases m fmt (c, m_c, k) =
1106
    let name = m.mname.node_id in
1107
    let mem = mk_mem m in
1108
    let inputs = m.mstep.step_inputs in
1109
    let outputs = m.mstep.step_outputs in
1110
    let l = List.init (k - 1) (fun n -> n + 1) in
1111
    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
1112
      (fun fmt n ->
1113
         let l = List.init (n + 1) (fun n -> n) in
1114
         let l' = List.init n (fun n -> n) in
1115
         let pp =
1116
           pp_implies
1117
             (pp_and
1118
                (pp_and_l (fun fmt -> function
1119
                     | 0 ->
1120
                       pp_init pp_print_string fmt (name, rename 0 mem)
1121
                     | n ->
1122
                       pp_transition_aux m pp_print_string pp_print_string pp_var_decl
1123
                         fmt
1124
                         (name,
1125
                          List.map (rename_var_decl n) (inputs @ outputs),
1126
                          rename (n - 1) mem,
1127
                          rename n mem)))
1128
                (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1129
             (pp_contract m)
1130
         in
1131
         pp_predicate
1132
           (pp_k_induction_base_case
1133
              m
1134
              (pp_machine_decl' ~ghost:true)
1135
              (pp_machine_decl' ~ghost:true)
1136
              (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs)))
1137
           (pp_forall (pp_locals m)
1138
              (if n > 1 then
1139
                 pp_forall
1140
                   (fun fmt l -> fprintf fmt "%a@,%a"
1141
                       (pp_machine_decl ~ghost:true
1142
                          (pp_comma_list ~pp_eol:pp_print_comma
1143
                             (fun fmt n -> pp_print_string fmt (rename n mem))))
1144
                       (name, but_last l)
1145
                       (pp_locals m)
1146
                       (List.flatten
1147
                          (List.map (fun n ->
1148
                               List.map (rename_var_decl n) (inputs @ outputs))
1149
                              (List.tl l))))
1150
                   pp
1151
               else
1152
                 fun fmt (_, x) -> pp fmt x))
1153
           fmt
1154
           ((n, (name, rename (n - 1) mem), (name, rename n mem)),
1155
            (List.map (rename_var_decl n) m_c.mstep.step_outputs,
1156
             (l', ((l,
1157
                    (m_c.mname.node_id,
1158
                     List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs),
1159
                     "", "")),
1160
                   rename_contract n c)))))
1161
           fmt
1162
           l
1163

  
1164
  let pp_inductive_case m fmt (c, m_c, k) =
1165
    let name = m.mname.node_id in
1166
    let mem = mk_mem m in
1167
    let inputs = m.mstep.step_inputs in
1168
    let outputs = m.mstep.step_outputs in
1169
    let l = List.init k (fun n -> n + 1) in
1170
    let pp =
1171
      pp_implies
1172
        (pp_and_l (fun fmt n ->
1173
             pp_and
1174
               (pp_and
1175
                  (pp_transition_aux m pp_print_string pp_print_string pp_var_decl)
1176
                  (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1177
               (pp_contract m)
1178
               fmt
1179
               (((name,
1180
                  List.map (rename_var_decl n) (inputs @ outputs),
1181
                  rename (n - 1) mem,
1182
                  rename n mem),
1183
                 (m_c.mname.node_id,
1184
                  List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs),
1185
                  "", "")),
1186
                rename_contract n c)))
1187
        (pp_contract m)
1188
    in
1189
    pp_predicate
1190
      (pp_k_induction_inductive_case
1191
         m
1192
         (pp_machine_decl' ~ghost:true)
1193
         (pp_machine_decl' ~ghost:true)
1194
         (fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs)))
1195
      (pp_forall (pp_locals m)
1196
         (if k > 1 then
1197
            pp_forall
1198
              (fun fmt l -> fprintf fmt "%a@,%a"
1199
                  (pp_machine_decl ~ghost:true
1200
                     (pp_comma_list ~pp_eol:pp_print_comma
1201
                        (fun fmt n -> pp_print_string fmt (rename (n - 1) mem))))
1202
                  (name, but_last l)
1203
                  (pp_locals m)
1204
                  (List.flatten
1205
                     (List.map (fun n ->
1206
                          List.map (rename_var_decl (n - 1)) (inputs @ outputs))
1207
                         (List.tl l))))
1208
              pp
1209
          else
1210
            fun fmt (_, x) -> pp fmt x))
1211
      fmt
1212
      ((k, (name, rename (k - 1) mem), (name, rename k mem)),
1213
       (List.(flatten (List.map (fun n -> List.map (rename_var_decl n) m_c.mstep.step_outputs) l)),
1214
        (l, (l, rename_contract k c))))
1215

  
1216
  let pp_k_induction_lemmas m fmt k =
1217
    let name = m.mname.node_id in
1218
    let mem_in = mk_mem_in m in
1219
    let mem_out = mk_mem_out m in
1220
    let inputs = m.mstep.step_inputs in
1221
    let outputs = m.mstep.step_outputs in
1222
    let l = List.init k (fun n -> n + 1) in
1223
    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
1224
      (fun fmt n ->
1225
         pp_lemma
1226
           (fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
1227
           (pp_forall
1228
              (fun fmt () -> fprintf fmt "%a,@;%a"
1229
                  (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1230
                  (name, [mem_in; mem_out])
1231
                  (pp_locals m)
1232
                  (inputs @ outputs))
1233
              ((if n = k then
1234
                  pp_k_induction_inductive_case
1235
                else
1236
                  pp_k_induction_base_case)
1237
                 m
1238
                 pp_print_string
1239
                 pp_print_string
1240
                 (pp_comma_list pp_var_decl)))
1241
           fmt
1242
           (n, ((), (n, mem_in, mem_out))))
1243
      fmt
1244
      l
1245

  
1246
  let pp_k_induction_axiom m fmt (c, m_c, k) =
1247
    let name = m.mname.node_id in
1248
    let mem_in = mk_mem_in m in
1249
    let mem_out = mk_mem_out m in
1250
    let inputs = m.mstep.step_inputs in
1251
    let outputs = m.mstep.step_outputs in
1252
    let l = List.init k (fun n -> n + 1) in
1253
    pp_axiomatic
1254
      (fun fmt () -> fprintf fmt "%s_k_Induction" name)
1255
      (pp_axiom
1256
         (fun fmt () -> fprintf fmt "%s_k_induction" name)
1257
         (pp_forall
1258
           (pp_locals m)
1259
           (pp_forall
1260
              (fun fmt () -> fprintf fmt "%a,@;%a"
1261
                  (pp_machine_decl ~ghost:true (pp_comma_list pp_print_string))
1262
                  (name, [mem_in; mem_out])
1263
                  (pp_locals m)
1264
                  (inputs @ outputs))
1265
              (pp_implies
1266
                 (pp_and
1267
                    (pp_and_l
1268
                       (fun fmt n ->
1269
                          (if n = k then
1270
                             pp_k_induction_inductive_case
1271
                           else
1272
                             pp_k_induction_base_case)
1273
                            m
1274
                            pp_print_string
1275
                            pp_print_string
1276
                            (pp_comma_list pp_var_decl)
1277
                            fmt
1278
                            (n, mem_in, mem_out)))
1279
                    (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
1280
                 (pp_contract m)))))
1281
      fmt
1282
      ((),
1283
       ((),
1284
        (m_c.mstep.step_outputs,
1285
         ((),
1286
          (((l,
1287
             (m_c.mname.node_id,
1288
              m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
1289
              "", "")), c))))))
1290

  
1291

  
1292
  let pp_k_induction m fmt (_, _, k as c_m_k) =
1293
    pp_acsl_cut
1294
      (fun fmt () -> fprintf fmt "%a@,@,%a@,@,%a@,@,%a@,@,%a"
1295
          pp_init_def m
1296
          (pp_base_cases m) c_m_k
1297
          (pp_inductive_case m) c_m_k
1298
          (pp_k_induction_lemmas m) k
1299
          (pp_k_induction_axiom m) c_m_k)
1300
      fmt
1301
      ()
1302

  
1303
  let pp_proof_annotation m m_c fmt c =
1304
    let pp m_c fmt = function
1305
      | Kinduction k ->
1306
        pp_k_induction m fmt (c, m_c, k)
1307
    in
1308
    match m_c with
1309
    | Some m_c ->
1310
      pp_print_option (pp m_c) fmt c.mc_proof
1311
    | None -> ()
1001 1312

  
1002 1313
  let pp_step_spec fmt machines self mem m =
1003 1314
    let name = m.mname.node_id in
......
1014 1325
    let pp_if_outputs pp =
1015 1326
      if outputs = [] then pp_print_nothing else pp
1016 1327
    in
1017
    let spec = m.mspec.mnode_spec in
1328
    let c, m_c = contract_of machines m in
1018 1329
    (* (\* prevent printing an ensures clause with contract name *\)
1019 1330
     * let spec =
1020 1331
     *   match m.mspec.mnode_spec with
......
1022 1333
     *   | s -> s
1023 1334
     * in *)
1024 1335
    let pp_spec = pp_print_option
1025
        (if m.mis_contract then pp_print_nothing else pp_ensures (pp_node_spec m)) in
1336
        (if m.mis_contract then pp_print_nothing else pp_ensures (pp_contract m)) in
1337
    let pp_spec_vars, pp_assigns_spec_vars =
1338
      match m.mspec.mnode_spec with
1339
      | Some (NodeSpec f) ->
1340
        let m_f = find_machine f machines in
1341
        pp_acsl_cut
1342
          (pp_ghost
1343
             (fun fmt () ->
1344
                fprintf
1345
                  fmt
1346
                  "@;<0 2>@[<v>%a@]"
1347
                  (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
1348
                     ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m))
1349
                  m_f.mstep.step_outputs)),
1350
        fun fmt () -> pp_assigns pp_var_decl fmt m_f.mstep.step_outputs
1351
      | _ -> pp_print_nothing, pp_print_nothing
1352
    in
1353
    pp_print_option (pp_proof_annotation m m_c) fmt c;
1354
    pp_spec_vars fmt ();
1026 1355
    pp_acsl_cut
1027 1356
      ~ghost:m.mis_contract
1028 1357
      (fun fmt () ->
1029 1358
        if fst (get_stateless_status m) then
1030 1359
          fprintf
1031 1360
            fmt
1032
            "%a@,%a@,%a@,%a@,%a"
1361
            "%a@,%a@,%a@,%a@,%a@,%a"
1033 1362
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1034 1363
            outputs
1035 1364
            (pp_if_outputs (pp_requires pp_separated''))
1036 1365
            outputs
1366
            pp_assigns_spec_vars ()
1037 1367
            (pp_assigns pp_ptr_decl)
1038 1368
            outputs
1039 1369
            (pp_ensures (pp_transition_aux' m))
1040 1370
            (name, inputs @ outputs, "", "")
1041 1371
            pp_spec
1042
            spec
1372
            c
1043 1373
        else
1044 1374
          fprintf
1045 1375
            fmt
1046
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
1376
            "%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
1047 1377
            (pp_if_outputs (pp_requires (pp_valid pp_var_decl)))
1048 1378
            outputs
1049 1379
            (pp_requires pp_mem_valid')
......
1059 1389
                    (if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
1060 1390
            (name, inputs @ outputs, mem, mem)
1061 1391
            pp_spec
1062
            spec
1392
            c
1393
            pp_assigns_spec_vars ()
1063 1394
            (pp_assigns pp_ptr_decl)
1064 1395
            outputs
1065 1396
            (pp_assigns (pp_reg self))
......
1131 1462

  
1132 1463
  let pp_contract fmt machines _self m =
1133 1464
    match m.mspec.mnode_spec with
1134
    | Some (NodeSpec (f, _)) ->
1465
    | Some (NodeSpec f) ->
1135 1466
      let m_f = find_machine f machines in
1136
      pp_acsl_cut
1467
      pp_acsl_line'_cut
1137 1468
        (pp_ghost
1138 1469
           (fun fmt () ->
1139 1470
              fprintf
1140 1471
                fmt
1141
                "@;<0 2>@[<v>%a%a(%a%a);@]"
1142
                (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m))
1143
                m_f.mstep.step_outputs
1472
                "%a(%a%a);"
1144 1473
                pp_machine_step_name
1145 1474
                m_f.mname.node_id
1146 1475
                (pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m))

Also available in: Unified diff