From e4edfe6242c1f87bcae3beb17c398486b525dd77 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 6 May 2021 20:53:16 +0100 Subject: Prove a spec for the mapping of function params Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction. --- src/hls/HTLgen.v | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 6a2fc82..a7e3584 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -469,6 +469,17 @@ Definition return_val fin rtrn r := Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)). +Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := + match l with + | nil => ret nil + | arg::args => + do param_reg <- map_externctrl fn (ctrl_param n); + do rest <- xmap_externctrl_params (S n) fn args; + ret ((param_reg, arg) :: rest) + end. + +Definition map_externctrl_params := xmap_externctrl_params 0. + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -497,11 +508,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then - do params <- traverselist - (fun (a: nat * reg) => let (idx, arg) := a in - do param_reg <- map_externctrl fn (ctrl_param idx); - ret (param_reg, arg)) - (enumerate 0 args); + do params <- map_externctrl_params fn args; do _ <- declare_reg None dst 32; do join_state <- create_state; -- cgit