Skip to content

Commit bdd48ad

Browse files
lfrenotlfrenot
committed
Working registers and tests
1 parent f87c292 commit bdd48ad

File tree

6 files changed

+153
-13
lines changed

6 files changed

+153
-13
lines changed

Diff for: ‎src/lib/state.ml

+26
Original file line numberDiff line numberDiff line change
@@ -834,6 +834,32 @@ let register_refs_coq doc_id coq_record_update env registers =
834834
in
835835
separate hardline [generic_convs; refs; getters_setters]
836836

837+
let register_refs_lean doc_id doc_typ registers =
838+
let generic_convs = separate_map hardline string [""; "variable [MonadReg]"; ""; "open MonadReg"; ""] in
839+
let register_ref (typ, id, _) =
840+
let idd = doc_id id in
841+
let typp = doc_typ typ in
842+
concat
843+
[
844+
string " set_";
845+
idd;
846+
colon;
847+
space;
848+
typp;
849+
string " -> SailM Unit";
850+
hardline;
851+
string " get_";
852+
idd;
853+
colon;
854+
space;
855+
string "SailM (";
856+
typp;
857+
string ")";
858+
]
859+
in
860+
let refs = separate_map hardline register_ref registers in
861+
separate hardline [string "class MonadReg where"; refs; generic_convs]
862+
837863
let generate_regstate_defs ctx env ast =
838864
let defs = ast.defs in
839865
let registers = find_registers defs in

Diff for: ‎src/sail_lean_backend/pretty_print_lean.ml

+89-5
Original file line numberDiff line numberDiff line change
@@ -257,14 +257,82 @@ let string_of_exp_con (E_aux (e, _)) =
257257
| E_vector _ -> "E_vector"
258258
| E_let _ -> "E_let"
259259

