Merge tag 'upstream/0.2'

[pkg-cerco/acc-trusted.git] / extracted / interpret2.ml

diff --git a/extracted/interpret2.ml b/extracted/interpret2.ml
index 530ad615e803415f623a53c6cdd0778b076bca00..e4b89e432be127a70d5d982aacaa2f0d39ddf84f 100644 (file)
--- a/extracted/interpret2.ml
+++ b/extracted/interpret2.ml
@@ -467,3 +467,21 @@ let aSM_preclassified_system c sigma policy =
       (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
         policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
 
+(** val aSM_status :
+    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
+    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
+let aSM_status c sigma policy =
+  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
+  let symbol_map = Status.construct_datalabels c.ASM.preamble in
+  let addr_of_label = fun x ->
+    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
+      Nat.O))))))))))))))))
+      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
+  in
+  let addr_of_symbol = fun x ->
+    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
+      (addr_of_label x)
+  in
+  aSM_abstract_status c addr_of_label addr_of_symbol sigma policy
+