Skip to content
This repository has been archived by the owner on Mar 20, 2024. It is now read-only.

Future: Investigate using analysis/optimization framework from move-prover. #204

Open
nvjle opened this issue Jun 16, 2023 · 4 comments
Open

Future: Investigate using analysis/optimization framework from move-prover. #204

nvjle opened this issue Jun 16, 2023 · 4 comments
Labels
enhancement New feature or request

Comments

@nvjle
Copy link

nvjle commented Jun 16, 2023

Currently we use only the baseline move-prover generated stackless bytecode as input to our translation. However, the prover also provides a number of potentially useful analyses and optimizations that could improve our input code. Moreover, some of these are fairly nice generic frameworks (e.g., a generic dataflow analysis framework and a generic interprocedural compositional analysis framework) that we could build our own stackless bytecode analyses and optimizations on.

Some of the analyses/optimizations are targeted only to the "specification" language, but others are generally applicable. Below is their default pipeline:

pub fn default_pipeline_with_options(options: &ProverOptions) -> FunctionTargetPipeline {
    // NOTE: the order of these processors is import!
    let mut processors: Vec<Box<dyn FunctionTargetProcessor>> = vec![
        DebugInstrumenter::new(),
        // transformation and analysis
        EliminateImmRefsProcessor::new(),
        MutRefInstrumenter::new(),
        ReachingDefProcessor::new(),
        LiveVarAnalysisProcessor::new(),
        BorrowAnalysisProcessor::new_borrow_natives(options.borrow_natives.clone()),
        MemoryInstrumentationProcessor::new(),
        CleanAndOptimizeProcessor::new(),
        UsageProcessor::new(),
        VerificationAnalysisProcessor::new(),
    ];

    if !options.skip_loop_analysis {
        processors.push(LoopAnalysisProcessor::new());
    }

    processors.append(&mut vec![
        // spec instrumentation
        SpecInstrumentationProcessor::new(),
        GlobalInvariantAnalysisProcessor::new(),
        GlobalInvariantInstrumentationProcessor::new(),
        WellFormedInstrumentationProcessor::new(),
        DataInvariantInstrumentationProcessor::new(),
        // monomorphization
        MonoAnalysisProcessor::new(),
    ]);

    if options.mutation {
        // pass which may do nothing
        processors.push(MutationTester::new());
    }

    // inconsistency check instrumentation should be the last one in the pipeline
    if options.check_inconsistency {
        processors.push(InconsistencyCheckInstrumenter::new());
    }

    if !options.for_interpretation {
        processors.push(NumberOperationProcessor::new());
    }
    ...

Of course we're generating LLVM IR and we let LLVM do much of the optimization heavy lifting. But in addition to the fact that running the prover pipeline may give us better input SBC to begin with, there may be other domain/Move-specific analyses/optimizations that are easier to apply on SBC as opposed to later in LLVM.
@nvjle nvjle added the enhancement New feature or request label Jun 16, 2023
@nvjle nvjle changed the title Investigate using analysis/optimization framework from move-prover. Future: Investigate using analysis/optimization framework from move-prover. Jun 16, 2023
@nvjle nvjle mentioned this issue Jun 30, 2023
Open
@ksolana
Copy link
Collaborator

ksolana commented Jul 14, 2023

These are good to have but we can postpone this work until stage 3.

@jcivlin
Copy link
Collaborator

jcivlin commented Sep 2, 2023

These are good to have but we can postpone this work until stage 3.

I found that compilation of stdlib (ascii.moe, in particular, but this will chain vector.move and more) generates byte code Prop, which we do not support.
I think it is coming from move-prover and due to usage of Move spec in stdlib code.

So the optimizations may wait but we need to take a deeper look at move-prover sooner.

@jcivlin
Copy link
Collaborator

jcivlin commented Sep 2, 2023

see more about Prop here: #250

@dmakarov
Copy link
Collaborator

dmakarov commented Sep 2, 2023

When I compile unit tests using move-cli with Solana backend., everything compiles correctly, including the test_ascii_chars. Here's the generated llvm code for that test.

define private void @ascii_tests__test_ascii_chars() {
entry:
  %local_0 = alloca { ptr, i64, i64 }, align 8
  %local_1 = alloca i8, align 1
  %local_2 = alloca %struct.ascii__String, align 8
  %local_3 = alloca { ptr, i64, i64 }, align 8
  %local_4 = alloca i8, align 1
  %local_5 = alloca { ptr, i64, i64 }, align 8
  %local_6 = alloca i8, align 1
  %local_7 = alloca i8, align 1
  %local_8 = alloca i1, align 1
  %local_9 = alloca i8, align 1
  %local_10 = alloca i1, align 1
  %local_11 = alloca i64, align 8
  %local_12 = alloca ptr, align 8
  %local_13 = alloca i8, align 1
  %local_14 = alloca i8, align 1
  %local_15 = alloca i8, align 1
  %local_16 = alloca i8, align 1
  %local_17 = alloca { ptr, i64, i64 }, align 8
  %local_18 = alloca %struct.ascii__String, align 8
  %local_19 = alloca ptr, align 8
  %local_20 = alloca ptr, align 8
  %local_21 = alloca i64, align 8
  %local_22 = alloca i64, align 8
  %local_23 = alloca i1, align 1
  %local_24 = alloca i64, align 8
  %local_25 = alloca ptr, align 8
  %local_26 = alloca i1, align 1
  %local_27 = alloca i1, align 1
  %local_28 = alloca i64, align 8
  %local_29 = alloca %struct.ascii__String, align 8
  %local_30 = alloca { ptr, i64, i64 }, align 8
  %local_31 = alloca ptr, align 8
  %local_32 = alloca i64, align 8
  %local_33 = alloca i64, align 8
  %local_34 = alloca i1, align 1
  %local_35 = alloca i64, align 8
  store i8 0, ptr %local_4, align 1
  %load_store_tmp = load i8, ptr %local_4, align 1
  store i8 %load_store_tmp, ptr %local_1, align 1
  %retval = call { ptr, i64, i64 } @move_native_vector_empty(ptr @__move_rttydesc_u8)
  store { ptr, i64, i64 } %retval, ptr %local_5, align 8
  %load_store_tmp1 = load { ptr, i64, i64 }, ptr %local_5, align 8
  store { ptr, i64, i64 } %load_store_tmp1, ptr %local_3, align 8
  br label %bb_6

bb_6:                                             ; preds = %join_bb, %entry
  %load_store_tmp2 = load i8, ptr %local_1, align 1
  store i8 %load_store_tmp2, ptr %local_6, align 1
  store i8 -128, ptr %local_7, align 1
  %lt_src_0 = load i8, ptr %local_6, align 1
  %lt_src_1 = load i8, ptr %local_7, align 1
  %lt_dst = icmp ult i8 %lt_src_0, %lt_src_1
  store i1 %lt_dst, ptr %local_8, align 1
  %cnd = load i1, ptr %local_8, align 1
  br i1 %cnd, label %bb_1, label %bb_0

bb_1:                                             ; preds = %bb_6
  br label %bb_2

bb_2:                                             ; preds = %bb_1
  %load_store_tmp3 = load i8, ptr %local_1, align 1
  store i8 %load_store_tmp3, ptr %local_9, align 1
  %call_arg_0 = load i8, ptr %local_9, align 1
  %retval4 = call i1 @ascii__is_valid_char(i8 %call_arg_0)
  store i1 %retval4, ptr %local_10, align 1
  %cnd5 = load i1, ptr %local_10, align 1
  br i1 %cnd5, label %bb_4, label %bb_3

bb_4:                                             ; preds = %bb_2
  br label %bb_5

bb_3:                                             ; preds = %bb_2
  store i64 0, ptr %local_11, align 8
  %call_arg_06 = load i64, ptr %local_11, align 8
  call void @move_rt_abort(i64 %call_arg_06)
  unreachable

bb_5:                                             ; preds = %bb_4
  store ptr %local_3, ptr %local_12, align 8
  %load_store_tmp7 = load i8, ptr %local_1, align 1
  store i8 %load_store_tmp7, ptr %local_13, align 1
  %loaded_alloca = load ptr, ptr %local_12, align 8
  call void @move_native_vector_push_back(ptr @__move_rttydesc_u8, ptr %loaded_alloca, ptr %local_13)
  %load_store_tmp8 = load i8, ptr %local_1, align 1
  store i8 %load_store_tmp8, ptr %local_14, align 1
  store i8 1, ptr %local_15, align 1
  %add_src_0 = load i8, ptr %local_14, align 1
  %add_src_1 = load i8, ptr %local_15, align 1
  %add_dst = add i8 %add_src_0, %add_src_1
  %ovfcond = icmp ult i8 %add_dst, %add_src_0
  br i1 %ovfcond, label %then_bb, label %join_bb

then_bb:                                          ; preds = %bb_5
  call void @move_rt_abort(i64 4017)
  unreachable

join_bb:                                          ; preds = %bb_5
  store i8 %add_dst, ptr %local_16, align 1
  %load_store_tmp9 = load i8, ptr %local_16, align 1
  store i8 %load_store_tmp9, ptr %local_1, align 1
  br label %bb_6

bb_0:                                             ; preds = %bb_6
  %load_store_tmp10 = load { ptr, i64, i64 }, ptr %local_3, align 8
  store { ptr, i64, i64 } %load_store_tmp10, ptr %local_17, align 8
  %call_arg_011 = load { ptr, i64, i64 }, ptr %local_17, align 8
  %retval12 = call %struct.ascii__String @ascii__string({ ptr, i64, i64 } %call_arg_011)
  store %struct.ascii__String %retval12, ptr %local_18, align 8
  %load_store_tmp13 = load %struct.ascii__String, ptr %local_18, align 8
  store %struct.ascii__String %load_store_tmp13, ptr %local_2, align 8
  store ptr %local_2, ptr %local_19, align 8
  %call_arg_014 = load ptr, ptr %local_19, align 8
  %retval15 = call ptr @ascii__as_bytes(ptr %call_arg_014)
  store ptr %retval15, ptr %local_20, align 8
  %loaded_alloca16 = load ptr, ptr %local_20, align 8
  %retval17 = call i64 @move_native_vector_length(ptr @__move_rttydesc_u8, ptr %loaded_alloca16)
  store i64 %retval17, ptr %local_21, align 8
  store i64 128, ptr %local_22, align 8
  %eq_src_0 = load i64, ptr %local_21, align 8
  %eq_src_1 = load i64, ptr %local_22, align 8
  %eq_dst = icmp eq i64 %eq_src_0, %eq_src_1
  store i1 %eq_dst, ptr %local_23, align 1
  %cnd18 = load i1, ptr %local_23, align 1
  br i1 %cnd18, label %bb_8, label %bb_7

bb_8:                                             ; preds = %bb_0
  br label %bb_9

bb_7:                                             ; preds = %bb_0
  store i64 0, ptr %local_24, align 8
  %call_arg_019 = load i64, ptr %local_24, align 8
  call void @move_rt_abort(i64 %call_arg_019)
  unreachable

bb_9:                                             ; preds = %bb_8
  store ptr %local_2, ptr %local_25, align 8
  %call_arg_020 = load ptr, ptr %local_25, align 8
  %retval21 = call i1 @ascii__all_characters_printable(ptr %call_arg_020)
  store i1 %retval21, ptr %local_26, align 1
  %not_src = load i1, ptr %local_26, align 1
  %not_dst = xor i1 %not_src, true
  store i1 %not_dst, ptr %local_27, align 1
  %cnd22 = load i1, ptr %local_27, align 1
  br i1 %cnd22, label %bb_11, label %bb_10

bb_11:                                            ; preds = %bb_9
  br label %bb_12

bb_10:                                            ; preds = %bb_9
  store i64 1, ptr %local_28, align 8
  %call_arg_023 = load i64, ptr %local_28, align 8
  call void @move_rt_abort(i64 %call_arg_023)
  unreachable

bb_12:                                            ; preds = %bb_11
  %call_arg_024 = load %struct.ascii__String, ptr %local_2, align 8
  %retval25 = call { ptr, i64, i64 } @ascii__into_bytes(%struct.ascii__String %call_arg_024)
  store { ptr, i64, i64 } %retval25, ptr %local_30, align 8
  %load_store_tmp26 = load { ptr, i64, i64 }, ptr %local_30, align 8
  store { ptr, i64, i64 } %load_store_tmp26, ptr %local_0, align 8
  store ptr %local_0, ptr %local_31, align 8
  %loaded_alloca27 = load ptr, ptr %local_31, align 8
  %retval28 = call i64 @move_native_vector_length(ptr @__move_rttydesc_u8, ptr %loaded_alloca27)
  store i64 %retval28, ptr %local_32, align 8
  store i64 128, ptr %local_33, align 8
  %eq_src_029 = load i64, ptr %local_32, align 8
  %eq_src_130 = load i64, ptr %local_33, align 8
  %eq_dst31 = icmp eq i64 %eq_src_029, %eq_src_130
  store i1 %eq_dst31, ptr %local_34, align 1
  %cnd32 = load i1, ptr %local_34, align 1
  br i1 %cnd32, label %bb_14, label %bb_13

bb_14:                                            ; preds = %bb_12
  br label %bb_15

bb_13:                                            ; preds = %bb_12
  store i64 2, ptr %local_35, align 8
  %call_arg_033 = load i64, ptr %local_35, align 8
  call void @move_rt_abort(i64 %call_arg_033)
  unreachable

bb_15:                                            ; preds = %bb_14
  ret void
}

The command to reproduce the compilation follows

LLVM_SYS_150_PREFIX=/path/to/move-dev \
PLATFORM_TOOLS_ROOT=/path/to/platform-tools \
MOVE_NATIVE=/path/to/move/language/move-native \
cargo run -p move-cli --features solana-backend --bin move -- test --solana -p language/tools/move-cli/tests/move_unit_tests/assign_dev_addr_for_dep

This will compile all of stdlib source file along with all stdlib unit test files. As it happens, any Move unit test depends on stdlib, and when move-cli builds the stdlib in test mode, it also compiles all stdlib unit tests.

@dmakarov dmakarov mentioned this issue Sep 3, 2023
Closed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@dmakarov @jcivlin @nvjle @ksolana