Skip to content
GitLab
Commit 910063bf authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Update the Cerberus dependency.

parent 561afc6c
Pipeline #42546 passed with stage
in 16 minutes and 38 seconds
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
View file @ 910063bf
......@@ -33,7 +33,7 @@ variables:
build-coq.8.12.0-timing:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
DENY_WARNINGS: "1"
only:
- master@iris/refinedc
......@@ -45,7 +45,7 @@ build-coq.8.12.0-timing:
build-coq.8.12.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
DENY_WARNINGS: "1"
only:
- /^ci/@iris/refinedc
......@@ -53,7 +53,7 @@ build-coq.8.12.0:
check-generated:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
DENY_WARNINGS: "1"
MAKE_TARGET: "check_generate_all"
# necessary because dune does not like running in parallel
......@@ -62,7 +62,7 @@ check-generated:
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
OPAM_PINS: "coq version 8.12.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV cerberus git git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
except:
only:
- triggers
......
README.md
View file @ 910063bf
......@@ -45,7 +45,7 @@ Assuming an appropriate [opam](https://opam.ocaml.org/doc/Install.html) switch
sudo apt-get install libmpfr-dev # Implicit Cerberus dependency.
opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
opam pin add refinedc "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
```
......@@ -114,7 +114,7 @@ dependencies can be made available to opam by running the following commands.
```bash
opam repo add coq-released "https://coq.inria.fr/opam/released"
opam repo add iris-dev "https://gitlab.mpi-sws.org/iris/opam.git"
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#6ea80db048080468761499238fa0d045222ccc52"
opam pin add -n -y cerberus "git+https://github.com/rems-project/cerberus.git#9f3a825a5f32a8245101a57105a5598a1adf6879"
```
You can then finally install RefinedC with the following command, or rather
decide to install it from a local clone to have access to various examples.
......
frontend/ail_to_coq.ml
View file @ 910063bf
......@@ -78,7 +78,10 @@ let collect_rc_attrs : Annot.attributes -> rc_attr list =
mkloc id (register_loc rc_locs loc)
in
let rc_attr_args =
let fn (loc, s) = mkloc s (register_str_loc rc_locs loc) in
let fn (loc, s, _) =
(* FIXME record data for location computation. *)
mkloc s (register_str_loc rc_locs loc)
in
List.map fn attr_args
in
{rc_attr_id; rc_attr_args} :: acc
......@@ -190,7 +193,8 @@ let rec macro_annot_to_list e =
let open AilSyntax in
let get_expr e =
match e with
| AnnotatedExpression(_, _, _, AilEarray_decay(AnnotatedExpression(_, _, _, AilEstr(_, strs)))) -> MacroString(String.concat "" strs)
| AnnotatedExpression(_, _, _, AilEarray_decay(AnnotatedExpression(_, _, _, AilEstr(_, strs)))) ->
MacroString(String.concat "" (List.concat (List.map snd strs)))
| _ -> MacroExpr(e)
in
match e with
......@@ -658,6 +662,8 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
| _ ->
not_impl loc "expr function_decay (not an ident)"
in res
| AilEgcc_statement ->
Panic.panic loc "Not implemented GCC statement expr." (* TODO *)
in
match (goal_ty, res_ty) with
| (None , _ )
......@@ -912,12 +918,12 @@ let warn_ignored_attrs so attrs =
| AilSskip -> "a skip"
| AilSexpr(_) -> "an expression"
| AilSif(_,_,_) -> "an if statement"
| AilSwhile(_,_) -> "a while loop"
| AilSdo(_,_) -> "a do-while loop"
| AilSwhile(_,_,_) -> "a while loop"
| AilSdo(_,_,_) -> "a do-while loop"
| AilSswitch(_,_) -> "a switch statement"
| AilScase(_,_) -> "a case statement"
| AilSdefault(_) -> "a default statement"
| AilSlabel(_,_) -> "a label"
| AilSlabel(_,_,_) -> "a label"
| AilSdeclaration(_) -> "a declaration"
| AilSpar(_) -> "a par statement"
| AilSreg_store(_,_) -> "a register store statement"
......@@ -1126,7 +1132,7 @@ let translate_block stmts blocks ret_ty =
(blocks, mkloc (Goto(id_else)) s.loc)
in
translate_bool_expr then_goto else_goto blocks e
| AilSwhile(e,s) ->
| AilSwhile(e,s,_) ->
let attrs = extra_attrs @ attrs in
let id_cond = fresh_block_id () in
let id_body = fresh_block_id () in
......@@ -1159,7 +1165,7 @@ let translate_block stmts blocks ret_ty =
add_block ~annots id_cond s blocks
in
(locate (Goto(id_cond)), blocks)
| AilSdo(s,e) ->
| AilSdo(s,e,_) ->
let attrs = extra_attrs @ attrs in
let id_cond = fresh_block_id () in
let id_body = fresh_block_id () in
......@@ -1296,7 +1302,7 @@ let translate_block stmts blocks ret_ty =
(* Update the default ref. *)
default_ref := Some(default_s);
(default_s, blocks)
| AilSlabel(l,s) ->
| AilSlabel(l,s,_) ->
let (s, blocks) = trans extra_attrs swstk ks (s :: stmts) blocks in
let blocks = add_block (sym_to_str l) s blocks in
(locate (Goto(sym_to_str l)), blocks)
......
frontend/cerb_wrapper.ml
View file @ 910063bf
......@@ -27,13 +27,17 @@ let impl_name =
try Sys.getenv "IMPL_NAME" with Not_found ->
"gcc_4.9.0_x86_64-apple-darwin10.8.0"
let set_cerb_conf () =
let open Global_ocaml in
set_cerb_conf false Random false Basic false false false false
let frontend cpp_cmd filename =
let conf =
{ debug_level = 0 ; pprints = [] ; astprints = [] ; ppflags = []
; typecheck_core = false ; rewrite_core = false
; sequentialise_core = false ; cpp_cmd ; cpp_stderr = true }
in
Global_ocaml.(set_cerb_conf false Random false Basic false false false);
set_cerb_conf ();
Ocaml_implementation.(set (HafniumImpl.impl));
load_core_stdlib () >>= fun stdlib ->
load_core_impl stdlib impl_name >>= fun impl ->
......@@ -45,7 +49,7 @@ let run_cpp cpp_cmd filename =
; typecheck_core = false ; rewrite_core = false
; sequentialise_core = false ; cpp_cmd ; cpp_stderr = true }
in
Global_ocaml.(set_cerb_conf false Random false Basic false false false);
set_cerb_conf ();
cpp (conf, io) ~filename
let cpp_cmd config =
......
frontend/warn.ml
View file @ 910063bf
......@@ -276,6 +276,8 @@ let points_to classify expr =
[]
| AilEunion (_, _, e_opt) ->
[]
| AilEgcc_statement ->
Panic.panic loc "Not implemented GCC statement expr." (* TODO *)
in
aux expr
......@@ -411,7 +413,8 @@ let rec taint_expr points_to (AnnotatedExpression (_, _, loc, expr_)) =
merge_pointsto (List.map (function (_, Some e) -> self e | (_, None) -> []) xs)
| AilEva_copy (e1, e2) ->
merge_pointsto [self e1; self e2]
| AilEgcc_statement ->
Panic.panic loc "Not implemented GCC statement expr." (* TODO *)
let taints_of_functions sigm =
List.fold_left (fun acc (sym_decl, (_, _, decl)) ->
......@@ -454,13 +457,13 @@ let taints_of_functions sigm =
merge_pointsto (List.map (fold_stmt env') ss)
| AilSif (e, s1, s2) ->
merge_pointsto [taint_expr e; fold_stmt env s1; fold_stmt env s2]
| AilSwhile (e, s)
| AilSdo (s, e)
| AilSwhile (e, s, _)
| AilSdo (s, e, _)
| AilSswitch (e, s) ->
merge_pointsto [taint_expr e; fold_stmt env s]
| AilScase (_, s)
| AilSdefault s
| AilSlabel (_, s) ->
| AilSlabel (_, s, _) ->
fold_stmt env s
| AilSdeclaration xs ->
merge_pointsto (List.map (fun (_, e) -> taint_expr e) xs)
......@@ -589,6 +592,8 @@ let warn_unseq taints_map expr =
merge_status (List.map (function (_, Some e) -> aux e | (_, None) -> NO_CALL) xs)
| AilEva_copy (e1, e2) ->
merge_status [aux e1; aux e2]
| AilEgcc_statement ->
Panic.panic loc "Not implemented GCC statement expr." (* TODO *)
in
ignore (aux expr)
......@@ -709,7 +714,10 @@ let warn_file (_, sigm) =
self e
| None ->
()
end in
end
| AilEgcc_statement ->
Panic.panic loc "Not implemented GCC statement expr." (* TODO *)
in
let rec aux env (AnnotatedStatement (loc, _, stmt_)) =
let self = aux env in
let warn_unseq e = warn_unseq taints_map e in
......@@ -736,11 +744,11 @@ let warn_file (_, sigm) =
warn_unseq e;
self s1;
self s2
| AilSwhile (e, s) ->
| AilSwhile (e, s, _) ->
self s;
aux_expr env e;
warn_unseq e
| AilSdo (s, e) ->
| AilSdo (s, e, _) ->
aux_expr env e;
warn_unseq e;
self s
......@@ -754,7 +762,7 @@ let warn_file (_, sigm) =
self s
| AilScase (_, s)
| AilSdefault s
| AilSlabel (_, s) ->
| AilSlabel (_, s, _) ->
self s
| AilSgoto _ ->
()
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment