diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 8 | ||||
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 1 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 4 |
4 files changed, 9 insertions, 6 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 876685bd..b59b4144 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -38,7 +38,7 @@ end let extern_reg r slice = match (r,slice) with | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2) - | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i) + | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field y x (i,i) end let rec extern_value mode for_mem v = match v with diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index c0237cbc..8400cf36 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -146,8 +146,8 @@ let to_vec ord len n = else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n])) ;; -let exts len v = match v with - | V_vector _ inc _ -> to_vec inc len (to_num true v) +let exts (V_tuple[V_lit(L_aux (L_num len) _);v]) = match v with + | V_vector _ inc _ -> to_vec inc (natFromInteger len) (to_num true v) | V_unknown -> V_unknown end ;; @@ -278,6 +278,8 @@ let function_map = [ ("minus_vec_range", arith_op_vec_range (-) 1); ("multiply", arith_op ( * )); ("multiply_vec", arith_op_vec ( * ) 2); + ("mult_range_vec", arith_op_range_vec ( * ) 2); + ("mult_vec_range", arith_op_vec_range ( * ) 2); ("mod", arith_op (mod)); ("mod_vec", arith_op_vec (mod) 1); ("mod_vec_range", arith_op_vec_range (mod) 1); @@ -289,7 +291,7 @@ let function_map = [ ("is_one", is_one); ("to_num_inc", to_num false); ("to_num_dec", to_num false); - ("EXTS", exts 64); + ("EXTS", exts); ("to_vec_inc", to_vec_inc); ("to_vec_dec", to_vec_dec); ("bitwise_not", bitwise_not); diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index e845754d..211dd015 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -354,6 +354,7 @@ let doc_exp, doc_let = let opening = separate space [string "switch"; exp e; lbrace] in let cases = separate_map (break 1) doc_case pexps in surround 2 1 opening cases rbrace + | E_exit e -> separate space [string "exit"; exp e;] (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index f8c05085..04b7eecc 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -137,7 +137,7 @@ let rec compact_exp (E_aux (e, l)) = wrap(E_field(compact_exp e, id)) | E_assign (lexp, e) -> wrap(E_assign(lexp, compact_exp e)) | E_block [] | E_nondet [] | E_cast (_, _) | E_internal_cast (_, _) - | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ -> + | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ | E_exit _-> wrap e (* extract, compact and reverse expressions on the stack; @@ -157,7 +157,7 @@ module Reg = struct let to_string id v = sprintf "%s -> %s" id (val_to_string v) let find id m = -(* eprintf "reg_find called with %s\n" id;*) +(* eprintf "reg_find called with %s\n" id; *) let v = find id m in (* eprintf "%s -> %s\n" id (val_to_string v);*) v |