aqjune

(* sli     v3.2d, v4.2d, #32 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f605483)`;;

(*   output: - : thm = |- decode (word 1868584067) = SOME (arm_SLI_VEC Q3 Q4 32 64) *)

(* 2. Check that the symbolic output looks ok *)
let code_6f605483 = define `code_6f605483:byte list = [word 0x83; word 0x54; word 0x60; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f605483;;
g `ensures arm

aqjune

(* usra v1.2d, v3.2d, #30 *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x6f621461)`;;
(*   output: - : thm = |- decode (word 1868698721) = SOME (arm_USRA_VEC Q1 Q3 30 64 128) *)
(* 2. Check that the symbolic output looks ok *)
let code_6f621461 = define `code_6f621461:byte list = [word 0x61; word 0x14; word 0x62; word 0x6f]`;;
let execth = ARM_MK_EXEC_RULE code_6f621461;;
g `ensures arm
      (\s. aligned_bytes_loaded s (word pc) code_6f621461 /\
           read PC s = word pc)

aqjune

let test_mc =
  define_assert_from_elf "test_mc" "test.o"
[
  0x3dc00000;       (* arm_LDR Q0 X0 (Immediate_Offset (word 0)) *)
  0xa9000c22        (* arm_STP X2 X3 X1 (Immediate_Offset (iword (&0))) *)
];;

let TEST_EXEC = ARM_MK_EXEC_RULE test_mc;;

let STORE_DOES_NOT_TOUCH_LDR_Q = prove(

aqjune

(* ============= *)
(* 1. dup: https://developer.arm.com/documentation/ddi0602/2022-06/SIMD-FP-Instructions/DUP--general---Duplicate-general-purpose-register-to-vector- *)

(* dup v2.2d, x4 (0x4e080c82, 0100 1110 0000 1000 0000 1100 1000 0010) *)
(* 1. Check that decode succeeds *)
DECODE_CONV `decode (word 0x4e080c82)`;;
(*   output: - : thm = |- decode (word 1309150338) = SOME (arm_DUP Q2 X4) *)

(* 2. Check that the symbolic output looks ok *)
let code_4e080c82 = define `code_4e080c82:byte list = [word 0x82; word 0x0c; word 0x08; word 0x4e]`;;

aqjune

#map0 = affine_map<(d0, d1) -> (d0, d1)>
#map1 = affine_map<(d0) -> (d0)>
#map2 = affine_map<(d0, d1) -> (d0)>
module  {
  func @encrypt(%arg0: tensor<18x131072xi64>, %arg1: tensor<18x131072xi64>) -> tensor<18x131072xi64> {
    %cst = arith.constant dense<[1, 131072]> : tensor<2xi64>
    %cst_0 = arith.constant dense<1> : tensor<1xi64>
    %cst_1 = arith.constant dense<131072> : tensor<1xi64>
    %cst_2 = arith.constant dense<[30, 1]> : tensor<2xi64>
    %c18 = arith.constant 18 : index

aqjune

int ff_seek_frame_binary(AVFormatContext *s, int stream_index,
                         int64_t target_ts, int flags)
{
    const AVInputFormat *const avif = s->iformat;
    int64_t pos_min=pos_min, pos_max=pos_max, pos, pos_limit;
    int64_t ts_min, ts_max, ts;
    int index;
    int64_t ret; 
    AVStream *st; 
    FFStream *sti;

aqjune

int ff_seek_frame_binary(AVFormatContext *s, int stream_index,
                         int64_t target_ts, int flags)
{
    const AVInputFormat *const avif = s->iformat;
    int64_t pos_min=pos_min, pos_max=pos_max, pos, pos_limit;
    int64_t ts_min, ts_max, ts;
    int index;
    int64_t ret; 
    AVStream *st; 
    FFStream *sti;

aqjune

// RUN: iree-opt -split-input-file -iree-codegen-convert-conv-to-img2col %s

#map0 = affine_map<(d0, d1, d2, d3, d4, d5) -> (d0, d1 + d3, d2 + d4, d5)>
#map1 = affine_map<(d0, d1, d2, d3, d4, d5) -> (d0, d1, d2, d3, d4, d5)>
module  {
  func @conv_16433136(%arg0: tensor<1x16x16x4xf32>, %arg1: tensor<3x3x4x16xf32>, %arg2: tensor<1x14x14x16xf32>) -> tensor<1x14x14x16xf32> {
    %0 = linalg.init_tensor [1, 14, 14, 3, 3, 4] : tensor<1x14x14x3x3x4xf32>
    %1 = linalg.generic {indexing_maps = [#map0, #map1], iterator_types = ["parallel", "parallel", "parallel", "parallel", "parallel", "parallel"]} ins(%arg0 : tensor<1x16x16x4xf32>) outs(%0 : tensor<1x14x14x3x3x4xf32>) {
    ^bb0(%arg3: f32, %arg4: f32):  // no predecessors
      linalg.yield %arg3 : f32

aqjune

#include<iostream>
#include<sstream>
using namespace std;

int main() {
  stringstream ss;
  ss << "aa\nbb\n";
  string str1;
  getline(ss, str1);
  cout << "str(): " << ss.str() << endl;

aqjune

----------------------------------------
define i1 @merge_logical_and_and(i1 %X, i1 %Y) {
%0:
  %c = select i1 %X, i1 %Y, i1 0
  %res = and i1 %X, %c
  ret i1 %res
}
=>
define i1 @merge_logical_and_and(i1 %X, i1 %Y) {