260+
let string_of_pat_con (P_aux (p, _)) =
261+
match p with
262+
| P_app _ -> "P_app"
263+
| P_wild -> "P_wild"
264+
| P_lit _ -> "P_lit"
265+
| P_or _ -> "P_or"
266+
| P_not _ -> "P_not"
267+
| P_as _ -> "P_as"
268+
| P_typ _ -> "P_typ"
269+
| P_id _ -> "P_id"
270+
| P_var _ -> "P_var"
271+
| P_vector _ -> "P_vector"
272+
| P_vector_concat _ -> "P_vector_concat"
273+
| P_vector_subrange _ -> "P_vector_subrange"
274+
| P_tuple _ -> "P_tuple"
275+
| P_list _ -> "P_list"
276+
| P_cons _ -> "P_cons"
277+
| P_string_append _ -> "P_string_append"
278+
| P_struct _ -> "P_struct"
279+
280+
let rec doc_pat ctxt apat_needed (P_aux (p, (l, annot)) as pat) =
281+
let env = env_of_annot (l, annot) in
282+
let typ = Env.expand_synonyms env (typ_of_annot (l, annot)) in
283+
match p with
284+
| P_typ (ptyp, p) ->
285+
let doc_p = doc_pat ctxt true p in
286+
doc_p
287+
| P_id id -> doc_id_ctor id
288+
| _ -> failwith ("Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.")
289+
290+
(* Copied from the Coq PP *)
291+
let rebind_cast_pattern_vars pat typ exp =
292+
let rec aux pat typ =
293+
match (pat, typ) with
294+
| P_aux (P_typ (target_typ, P_aux (P_id id, (l, ann))), _), source_typ when not (is_enum (env_of exp) id) ->
295+
if Typ.compare target_typ source_typ == 0 then []
296+
else (
297+
let l = Parse_ast.Generated l in
298+
let cast_annot = Type_check.replace_typ source_typ ann in
299+
let e_annot = Type_check.mk_tannot (env_of exp) source_typ in
300+
[LB_aux (LB_val (pat, E_aux (E_id id, (l, e_annot))), (l, ann))]
301+
)
302+
| P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs)
303+
| _ -> []
304+
in
305+
let add_lb (E_aux (_, ann) as exp) lb = E_aux (E_let (lb, exp), ann) in
306+
(* Don't introduce new bindings at the top-level, we'd just go into a loop. *)
307+
let lbs =
308+
match (pat, typ) with
309+
| P_aux (P_tuple pats, _), Typ_aux (Typ_tuple typs, _) -> List.concat (List.map2 aux pats typs)
310+
| _ -> []
311+
in
312+
List.fold_left add_lb exp lbs
313+
260314
let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
261315
let env = env_of_tannot annot in
262316
match e with
263317
| E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *)
264318
| E_lit l -> doc_lit l
265319
| E_app (Id_aux (Id "internal_pick", _), _) ->
266320
string "sorry" (* TODO replace by actual implementation of internal_pick *)
267-
| E_internal_plet _ -> string "sorry" (* TODO replace by actual implementation of internal_plet *)
321+
| E_internal_plet (pat, e1, e2) ->
322+
(* doc_exp ctxt e1 ^^ hardline ^^ doc_exp ctxt e2 *)
323+
let e0 = doc_pat ctxt false pat in
324+
let e1_pp = doc_exp ctxt e1 in
325+
let e2' = rebind_cast_pattern_vars pat (typ_of e1) e2 in
326+
let e2_pp = doc_exp ctxt e2' in
327+
(* infix 0 1 middle e1_pp e2_pp *)
328+
let e0_pp =
329+
begin
330+
match pat with
331+
| P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ""
332+
| _ -> separate space [string "let"; e0; string ":="] ^^ space
333+
end
334+
in
335+
e0_pp ^^ e1_pp ^^ hardline ^^ e2_pp
268336
| E_app (f, args) ->
269337
let d_id =
270338
if Env.is_extern f env "lean" then string (Env.get_extern f env "lean")
@@ -273,7 +341,13 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
273341
let d_args = List.map (doc_exp ctxt) args in
274342
nest 2 (parens (flow (break 1) (d_id :: d_args)))
275343
| E_vector vals -> failwith "vector found"
276-
| E_typ (typ, e) -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ])
344+
| E_typ (typ, e) -> (
345+
match e with
346+
| E_aux (E_assign _, _) -> doc_exp ctxt e
347+
| E_aux (E_app (Id_aux (Id "internal_pick", _), _), _) ->
348+
string "return " ^^ nest 7 (parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ]))
349+
| _ -> parens (separate space [doc_exp ctxt e; colon; doc_typ ctxt typ])
350+
)
277351
| E_tuple es -> parens (separate_map (comma ^^ space) (doc_exp ctxt) es)
278352
| E_let (LB_aux (LB_val (lpat, lexp), _), e) ->
279353
let id =
@@ -290,6 +364,13 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
290364
| E_struct_update (exp, fexps) ->
291365
let args = List.map (doc_fexp ctxt) fexps in
292366
braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space)
367+
| E_assign ((LE_aux (le_act, tannot) as le), e) -> (
368+
match le_act with
369+
| LE_id id | LE_typ (_, id) -> string "set_" ^^ doc_id_ctor id ^^ space ^^ doc_exp ctxt e
370+
| LE_deref e -> string "sorry /- deref -/"
371+
| _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet")
372+
)
373+
| E_internal_return e -> nest 2 (string "return" ^^ space ^^ nest 5 (doc_exp ctxt e))
293374
| _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")
294375

295376
and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp
@@ -353,8 +434,7 @@ let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) =
353434

354435
let doc_funcl_body (FCL_aux (FCL_funcl (id, pexp), annot)) =
355436
let _, _, exp, _ = destruct_pexp pexp in
356-
let is_monadic = effectful (effect_of exp) in
357-
if is_monadic then nest 2 (flow (break 1) [string "return"; doc_exp empty_context exp]) else doc_exp empty_context exp
437+
doc_exp empty_context exp
358438

359439
let doc_funcl funcl =
360440
let comment, signature = doc_funcl_init funcl in
@@ -415,6 +495,10 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en
415495

416496
let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
417497
let defs = remove_imports defs 0 in
498+
let regs = State.find_registers defs in
499+
let register_refs =
500+
match regs with [] -> empty | _ -> State.register_refs_lean doc_id_ctor (doc_typ empty_context) regs ^^ hardline
501+
in
418502
let output : document = separate_map empty (doc_def empty_context) defs in
419-
print o output;
503+
print o (register_refs ^^ output);
420504
()

