diff options
author | James Pollard <james@pollard.dev> | 2020-06-01 16:08:56 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-01 16:08:56 +0100 |
commit | 41f1832503686a6afdd1a82b761c19679611426a (patch) | |
tree | 9aa99cdb81ad31636435ae2141088fd341235f7e /src/verilog | |
parent | c3fe9469171bbf706dcb7bc84297123590377100 (diff) | |
parent | 71ba686359b9cdf2178d0837552fc564a905b18f (diff) | |
download | vericert-kvx-41f1832503686a6afdd1a82b761c19679611426a.tar.gz vericert-kvx-41f1832503686a6afdd1a82b761c19679611426a.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/HTL.v | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index a21064c..fffbb81 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -47,10 +47,13 @@ Record module: Type := mod_return : reg }. +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + (** * Operational Semantics *) -Definition genv := Globalenvs.Genv.t unit unit. -Definition genv_empty := Globalenvs.Genv.empty_genv unit unit nil. +Definition genv := Globalenvs.Genv.t fundef unit. Inductive state : Type := | State : @@ -84,15 +87,19 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := step g (State m st assoc) t (Returnstate retval). Hint Constructors step : htl. -Inductive initial_state (m : module) : state -> Prop := -| initial_state_intro : forall st, - st = m.(mod_entrypoint) -> - initial_state m (State m st empty_assocmap). +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 st m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + st = m.(mod_entrypoint) -> + initial_state p (State m st empty_assocmap). Inductive final_state : state -> Integers.int -> Prop := | final_state_intro : forall retval retvali, value_int_eqb retval retvali = true -> final_state (Returnstate retval) retvali. -Definition semantics (m : module) := - Smallstep.Semantics step (initial_state m) final_state genv_empty. +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). |