summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64_small/gen/ast.hgen2
-rw-r--r--aarch64_small/gen/fold.hgen2
-rw-r--r--aarch64_small/gen/lexer.hgen17
-rw-r--r--aarch64_small/gen/map.hgen2
-rw-r--r--aarch64_small/gen/parser.hgen12
-rw-r--r--aarch64_small/gen/pretty.hgen6
-rw-r--r--aarch64_small/gen/regs_out_in.hgen6
-rw-r--r--aarch64_small/gen/sail_trans_out.hgen8
-rw-r--r--aarch64_small/gen/token_types.hgen4
-rw-r--r--aarch64_small/gen/tokens.hgen5
-rw-r--r--aarch64_small/gen/trans_sail.hgen12
-rw-r--r--aarch64_small/gen/types.hgen4
-rw-r--r--aarch64_small/gen/types_sail_trans_out.hgen19
-rw-r--r--aarch64_small/gen/types_trans_sail.hgen6
-rw-r--r--src/libsail.mllib1
15 files changed, 105 insertions, 1 deletions
diff --git a/aarch64_small/gen/ast.hgen b/aarch64_small/gen/ast.hgen
index 98148a5c..3f0ce79d 100644
--- a/aarch64_small/gen/ast.hgen
+++ b/aarch64_small/gen/ast.hgen
@@ -43,3 +43,5 @@
| `AArch64TestBitAndBranch of inst_reg*reg_size*uinteger*bit*bit64 (* t,datasize,bit_pos,bit_val,offset *)
| `AArch64MoveSystemRegister of inst_reg*uinteger*uinteger*uinteger*uinteger*uinteger*boolean (* t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read *)
| `AArch64MoveSystemImmediate of bit4*pSTATEField (* operand,field *)
+ | `AArch64DataCache of inst_reg*dCOp
+ | `AArch64InstructionCache of inst_reg*iCOp
diff --git a/aarch64_small/gen/fold.hgen b/aarch64_small/gen/fold.hgen
index fbe52794..411262e5 100644
--- a/aarch64_small/gen/fold.hgen
+++ b/aarch64_small/gen/fold.hgen
@@ -43,3 +43,5 @@
| `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> fold_reg t (y_reg, y_sreg)
| `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> fold_reg t (y_reg, y_sreg)
| `AArch64MoveSystemImmediate (operand,field) -> (y_reg, y_sreg)
+| `AArch64DataCache (t, dc_op) -> fold_reg t (y_reg, y_sreg)
+| `AArch64InstructionCache (t, ic_op) -> fold_reg t (y_reg, y_sreg)
diff --git a/aarch64_small/gen/lexer.hgen b/aarch64_small/gen/lexer.hgen
index 6ff24317..e0550dd0 100644
--- a/aarch64_small/gen/lexer.hgen
+++ b/aarch64_small/gen/lexer.hgen
@@ -223,6 +223,9 @@
"MRS" , MRS {txt="MRS"} ;
"MSR" , MSR {txt="MSR"} ;
+ "DC" , DC {txt="DC"} ;
+ "IC" , IC {txt="IC"} ;
+
(*** instructions/operands ***)
@@ -307,3 +310,17 @@
"SPSel" , PSTATEFIELD (PSTATEField_SP) ;
"DAIFSet" , PSTATEFIELD (PSTATEField_DAIFSet) ;
"DAIFClr" , PSTATEFIELD (PSTATEField_DAIFClr) ;
+
+ "IVAC" , DCOP (IVAC) ;
+ "ISW" , DCOP (ISW) ;
+ "CSW" , DCOP (CSW) ;
+ "CISW" , DCOP (CISW) ;
+ "ZVA" , DCOP (ZVA) ;
+ "CVAC" , DCOP (CVAC) ;
+ "CVAU" , DCOP (CVAU) ;
+ "CIVAC" , DCOP (CIVAC) ;
+
+ "IALLUIS" , ICOP (IALLUIS) ;
+ "IALLU" , ICOP (IALLU) ;
+ "IVAU" , ICOP (IVAU) ;
+
diff --git a/aarch64_small/gen/map.hgen b/aarch64_small/gen/map.hgen
index 3d5419b4..1957a03d 100644
--- a/aarch64_small/gen/map.hgen
+++ b/aarch64_small/gen/map.hgen
@@ -43,3 +43,5 @@
| `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> `AArch64TestBitAndBranch (map_reg t,datasize,bit_pos,bit_val,offset)
| `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> `AArch64MoveSystemRegister (map_reg t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read)
| `AArch64MoveSystemImmediate (operand,field) -> `AArch64MoveSystemImmediate (operand,field)
+| `AArch64DataCache (t, dc_op) -> `AArch64DataCache (map_reg t, dc_op)
+| `AArch64InstructionCache (t, ic_op) -> `AArch64InstructionCache (map_reg t, ic_op)
diff --git a/aarch64_small/gen/parser.hgen b/aarch64_small/gen/parser.hgen
index 53fc1c8f..685dc218 100644
--- a/aarch64_small/gen/parser.hgen
+++ b/aarch64_small/gen/parser.hgen
@@ -1401,3 +1401,15 @@
| MSR SYSREG COMMA xreg
{ if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <systemreg>, <Xt>")
else `AArch64MoveSystemRegister($4,$2.sys_op0,$2.sys_op1,$2.sys_op2,$2.sys_crn,$2.sys_crm,false) }
+
+ /* DC */
+
+ | DC DCOP COMMA xreg
+ { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <dc_op>, <Xt>")
+ else `AArch64DataCache($4,$2) }
+
+ /* IC */
+
+ | IC ICOP COMMA xreg
+ { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <ic_op>, <Xt>")
+ else `AArch64InstructionCache($4,$2) }
diff --git a/aarch64_small/gen/pretty.hgen b/aarch64_small/gen/pretty.hgen
index b412fdda..998e58ad 100644
--- a/aarch64_small/gen/pretty.hgen
+++ b/aarch64_small/gen/pretty.hgen
@@ -394,3 +394,9 @@
| `AArch64MoveSystemImmediate (operand,field) ->
sprintf "MSR %s,%s" (pp_pstatefield field) (pp_imm operand)
+
+| `AArch64DataCache (t, dc_op) ->
+ sprintf "DC %s,%s" (pp_dcop dc_op) (pp_regzr Set64 t)
+
+| `AArch64InstructionCache (t, ic_op) ->
+ sprintf "IC %s,%s" (pp_icop ic_op) (pp_regzr Set64 t)
diff --git a/aarch64_small/gen/regs_out_in.hgen b/aarch64_small/gen/regs_out_in.hgen
index bab53be7..72b1ac3c 100644
--- a/aarch64_small/gen/regs_out_in.hgen
+++ b/aarch64_small/gen/regs_out_in.hgen
@@ -154,3 +154,9 @@
| `AArch64MoveSystemImmediate (_operand,_field) ->
([], [], [], [Next])
+
+| `AArch64DataCache (_t, _dc_op) ->
+ failwith "is anyone using this?"
+
+| `AArch64InstructionCache (_t, _ic_op) ->
+ failwith "is anyone using this?"
diff --git a/aarch64_small/gen/sail_trans_out.hgen b/aarch64_small/gen/sail_trans_out.hgen
index 0399fa8b..9f84411b 100644
--- a/aarch64_small/gen/sail_trans_out.hgen
+++ b/aarch64_small/gen/sail_trans_out.hgen
@@ -326,3 +326,11 @@
| "MoveSystemImmediate", [operand; field] ->
`AArch64MoveSystemImmediate ( translate_out_int operand,
translate_out_pSTATEField field)
+
+| "DataCache", [t; dc_op] ->
+ `AArch64DataCache ( translate_out_regzr Set64 t,
+ translate_out_dCOp dc_op)
+
+| "InstructionCache", [t; ic_op] ->
+ `AArch64InstructionCache (translate_out_regzr Set64 t,
+ translate_out_iCOp ic_op)
diff --git a/aarch64_small/gen/token_types.hgen b/aarch64_small/gen/token_types.hgen
index 411dddf9..bf17cd13 100644
--- a/aarch64_small/gen/token_types.hgen
+++ b/aarch64_small/gen/token_types.hgen
@@ -69,6 +69,8 @@ type token_RET = {txt : string}
type token_TST = {txt : string}
type token_MRS = {txt : string}
type token_MSR = {txt : string}
+type token_DC = {txt : string}
+type token_IC = {txt : string}
(*** instructions/operands ***)
@@ -83,3 +85,5 @@ type token_BARROP = {domain : mBReqDomain; types : mBReqTypes}
type token_PRFOP = inst_reg (* this is an int that is encoded in a reg field *)
type token_SYSREG = {sys_op0 : uinteger; sys_op1 : uinteger; sys_op2 : uinteger; sys_crn : uinteger; sys_crm : uinteger}
type token_PSTATEFIELD = pSTATEField
+type token_DCOP = dCOp
+type token_ICOP = iCOp
diff --git a/aarch64_small/gen/tokens.hgen b/aarch64_small/gen/tokens.hgen
index bf49e463..18142bc7 100644
--- a/aarch64_small/gen/tokens.hgen
+++ b/aarch64_small/gen/tokens.hgen
@@ -62,6 +62,8 @@
%token <AArch64HGenBase.token_TST> TST
%token <AArch64HGenBase.token_MRS> MRS
%token <AArch64HGenBase.token_MSR> MSR
+%token <AArch64HGenBase.token_DC> DC
+%token <AArch64HGenBase.token_IC> IC
/*** instructions/operands ***/
@@ -75,4 +77,5 @@
%token <AArch64HGenBase.token_PRFOP> PRFOP
%token <AArch64HGenBase.token_SYSREG> SYSREG
%token <AArch64HGenBase.token_PSTATEFIELD> PSTATEFIELD
-
+%token <AArch64HGenBase.token_DCOP> DCOP
+%token <AArch64HGenBase.token_ICOP> ICOP
diff --git a/aarch64_small/gen/trans_sail.hgen b/aarch64_small/gen/trans_sail.hgen
index df2ed81c..7ad837d9 100644
--- a/aarch64_small/gen/trans_sail.hgen
+++ b/aarch64_small/gen/trans_sail.hgen
@@ -379,3 +379,15 @@
[translate_bit4 "operand" operand;
translate_pSTATEField "field" field],
[])
+
+| `AArch64DataCache (t, dc_op) ->
+ ("DataCache",
+ [translate_reg "t" t;
+ translate_dCOp "dc_op" dc_op],
+ [])
+
+| `AArch64InstructionCache (t, ic_op) ->
+ ("InstructionCache",
+ [translate_reg "t" t;
+ translate_iCOp "ic_op" ic_op],
+ [])
diff --git a/aarch64_small/gen/types.hgen b/aarch64_small/gen/types.hgen
index d581a233..c2a9c3e0 100644
--- a/aarch64_small/gen/types.hgen
+++ b/aarch64_small/gen/types.hgen
@@ -88,3 +88,7 @@ type revOp = RevOp_RBIT | RevOp_REV16 | RevOp_REV32 | RevOp_REV64
type pSTATEField = PSTATEField_DAIFSet | PSTATEField_DAIFClr |
PSTATEField_SP
+
+type dCOp = IVAC | ISW | CSW | CISW | ZVA | CVAC | CVAU | CIVAC
+
+type iCOp = IALLUIS | IALLU | IVAU
diff --git a/aarch64_small/gen/types_sail_trans_out.hgen b/aarch64_small/gen/types_sail_trans_out.hgen
index 082a5464..89fbad42 100644
--- a/aarch64_small/gen/types_sail_trans_out.hgen
+++ b/aarch64_small/gen/types_sail_trans_out.hgen
@@ -187,3 +187,22 @@ let translate_out_pSTATEField inst =
| 1 -> PSTATEField_DAIFClr
| 2 -> PSTATEField_SP
| _ -> assert false
+
+let translate_out_dCOp inst =
+ match translate_out_enum inst with
+ | 0 -> IVAC
+ | 1 -> ISW
+ | 2 -> CSW
+ | 3 -> CISW
+ | 4 -> ZVA
+ | 5 -> CVAC
+ | 6 -> CVAU
+ | 7 -> CIVAC
+ | _ -> assert false
+
+let translate_out_iCOp inst =
+ match translate_out_enum inst with
+ | 0 -> IALLUIS
+ | 1 -> IALLU
+ | 2 -> IVAU
+ | _ -> assert false
diff --git a/aarch64_small/gen/types_trans_sail.hgen b/aarch64_small/gen/types_trans_sail.hgen
index 7f2d5fe7..8081e316 100644
--- a/aarch64_small/gen/types_trans_sail.hgen
+++ b/aarch64_small/gen/types_trans_sail.hgen
@@ -117,3 +117,9 @@ let translate_revOp =
let translate_pSTATEField =
translate_enum [PSTATEField_DAIFSet; PSTATEField_DAIFClr; PSTATEField_SP]
+
+let translate_dCOp =
+ translate_enum [IVAC; ISW; CSW; CISW; ZVA; CVAC; CVAU; CIVAC]
+
+let translate_iCOp =
+ translate_enum [IALLUIS; IALLU; IVAU]
diff --git a/src/libsail.mllib b/src/libsail.mllib
index fb3d1264..2d1f568f 100644
--- a/src/libsail.mllib
+++ b/src/libsail.mllib
@@ -52,6 +52,7 @@ Sail
Sail2_values
Sail_lib
Scattered
+Smtlib
Spec_analysis
Specialize
State
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:23:04 +0000