diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/deep_shallow_convert.lem | 526 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 10 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 550 |
3 files changed, 540 insertions, 546 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem new file mode 100644 index 00000000..aa16f069 --- /dev/null +++ b/src/gen_lib/deep_shallow_convert.lem @@ -0,0 +1,526 @@ +open import Pervasives_extra +open import Sail_impl_base +open import Interp +open import Interp_ast +open import Sail_values + + +class (ToFromInterpValue 'a) + val toInterpValue : 'a -> Interp.value + val fromInterpValue : Interp.value -> 'a +end + +let toInterValueBool = function + | true -> Interp.V_lit (L_aux (L_one) Unknown) + | false -> Interp.V_lit (L_aux (L_zero) Unknown) +end +let rec fromInterpValueBool v = match v with + | Interp.V_lit (L_aux (L_true) _) -> true + | Interp.V_lit (L_aux (L_false) _) -> false + | Interp.V_lit (L_aux (L_one) _) -> true + | Interp.V_lit (L_aux (L_zero) _) -> false + | Interp.V_tuple [v] -> fromInterpValueBool v + | v -> failwith ("fromInterpValue bool: unexpected value. " ^ + Interp.debug_print_value v) +end +instance (ToFromInterpValue bool) + let toInterpValue = toInterValueBool + let fromInterpValue = fromInterpValueBool +end + + +let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown) +let rec fromInterpValueUnit v = match v with + | Interp.V_lit (L_aux (L_unit) _) -> () + | Interp.V_tuple [v] -> fromInterpValueUnit v + | v -> failwith ("fromInterpValue unit: unexpected value. " ^ + Interp.debug_print_value v) +end +instance (ToFromInterpValue unit) + let toInterpValue = toInterpValueUnit + let fromInterpValue = fromInterpValueUnit +end + + +let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown) +let rec fromInterpValueInteger v = match v with + | Interp.V_lit (L_aux (L_num i) _) -> i + | Interp.V_tuple [v] -> fromInterpValueInteger v + | v -> failwith ("fromInterpValue integer: unexpected value. " ^ + Interp.debug_print_value v) +end +instance (ToFromInterpValue integer) + let toInterpValue = toInterpValueInteger + let fromInterpValue = fromInterpValueInteger +end + + +let toInterpValueString s = V_lit (L_aux (L_string s) Unknown) +let rec fromInterpValueString v = match v with + | Interp.V_lit (L_aux (L_string s) _) -> s + | Interp.V_tuple [v] -> fromInterpValueString v + | v -> failwith ("fromInterpValue integer: unexpected value. " ^ + Interp.debug_print_value v) +end +instance (ToFromInterpValue string) + let toInterpValue = toInterpValueString + let fromInterpValue = fromInterpValueString +end + + +let toInterpValueBitU = function + | I -> Interp.V_lit (L_aux (L_one) Unknown) + | O -> Interp.V_lit (L_aux (L_zero) Unknown) + | Undef -> Interp.V_lit (L_aux (L_undef) Unknown) +end +let rec fromInterpValueBitU v = match v with + | Interp.V_lit (L_aux (L_one) _) -> I + | Interp.V_lit (L_aux (L_zero) _) -> O + | Interp.V_lit (L_aux (L_undef) _) -> Undef + | Interp.V_lit (L_aux (L_true) _) -> I + | Interp.V_lit (L_aux (L_false) _) -> O + | Interp.V_tuple [v] -> fromInterpValueBitU v + | v -> failwith ("fromInterpValue bitU: unexpected value. " ^ + Interp.debug_print_value v) +end +instance (ToFromInterpValue bitU) + let toInterpValue = toInterpValueBitU + let fromInterpValue = fromInterpValueBitU +end + + +let tuple2ToInterpValue (a,b) = + V_tuple [toInterpValue a;toInterpValue b] +let rec tuple2FromInterpValue v = match v with + | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b) + | V_tuple [v] -> tuple2FromInterpValue v + | v -> failwith ("fromInterpValue a*b: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b)) + let toInterpValue = tuple2ToInterpValue + let fromInterpValue = tuple2FromInterpValue +end + + +let tuple3ToInterpValue (a,b,c) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c] +let rec tuple3FromInterpValue v = match v with + | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c) + | V_tuple [v] -> tuple3FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c => + (ToFromInterpValue ('a * 'b * 'c)) + let toInterpValue = tuple3ToInterpValue + let fromInterpValue = tuple3FromInterpValue +end + + +let tuple4ToInterpValue (a,b,c,d) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d] +let rec tuple4FromInterpValue v = match v with + | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b, + fromInterpValue c,fromInterpValue d) + | V_tuple [v] -> tuple4FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd => + (ToFromInterpValue ('a * 'b * 'c * 'd)) + let toInterpValue = tuple4ToInterpValue + let fromInterpValue = tuple4FromInterpValue +end + + +let tuple5ToInterpValue (a,b,c,d,e) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e] +let rec tuple5FromInterpValue v = match v with + | V_tuple [a;b;c;d;e] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e) + | V_tuple [v] -> tuple5FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e)) + let toInterpValue = tuple5ToInterpValue + let fromInterpValue = tuple5FromInterpValue +end + + +let tuple6ToInterpValue (a,b,c,d,e,f) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f] +let rec tuple6FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f) + | V_tuple [v] -> tuple6FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f)) + let toInterpValue = tuple6ToInterpValue + let fromInterpValue = tuple6FromInterpValue +end + + +let tuple7ToInterpValue (a,b,c,d,e,f,g) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g] +let rec tuple7FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g) + | V_tuple [v] -> tuple7FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g)) + let toInterpValue = tuple7ToInterpValue + let fromInterpValue = tuple7FromInterpValue +end + + +let tuple8ToInterpValue (a,b,c,d,e,f,g,h) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h] +let rec tuple8FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g;h] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g,fromInterpValue h) + | V_tuple [v] -> tuple8FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g 'h. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g, ToFromInterpValue 'h => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h)) + let toInterpValue = tuple8ToInterpValue + let fromInterpValue = tuple8FromInterpValue +end + + +let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; + toInterpValue i] +let rec tuple9FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g;h;i] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g,fromInterpValue h,fromInterpValue i) + | V_tuple [v] -> tuple9FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g, ToFromInterpValue 'h, + ToFromInterpValue 'i => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i)) + let toInterpValue = tuple9ToInterpValue + let fromInterpValue = tuple9FromInterpValue +end + + +let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; + toInterpValue i;toInterpValue j;] +let rec tuple10FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g;h;i;j] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g,fromInterpValue h,fromInterpValue i, + fromInterpValue j) + | V_tuple [v] -> tuple10FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g, ToFromInterpValue 'h, + ToFromInterpValue 'i, ToFromInterpValue 'j => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j)) + let toInterpValue = tuple10ToInterpValue + let fromInterpValue = tuple10FromInterpValue +end + + +let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; + toInterpValue i;toInterpValue j;toInterpValue k;] +let rec tuple11FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g;h;i;j;k] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g,fromInterpValue h,fromInterpValue i, + fromInterpValue j,fromInterpValue k) + | V_tuple [v] -> tuple11FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g, ToFromInterpValue 'h, + ToFromInterpValue 'i, ToFromInterpValue 'j, + ToFromInterpValue 'k => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k)) + let toInterpValue = tuple11ToInterpValue + let fromInterpValue = tuple11FromInterpValue +end + + +let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) = + V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; + toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; + toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;] +let rec tuple12FromInterpValue v = match v with + | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] -> + (fromInterpValue a,fromInterpValue b,fromInterpValue c, + fromInterpValue d,fromInterpValue e,fromInterpValue f, + fromInterpValue g,fromInterpValue h,fromInterpValue i, + fromInterpValue j,fromInterpValue k,fromInterpValue l) + | V_tuple [v] -> tuple12FromInterpValue v + | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k*l: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l. + ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd, + ToFromInterpValue 'e, ToFromInterpValue 'f, + ToFromInterpValue 'g, ToFromInterpValue 'h, + ToFromInterpValue 'i, ToFromInterpValue 'j, + ToFromInterpValue 'k, ToFromInterpValue 'l => + (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l)) + let toInterpValue = tuple12ToInterpValue + let fromInterpValue = tuple12FromInterpValue +end + + +let listToInterpValue l = V_list (List.map toInterpValue l) +let rec listFromInterpValue v = match v with + | V_list l -> List.map fromInterpValue l + | V_tuple [v] -> listFromInterpValue v + | v -> failwith ("fromInterpValue list 'a: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a)) + let toInterpValue = listToInterpValue + let fromInterpValue = listFromInterpValue +end + + +let vectorToInterpValue (Vector vs start direction) = + V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs) +let rec vectorFromInterpValue v = match v with + | V_vector start direction vs -> + Vector (List.map fromInterpValue vs) (integerFromNat start) + (match direction with | IInc -> true | IDec -> false end) + | V_vector_sparse start length direction valuemap defaultval -> + make_indexed_vector + (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap) + (fromInterpValue defaultval) + (integerFromNat start) (integerFromNat length) + (match direction with | IInc -> true | IDec -> false end) + | V_tuple [v] -> vectorFromInterpValue v + | v -> failwith ("fromInterpValue vector 'a: unexpected value. " ^ + Interp.debug_print_value v) + end +instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a)) + let toInterpValue = vectorToInterpValue + let fromInterpValue = vectorFromInterpValue +end + +(* Here the type information is not accurate: instead of T_id "option" it should + be T_app (T_id "option") (...), but temporarily we'll do it like this. The + same thing has to be fixed in pretty_print.ml when we're generating the + type-class instances. *) +let maybeToInterpValue = function + | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown)) + | Just a -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a) + end +let rec maybeFromInterpValue v = match v with + | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing + | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v) + | V_tuple [v] -> maybeFromInterpValue v + | v -> failwith ("fromInterpValue maybe 'a: unexpected value. " ^ + Interp.debug_print_value v) + end + +instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a)) + let toInterpValue = maybeToInterpValue + let fromInterpValue = maybeFromInterpValue +end + + +module SI = Interp +module SIA = Interp_ast + + +let read_kindToInterpValue = function + | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ()) + | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) + | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) + | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) + | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) + | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) + | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) + | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) + end +let rec read_kindFromInterpValue v = match v with + | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain + | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag + | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve + | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve + | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire + | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive + | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire + | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream + | V_tuple [v] -> read_kindFromInterpValue v + | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue read_kind) + let toInterpValue = read_kindToInterpValue + let fromInterpValue = read_kindFromInterpValue +end + + +let write_kindToInterpValue = function + | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ()) + | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) + | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) + | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) + | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) + | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) + | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) + end +let rec write_kindFromInterpValue v = match v with + | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain + | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag + | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional + | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional + | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release + | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive + | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release + | V_tuple [v] -> write_kindFromInterpValue v + | v -> failwith ("fromInterpValue write_kind: unexpected value " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue write_kind) + let toInterpValue = write_kindToInterpValue + let fromInterpValue = write_kindFromInterpValue +end + + +let barrier_kindToInterpValue = function + | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ()) + | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ()) + | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ()) + | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ()) + | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ()) + | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ()) + | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ()) + | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ()) + | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) + | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) + | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) + end +let rec barrier_kindFromInterpValue v = match v with + | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync + | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync + | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio + | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync + | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB + | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST + | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD + | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB + | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST + | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD + | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB + | V_tuple [v] -> barrier_kindFromInterpValue v + | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue barrier_kind) + let toInterpValue = barrier_kindToInterpValue + let fromInterpValue = barrier_kindFromInterpValue +end + + +let instruction_kindToInterpValue = function + | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) + | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) + | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) + | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + end +let rec instruction_kindFromInterpValue v = match v with + | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v) + | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) + | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) + | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple + | V_tuple [v] -> instruction_kindFromInterpValue v + | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue instruction_kind) + let toInterpValue = instruction_kindToInterpValue + let fromInterpValue = instruction_kindFromInterpValue +end + +let regfpToInterpValue = function + | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + end + +let rec regfpFromInterpValue v = match v with + | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v) + | SI.V_tuple [v] -> regfpFromInterpValue v + | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v) + end + +instance (ToFromInterpValue regfp) + let toInterpValue = regfpToInterpValue + let fromInterpValue = regfpFromInterpValue +end + + + + diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 5532089d..f770042c 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -2,14 +2,10 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values - import Interp_interface -(* this needs to go away: it's only so we can make the ppcmem outcome types the -same *) - -val return : forall 's 'a. 'a -> outcome 's 'a +val return : forall 'a. 'a -> outcome 'a let return a = Done a -val bind : forall 's 'a 'b. outcome 's 'a -> ('a -> outcome 's 'b) -> outcome 's 'b +val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b let rec bind m f = match m with | Done a -> f a | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) @@ -26,7 +22,7 @@ let rec bind m f = match m with end -type M 'a = Sail_impl_base.outcome Interp_interface.instruction_state 'a +type M 'a = outcome 'a let inline (>>=) = bind val (>>) : forall 'b. M unit -> M 'b -> M 'b diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 2ad25110..3357fe3d 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,6 +1,4 @@ open import Pervasives_extra -open import Interp (* only for converting between shallow- and deep-embedding values *) -open import Interp_ast (* only for converting between shallow- and deep-embedding values *) open import Sail_impl_base @@ -18,7 +16,6 @@ let rec replace bs ((n : integer),b') = match bs with end - (*** Bits *) type bitU = O | I | Undef @@ -887,9 +884,6 @@ let assert' b msg_opt = end in if bitU_to_bool b then () else failwith msg - - - (* convert numbers unsafely to naturals *) class (ToNatural 'a) val toNatural : 'a -> natural end @@ -906,532 +900,24 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) = toNatural n5) - -(* convert to/from interpreter values *) - -class (ToFromInterpValue 'a) - val toInterpValue : 'a -> Interp.value - val fromInterpValue : Interp.value -> 'a -end - -let toInterValueBool = function - | true -> Interp.V_lit (L_aux (L_one) Unknown) - | false -> Interp.V_lit (L_aux (L_zero) Unknown) -end -let rec fromInterpValueBool v = match v with - | Interp.V_lit (L_aux (L_true) _) -> true - | Interp.V_lit (L_aux (L_false) _) -> false - | Interp.V_lit (L_aux (L_one) _) -> true - | Interp.V_lit (L_aux (L_zero) _) -> false - | Interp.V_tuple [v] -> fromInterpValueBool v - | v -> failwith ("fromInterpValue bool: unexpected value. " ^ - Interp.debug_print_value v) -end -instance (ToFromInterpValue bool) - let toInterpValue = toInterValueBool - let fromInterpValue = fromInterpValueBool -end - - -let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown) -let rec fromInterpValueUnit v = match v with - | Interp.V_lit (L_aux (L_unit) _) -> () - | Interp.V_tuple [v] -> fromInterpValueUnit v - | v -> failwith ("fromInterpValue unit: unexpected value. " ^ - Interp.debug_print_value v) -end -instance (ToFromInterpValue unit) - let toInterpValue = toInterpValueUnit - let fromInterpValue = fromInterpValueUnit -end - - -let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown) -let rec fromInterpValueInteger v = match v with - | Interp.V_lit (L_aux (L_num i) _) -> i - | Interp.V_tuple [v] -> fromInterpValueInteger v - | v -> failwith ("fromInterpValue integer: unexpected value. " ^ - Interp.debug_print_value v) -end -instance (ToFromInterpValue integer) - let toInterpValue = toInterpValueInteger - let fromInterpValue = fromInterpValueInteger -end - - -let toInterpValueString s = V_lit (L_aux (L_string s) Unknown) -let rec fromInterpValueString v = match v with - | Interp.V_lit (L_aux (L_string s) _) -> s - | Interp.V_tuple [v] -> fromInterpValueString v - | v -> failwith ("fromInterpValue integer: unexpected value. " ^ - Interp.debug_print_value v) -end -instance (ToFromInterpValue string) - let toInterpValue = toInterpValueString - let fromInterpValue = fromInterpValueString -end - - -let toInterpValueBitU = function - | I -> Interp.V_lit (L_aux (L_one) Unknown) - | O -> Interp.V_lit (L_aux (L_zero) Unknown) - | Undef -> Interp.V_lit (L_aux (L_undef) Unknown) -end -let rec fromInterpValueBitU v = match v with - | Interp.V_lit (L_aux (L_one) _) -> I - | Interp.V_lit (L_aux (L_zero) _) -> O - | Interp.V_lit (L_aux (L_undef) _) -> Undef - | Interp.V_lit (L_aux (L_true) _) -> I - | Interp.V_lit (L_aux (L_false) _) -> O - | Interp.V_tuple [v] -> fromInterpValueBitU v - | v -> failwith ("fromInterpValue bitU: unexpected value. " ^ - Interp.debug_print_value v) -end -instance (ToFromInterpValue bitU) - let toInterpValue = toInterpValueBitU - let fromInterpValue = fromInterpValueBitU -end - - -let tuple2ToInterpValue (a,b) = - V_tuple [toInterpValue a;toInterpValue b] -let rec tuple2FromInterpValue v = match v with - | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b) - | V_tuple [v] -> tuple2FromInterpValue v - | v -> failwith ("fromInterpValue a*b: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b)) - let toInterpValue = tuple2ToInterpValue - let fromInterpValue = tuple2FromInterpValue -end - - -let tuple3ToInterpValue (a,b,c) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c] -let rec tuple3FromInterpValue v = match v with - | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c) - | V_tuple [v] -> tuple3FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c => - (ToFromInterpValue ('a * 'b * 'c)) - let toInterpValue = tuple3ToInterpValue - let fromInterpValue = tuple3FromInterpValue -end - - -let tuple4ToInterpValue (a,b,c,d) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d] -let rec tuple4FromInterpValue v = match v with - | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b, - fromInterpValue c,fromInterpValue d) - | V_tuple [v] -> tuple4FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd => - (ToFromInterpValue ('a * 'b * 'c * 'd)) - let toInterpValue = tuple4ToInterpValue - let fromInterpValue = tuple4FromInterpValue -end - - -let tuple5ToInterpValue (a,b,c,d,e) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e] -let rec tuple5FromInterpValue v = match v with - | V_tuple [a;b;c;d;e] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e) - | V_tuple [v] -> tuple5FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e)) - let toInterpValue = tuple5ToInterpValue - let fromInterpValue = tuple5FromInterpValue -end - - -let tuple6ToInterpValue (a,b,c,d,e,f) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f] -let rec tuple6FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f) - | V_tuple [v] -> tuple6FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f)) - let toInterpValue = tuple6ToInterpValue - let fromInterpValue = tuple6FromInterpValue -end - - -let tuple7ToInterpValue (a,b,c,d,e,f,g) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g] -let rec tuple7FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g) - | V_tuple [v] -> tuple7FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g)) - let toInterpValue = tuple7ToInterpValue - let fromInterpValue = tuple7FromInterpValue -end - - -let tuple8ToInterpValue (a,b,c,d,e,f,g,h) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h] -let rec tuple8FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g;h] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g,fromInterpValue h) - | V_tuple [v] -> tuple8FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g 'h. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g, ToFromInterpValue 'h => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h)) - let toInterpValue = tuple8ToInterpValue - let fromInterpValue = tuple8FromInterpValue -end - - -let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; - toInterpValue i] -let rec tuple9FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g;h;i] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g,fromInterpValue h,fromInterpValue i) - | V_tuple [v] -> tuple9FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g, ToFromInterpValue 'h, - ToFromInterpValue 'i => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i)) - let toInterpValue = tuple9ToInterpValue - let fromInterpValue = tuple9FromInterpValue -end - - -let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; - toInterpValue i;toInterpValue j;] -let rec tuple10FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g;h;i;j] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g,fromInterpValue h,fromInterpValue i, - fromInterpValue j) - | V_tuple [v] -> tuple10FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g, ToFromInterpValue 'h, - ToFromInterpValue 'i, ToFromInterpValue 'j => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j)) - let toInterpValue = tuple10ToInterpValue - let fromInterpValue = tuple10FromInterpValue -end - - -let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; - toInterpValue i;toInterpValue j;toInterpValue k;] -let rec tuple11FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g;h;i;j;k] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g,fromInterpValue h,fromInterpValue i, - fromInterpValue j,fromInterpValue k) - | V_tuple [v] -> tuple11FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g, ToFromInterpValue 'h, - ToFromInterpValue 'i, ToFromInterpValue 'j, - ToFromInterpValue 'k => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k)) - let toInterpValue = tuple11ToInterpValue - let fromInterpValue = tuple11FromInterpValue -end - - -let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) = - V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d; - toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h; - toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;] -let rec tuple12FromInterpValue v = match v with - | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] -> - (fromInterpValue a,fromInterpValue b,fromInterpValue c, - fromInterpValue d,fromInterpValue e,fromInterpValue f, - fromInterpValue g,fromInterpValue h,fromInterpValue i, - fromInterpValue j,fromInterpValue k,fromInterpValue l) - | V_tuple [v] -> tuple12FromInterpValue v - | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k*l: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l. - ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd, - ToFromInterpValue 'e, ToFromInterpValue 'f, - ToFromInterpValue 'g, ToFromInterpValue 'h, - ToFromInterpValue 'i, ToFromInterpValue 'j, - ToFromInterpValue 'k, ToFromInterpValue 'l => - (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l)) - let toInterpValue = tuple12ToInterpValue - let fromInterpValue = tuple12FromInterpValue -end - - -let listToInterpValue l = V_list (List.map toInterpValue l) -let rec listFromInterpValue v = match v with - | V_list l -> List.map fromInterpValue l - | V_tuple [v] -> listFromInterpValue v - | v -> failwith ("fromInterpValue list 'a: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a)) - let toInterpValue = listToInterpValue - let fromInterpValue = listFromInterpValue -end - - -let vectorToInterpValue (Vector vs start direction) = - V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs) -let rec vectorFromInterpValue v = match v with - | V_vector start direction vs -> - Vector (List.map fromInterpValue vs) (integerFromNat start) - (match direction with | IInc -> true | IDec -> false end) - | V_vector_sparse start length direction valuemap defaultval -> - make_indexed_vector - (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap) - (fromInterpValue defaultval) - (integerFromNat start) (integerFromNat length) - (match direction with | IInc -> true | IDec -> false end) - | V_tuple [v] -> vectorFromInterpValue v - | v -> failwith ("fromInterpValue vector 'a: unexpected value. " ^ - Interp.debug_print_value v) - end -instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a)) - let toInterpValue = vectorToInterpValue - let fromInterpValue = vectorFromInterpValue -end - -(* Here the type information is not accurate: instead of T_id "option" it should - be T_app (T_id "option") (...), but temporarily we'll do it like this. The - same thing has to be fixed in pretty_print.ml when we're generating the - type-class instances. *) -let maybeToInterpValue = function - | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown)) - | Just a -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a) - end -let rec maybeFromInterpValue v = match v with - | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing - | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v) - | V_tuple [v] -> maybeFromInterpValue v - | v -> failwith ("fromInterpValue maybe 'a: unexpected value. " ^ - Interp.debug_print_value v) - end - -instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a)) - let toInterpValue = maybeToInterpValue - let fromInterpValue = maybeFromInterpValue -end - - -module SI = Interp -module SIA = Interp_ast - - -let read_kindToInterpValue = function - | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ()) - | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) - | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) - | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) - | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) - | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) - | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) - | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) - end -let rec read_kindFromInterpValue v = match v with - | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain - | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag - | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve - | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve - | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire - | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive - | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire - | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream - | V_tuple [v] -> read_kindFromInterpValue v - | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^ - Interp.debug_print_value v) - end -instance (ToFromInterpValue read_kind) - let toInterpValue = read_kindToInterpValue - let fromInterpValue = read_kindFromInterpValue -end - - -let write_kindToInterpValue = function - | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ()) - | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) - | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) - | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) - | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) - | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) - | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) - end -let rec write_kindFromInterpValue v = match v with - | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain - | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag - | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional - | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional - | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release - | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive - | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release - | V_tuple [v] -> write_kindFromInterpValue v - | v -> failwith ("fromInterpValue write_kind: unexpected value " ^ - Interp.debug_print_value v) - end -instance (ToFromInterpValue write_kind) - let toInterpValue = write_kindToInterpValue - let fromInterpValue = write_kindFromInterpValue -end - - -let barrier_kindToInterpValue = function - | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ()) - | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ()) - | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ()) - | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ()) - | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ()) - | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ()) - | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ()) - | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ()) - | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) - | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) - | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) - end -let rec barrier_kindFromInterpValue v = match v with - | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync - | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync - | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio - | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync - | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB - | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST - | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD - | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB - | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST - | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD - | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB - | V_tuple [v] -> barrier_kindFromInterpValue v - | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^ - Interp.debug_print_value v) - end -instance (ToFromInterpValue barrier_kind) - let toInterpValue = barrier_kindToInterpValue - let fromInterpValue = barrier_kindFromInterpValue -end - - -let instruction_kindToInterpValue = function - | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) - | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) - end -let rec instruction_kindFromInterpValue v = match v with - | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch - | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple - | V_tuple [v] -> instruction_kindFromInterpValue v - | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^ - Interp.debug_print_value v) - end -instance (ToFromInterpValue instruction_kind) - let toInterpValue = instruction_kindToInterpValue - let fromInterpValue = instruction_kindFromInterpValue -end - - type regfp = | RFull of (string) | RSlice of (string * integer * integer) | RSliceBit of (string * integer) | RField of (string * string) -let regfpToInterpValue = function - | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - end - -let rec regfpFromInterpValue v = match v with - | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v) - | SI.V_tuple [v] -> regfpFromInterpValue v - | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v) - end - -instance (ToFromInterpValue regfp) - let toInterpValue = regfpToInterpValue - let fromInterpValue = regfpFromInterpValue -end +type niafp = + | NIAFP_successor + | NIAFP_concrete_address of vector bitU + | NIAFP_LR + | NIAFP_CTR + | NIAFP_register of regfp +(* only for MIPS *) +type diafp = + | DIAFP_none + | DIAFP_concrete of vector bitU + | DIAFP_reg of regfp let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function | RFull name -> @@ -1454,20 +940,6 @@ let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * Reg_field name start direction field_name slice end - -type niafp = - | NIAFP_successor - | NIAFP_concrete_address of vector bitU - | NIAFP_LR - | NIAFP_CTR - | NIAFP_register of regfp - -(* only for MIPS *) -type diafp = - | DIAFP_none - | DIAFP_concrete of vector bitU - | DIAFP_reg of regfp - let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) |