-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsymbolic_state_cmp_impl.v
82 lines (61 loc) · 2.74 KB
/
symbolic_state_cmp_impl.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
Require Import Arith.
Require Import Nat.
Require Import Bool.
Require Import bbv.Word.
Require Import Coq.NArith.NArith.
Require Import List.
Import ListNotations.
Require Import FORVES2.constants.
Import Constants.
Require Import FORVES2.program.
Import Program.
Require Import FORVES2.execution_state.
Import ExecutionState.
Require Import FORVES2.stack_operation_instructions.
Import StackOpInstrs.
Require Import FORVES2.misc.
Import Misc.
Require Import FORVES2.symbolic_state.
Import SymbolicState.
Require Import FORVES2.symbolic_state_eval.
Import SymbolicStateEval.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.valid_symbolic_state.
Import ValidSymbolicState.
Require Import FORVES2.symbolic_state_cmp.
Import SymbolicStateCmp.
Require Import FORVES2.eval_common.
Import EvalCommon.
Require Import FORVES2.constraints.
Import Constraints.
Require Import FORVES2.context.
Import Context.
Module SymbolicStateCmpImpl.
Definition compare_sstack (sstack_val_cmp: sstack_val_cmp_t) (ctx: ctx_t) (sstk1 sstk2: sstack) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
fold_right_two_lists (fun e1 e2 => sstack_val_cmp ctx e1 e2 maxidx1 sb1 maxidx2 sb2 ops) sstk1 sstk2.
Definition compare_smemory (smemory_cmp: smemory_cmp_t) (ctx: ctx_t) (smem1 smem2: smemory) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
smemory_cmp ctx smem1 smem2 maxidx1 sb1 maxidx2 sb2 ops.
Definition compare_sstorage (sstorage_cmp: sstorage_cmp_t) (ctx: ctx_t) (sstrg1 sstrg2: sstorage) (maxidx1: nat) (sb1: sbindings) (maxidx2: nat) (sb2: sbindings) (ops: stack_op_instr_map) : bool :=
sstorage_cmp ctx sstrg1 sstrg2 maxidx1 sb1 maxidx2 sb2 ops.
Definition sstate_cmp (sstack_val_cmp: sstack_val_cmp_t) (smemory_cmp: smemory_cmp_t) (sstorage_cmp: sstorage_cmp_t) (ctx: ctx_t) (sst1 sst2: sstate) (ops: stack_op_instr_map) : bool :=
let sstk1 := get_stack_sst sst1 in
let smem1 := get_memory_sst sst1 in
let sstrg1 := get_storage_sst sst1 in
let m1 := get_smap_sst sst1 in
let maxidx1 := get_maxidx_smap m1 in
let sb1 := get_bindings_smap m1 in
let sstk2 := get_stack_sst sst2 in
let smem2 := get_memory_sst sst2 in
let sstrg2 := get_storage_sst sst2 in
let m2 := get_smap_sst sst2 in
let maxidx2 := get_maxidx_smap m2 in
let sb2 := get_bindings_smap m2 in
if compare_sstack sstack_val_cmp ctx sstk1 sstk2 maxidx1 sb1 maxidx2 sb2 ops then
if compare_smemory smemory_cmp ctx smem1 smem2 maxidx1 sb1 maxidx2 sb2 ops then
if compare_sstorage sstorage_cmp ctx sstrg1 sstrg2 maxidx1 sb1 maxidx2 sb2 ops then
true
else false
else false
else false.
End SymbolicStateCmpImpl.