From 49f759ebbb3eb569c456a9dbe6affd165f3fc8b5 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 4 Jun 2021 19:08:44 +0200 Subject: starting refinement of symbolic execution --- scheduling/BTL_SEtheory.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 9ab64d7d..4b4571e4 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -437,7 +437,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := (* Syntax and Semantics of symbolic internal states *) (* [si_pre] is a precondition on initial context *) -Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }. +Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg:> reg -> sval; si_smem: smem }. (* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *) Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := @@ -446,25 +446,25 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). (** * Symbolic execution of final step *) -Definition sexec_final_sfv (i: final) (sis: sistate): sfval := +Definition sexec_final_sfv (i: final) (sreg: reg -> sval): sfval := match i with | Bgoto pc => Sgoto pc | Bcall sig ros args res pc => - let svos := sum_left_map sis.(si_sreg) ros in - let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in Scall sig svos sargs res pc | Btailcall sig ros args => - let svos := sum_left_map sis.(si_sreg) ros in - let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in Stailcall sig svos sargs | Bbuiltin ef args res pc => - let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in + let sargs := List.map (builtin_arg_map sreg) args in Sbuiltin ef sargs res pc | Breturn or => - let sor := SOME r <- or IN Some (sis.(si_sreg) r) in + let sor := SOME r <- or IN Some (sreg r) in Sreturn sor | Bjumptable reg tbl => - let sv := sis.(si_sreg) reg in + let sv := sreg reg in Sjumptable sv tbl end. -- cgit