From 3655a7585c925c0bb5825a8b65bec3d8323ad3b6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 19:20:24 +0200 Subject: injector wrapper function --- backend/Inject.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'backend/Inject.v') diff --git a/backend/Inject.v b/backend/Inject.v index 6799ec8a..e65cb060 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -77,3 +77,25 @@ Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list i Definition inject prog extra_pc injections : code := snd (inject' prog extra_pc injections). *) + +Section INJECTOR. + Variable gen_injections : function -> PTree.t (list inj_instr). + + Definition transf_function (f : function) : res function := + let injections := PTree.elements (gen_injections f) in + let max_pc := max_pc_function f in + if List.forallb (fun injection => (fst injection) <=? max_pc) injections + then + OK {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) injections); + fn_entrypoint := f.(fn_entrypoint) |} + else Error (msg "Inject.transf_function: injections at bad locations"). + +Definition transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. +End INJECTOR. -- cgit