Diff for: ‎test/lean/bitfield.expected.lean

+13-7
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ open Sail
55
def cr_type := (BitVec 8)
66

77
def undefined_cr_type (lit : Unit) : SailM (BitVec 8) :=
8-
return ((undefined_bitvector 8) : (BitVec 8))
8+
((undefined_bitvector 8) : (BitVec 8))
99

1010
def Mk_cr_type (v : (BitVec 8)) : (BitVec 8) :=
1111
v
@@ -17,7 +17,8 @@ def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) :=
1717
(Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x)
1818

1919
def _set_cr_type_bits (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 8)) : SailM Unit :=
20-
return sorry
20+
let r := (reg_deref r_ref)
21+
sorry /- deref -/
2122

2223
def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) :=
2324
(Sail.BitVec.extractLsb v 7 4)
@@ -26,7 +27,8 @@ def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) :=
2627
(Sail.BitVec.updateSubrange v 7 4 x)
2728

2829
def _set_cr_type_CR0 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 4)) : SailM Unit :=
29-
return sorry
30+
let r := (reg_deref r_ref)
31+
sorry /- deref -/
3032

3133
def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) :=
3234
(Sail.BitVec.extractLsb v 3 2)
@@ -35,7 +37,8 @@ def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
3537
(Sail.BitVec.updateSubrange v 3 2 x)
3638

3739
def _set_cr_type_CR1 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit :=
38-
return sorry
40+
let r := (reg_deref r_ref)
41+
sorry /- deref -/
3942

4043
def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) :=
4144
(Sail.BitVec.extractLsb v 1 0)
@@ -44,7 +47,8 @@ def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) :=
4447
(Sail.BitVec.updateSubrange v 1 0 x)
4548

4649
def _set_cr_type_CR3 (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 2)) : SailM Unit :=
47-
return sorry
50+
let r := (reg_deref r_ref)
51+
sorry /- deref -/
4852

4953
def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) :=
5054
(Sail.BitVec.extractLsb v 6 6)
@@ -53,7 +57,8 @@ def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
5357
(Sail.BitVec.updateSubrange v 6 6 x)
5458

5559
def _set_cr_type_GT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit :=
56-
return sorry
60+
let r := (reg_deref r_ref)
61+
sorry /- deref -/
5762

5863
def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) :=
5964
(Sail.BitVec.extractLsb v 7 7)
@@ -62,7 +67,8 @@ def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) :=
6267
(Sail.BitVec.updateSubrange v 7 7 x)
6368

6469
def _set_cr_type_LT (r_ref : RegisterRef Unit Unit (BitVec 8)) (v : (BitVec 1)) : SailM Unit :=
65-
return sorry
70+
let r := (reg_deref r_ref)
71+
sorry /- deref -/
6672

6773
def initialize_registers : Unit :=
6874
()

Diff for: ‎test/lean/reg.expected.lean

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import Out.Sail.Sail
2+
3+
open Sail
4+
5+
class MonadReg where
6+
set_R0: (BitVec 64) -> SailM Unit
7+
get_R0: SailM ((BitVec 64))
8+
9+
variable [MonadReg]
10+
11+
open MonadReg
12+
13+
def initialize_registers : SailM Unit :=
14+
let w__0 := (undefined_bitvector 64)
15+
set_R0 w__0
16+

Diff for: ‎test/lean/reg.sail

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
default Order dec
2+
3+
$include <prelude.sail>
4+
5+
register R0 : bits(64)

Diff for: ‎test/lean/struct.expected.lean

+4-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@ structure My_struct where
77
field2 : (BitVec 1)
88

99
def undefined_My_struct (lit : Unit) : SailM My_struct :=
10-
return sorry
10+
let w__0 := (undefined_int ())
11+
let w__1 := (undefined_bit ())
12+
return { field1 := w__0
13+
field2 := w__1 }
1114

1215
def struct_field2 (s : My_struct) : (BitVec 1) :=
1316
s.field2

0 commit comments

Comments
 (0)