bugfixes

matter-labs · May 14, 2024 · 885b006 · 885b006
1 parent 97b68fe
commit 885b006
Show file tree

Hide file tree

Showing 14 changed files with 27 additions and 27 deletions.
diff --git a/src/sem/FarRet.v b/src/sem/FarRet.v
@@ -53,7 +53,7 @@ A normal return from a **far** call. Will pop up current callframe, return
 unspent ergs to the caller, and continue execution from the saved return
 address (from where the call had taken place). The register `args`
 describes a span of memory passed to the external caller. """,
-
+legacy = RET_LEGACY,
 semantic = r"""
 1. Fetch the value from register `args` and decode the value of type [%fwd_memory]:
 

diff --git a/src/sem/FarRevert.v b/src/sem/FarRevert.v
@@ -42,7 +42,7 @@ Section FarRevertDefinition.
 
   Inductive step_farrevert: instruction -> smallstep :=
   (** {{{
-ins = Instruction("OpRevert", "revert", in1 = In.Reg)
+ins = Instruction("OpRevert", "rev", in1 = In.Reg)
 descr = InstructionDoc(
 ins=ins,
 add_to_title = "(case of far revert)",
@@ -53,7 +53,7 @@ An abnormal return from a far call. Will pop up current callframe, give back
 unspent ergs and execute a currently active exception handler. The input register
 describes a slice of memory passed to the external caller.
 """,
-legacy="`ret.revert in1`",
+legacy = REVERT_LEGACY,
 semantic = r"""
 Restores storage to the state before external call.
 1. Let $E$ be the address of the [%active_exception_handler].

diff --git a/src/sem/Load.v b/src/sem/Load.v
@@ -9,7 +9,7 @@ Section LoadDefinition.
   Generalizable Variables cs flags regs mem.
   Inductive step_load: instruction -> tsmallstep :=
   (** {{{
-ins = Instruction("OpLoad", "ldvl", in1 = In.RegImm, out1=Out.Reg, modifiers = [Modifier.DataPageType])
+ins = Instruction("OpLoad", "ldm", in1 = In.RegImm, out1=Out.Reg, modifiers = [Modifier.DataPageType])
 descr = InstructionDoc(
 ins=ins,
 legacy = """

diff --git a/src/sem/LoadInc.v b/src/sem/LoadInc.v
@@ -8,7 +8,7 @@ Section LoadIncDefinition.
   Generalizable Variables cs flags regs mem.
   Inductive step_load_inc : instruction -> tsmallstep :=
 (** {{{
-ins=Instruction("OpLoadInc", "ldvli", in1 = In.RegImm, out1=Out.Reg, out2=Out.Reg, modifiers = [Modifier.DataPageType])
+ins=Instruction("OpLoadInc", "ldmi", in1 = In.RegImm, out1=Out.Reg, out2=Out.Reg, modifiers = [Modifier.DataPageType])
 descr = InstructionDoc(ins=ins,
 legacy = """
 - `uma.inc.heap_read in1, out1, out2` aliased as `ld.1.inc in1, out1, out2`

diff --git a/src/sem/LoadPtr.v b/src/sem/LoadPtr.v
@@ -10,7 +10,7 @@ Section LoadPtrDefinition.
  (** {{{!
 describe(InstructionDoc(
 
-ins=Instruction("OpLoadPtr", "ldp", in1 = In.RegImm, out1=Out.Reg),
+ins=Instruction("OpLoadPtr", "ldp", in1 = In.Reg, out1=Out.Reg),
 legacy = """
 - `uma.fat_ptr_read in1, out` aliased as `ld in1, out`
 """,
@@ -44,7 +44,7 @@ semantic = r"""
 4. Store the word to `res`.
 """,
 
-usage = """
+usage = f"""
 - Read data from a read-only slice returned from a far call, or passed to a far call.
 - One of few instructions that accept only reg or imm operand but do not have
   full addressing mode, therefore can't e.g. address stack. The full list is: {INSNS_USE_REGIMM}.

diff --git a/src/sem/NearCall.v b/src/sem/NearCall.v
@@ -8,10 +8,10 @@ Section NearCallDefinition.
   (** {{{!
 describe(InstructionDoc(
 
-ins=Instruction("OpNearCall", "call", in1 = In.Reg, in2 = In.Reg, imm1 = "dest",imm2="handler"),
+ins=Instruction("OpNearCall", "call", in1 = In.Reg, in2 = None, imm1 = "dest",imm2="handler"),
 
 syntax_override = [
-r"- `call abi_reg, callee_address, exception_handler` as a fully expanded form.",
+r"`call abi_reg, callee_address, exception_handler` as a fully expanded form.",
 
 r"""`call abi_reg, callee_address`
   + The assembler expands this variation to

diff --git a/src/sem/NearRet.v b/src/sem/NearRet.v
@@ -15,7 +15,7 @@ in1 = In.Reg,
 kernelOnly = False,
 notStatic = False),
 
-legacy = "`ret.ok` aliased as `ret`",
+legacy = RET_LEGACY,
 
 preamble = NEAR_FAR_RET_LIKE_PREAMBLE('near return', 'NearRetDefinition', 'far return', 'FarRetDefinition'),
 summary = """

diff --git a/src/sem/NearRetTo.v b/src/sem/NearRetTo.v
@@ -9,7 +9,7 @@ Section NearRetToDefinition.
 describe(InstructionDoc(
 
 ins = Instruction("OpNearRetTo", "retl", imm1="label"),
-legacy = "`ret.ok.to_label label` ",
+legacy = "`ret.ok.to_label label`",
 summary = """
 A normal return from a **near** call. Will pop up current callframe, give back
 unspent ergs and continue execution from an explicitly provided label.

diff --git a/src/sem/NearRevert.v b/src/sem/NearRevert.v
@@ -10,7 +10,7 @@ Section NearRevertDefinition.
 describe(InstructionDoc(
 ins=Instruction("OpRevert", "rev", in1 = In.Reg),
 add_to_title = "(case of near revert)",
-legacy = "`ret.revert` aliased as `revert`",
+legacy = REVERT_LEGACY,
 preamble = NEAR_FAR_RET_LIKE_PREAMBLE('near revert', 'NearRevertDefinition', 'far revert', 'FarRevertDefinition'),
 
 summary = """

diff --git a/src/sem/PrecompileCall.v b/src/sem/PrecompileCall.v
@@ -12,7 +12,7 @@ Section PrecompileCallDefinition.
 describe(InstructionDoc(
 
 ins=Instruction(
-"OpPrecompile",
+"OpPrecompileCall",
 "callp",
 in1 = In.Reg,
 in2 = In.Reg,

diff --git a/src/sem/SLoad.v b/src/sem/SLoad.v
@@ -22,7 +22,7 @@ semantic = r"""
 2. Store the value to `dest`.
 """,
 usage = """
-- Only [%OpSLoad] is capable of reading data from transient storage.
+- Only [%OpSLoad] is capable of reading data from storage.
 """
 ))
 }}}

diff --git a/src/sem/SStore.v b/src/sem/SStore.v
@@ -14,7 +14,7 @@ Section SStoreDefinition.
   (** {{{!
 describe(InstructionDoc(
 
-ins=Instruction(abstract_name  = "OpTransientStore", mnemonic = "stt", in1= In.Reg, in2 = In.Reg),
+ins=Instruction(abstract_name  = "OpSStore", mnemonic = "sts", in1= In.Reg, in2 = In.Reg),
 
 legacy=" `log.swrite in1, in2` aliased as `sstore in1, in2` ",
 
@@ -28,9 +28,8 @@ semantic = r"""
 """,
 
 usage = """
-- Only [%OpTransientStore] is capable to write data to storage.
-- [%OpTransientStore] is rolled back if the current frame ended by [%OpPanic] or [%OpRevert].
-- Transient storage is reset after the transaction ends.
+- Only [%OpSStore] is capable to write data to storage.
+- [%OpSStore] is rolled back if the current frame ended by [%OpPanic] or [%OpRevert].
 """,
 affectedState = """
 - Depot of the current shard.

diff --git a/src/sem/SpAdd.v b/src/sem/SpAdd.v
@@ -13,7 +13,7 @@ ins=Instruction(abstract_name = "OpSpAdd", mnemonic = "incsp", in1 = In.Reg, in2
 
 syntax_override = ["`incsp reg+imm`", "`incsp reg`", "`incsp imm`"],
 
-legacy = r"`nop r0, r0, stack+=[reg+imm]`",
+legacy = r"`nop stack+=[reg+imm]`",
 summary = " Add `(reg + imm)` to SP.",
 
 semantic = r"""

diff --git a/src/sem/_preprocess_header.py b/src/sem/_preprocess_header.py
@@ -9,21 +9,22 @@
 INSNS_USE_REGIMM = "[%OpLoad], [%OpLoadInc], [%OpStore], [%OpStoreInc], [%OpLoadPointer], [%OpLoadPointerInc], [%OpStaticReadInc], [%OpStaticRead], [%OpStaticWrite], [%OpStaticWriteInc]"
 
 
-USES_REGIMM = r"""
+USES_REGIMM = f"""
 - One of few instructions that accept only reg or imm operand but do not have
   full addressing mode, therefore can't e.g. address stack. The full list is:
   {INSNS_USE_REGIMM}.
 """
 
-INSNS_USE_REGIMM = "[%OpLoad], [%OpLoadInc], [%OpStore], [%OpStoreInc], [%OpLoadPointer], [%OpLoadPointerInc], [%OpStaticReadInc], [%OpStaticRead], [%OpStaticWrite], [%OpStaticWriteInc]"
-
+RET_LEGACY= ["`ret in1`",
+"`ret` is an alias for `ret r1`",
+"`ret.ok in1` aliased as `ret in1`"
+]
 
-USES_REGIMM = r"""
-- One of few instructions that accept only reg or imm operand but do not have
-  full addressing mode, therefore can't e.g. address stack. The full list is:
-  {INSNS_USE_REGIMM}.
-"""
 
+REVERT_LEGACY= [
+   "`revert` is an alias for `revert r1`",
+"`ret.revert in1`"
+]
 
 def heap_var_op_syntax(ins):
    return syntax(ins) + [